Process mining techniques are widely used to discover, monitor, and improve real processes based on digital traces captured in event logs. This paper proposes an integrated tool framework which allows performance evaluation, and quantitative compliance checking of process models discovered using process mining techniques. Our approach involves learning the process model, i.e., Petri Net from an existing event log by using ProM toolset. We generate its reachability graph, and extract important state and transition related information. We encode this information into mCRL2 formal specification language and use its associated toolset to generate the corresponding Labeled Transition System (LTS). Next, we transform this LTS model into an action-labeled discrete-time Markov chain (ADTMC) by simulating the event log on the LTS model. We use an action-based Probabilistic Computation Tree Logic (APCTL) and APCTL* for specifying interesting performance and compliance related properties. In the final step, we apply probabilistic model and logical embeddings which enable one to efficiently verify probabilistic process algebraic models using PRISM model checker. We validate the efficacy of our approach by applying it on several interesting case studies from different application domains.