{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:11:52Z","timestamp":1760134312051,"version":"build-2065373602"},"reference-count":60,"publisher":"MDPI AG","issue":"12","license":[{"start":{"date-parts":[[2023,11,26]],"date-time":"2023-11-26T00:00:00Z","timestamp":1700956800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Future Internet"],"abstract":"<jats:p>The study of business process analysis and optimisation has attracted significant scholarly interest in the recent past, due to its integral role in boosting organisational performance. A specific area of focus within this broader research field is process mining (PM). Its purpose is to extract knowledge and insights from event logs maintained by information systems, thereby discovering process models and identifying process-related issues. On the other hand, statistical model checking (SMC) is a verification technique used to analyse and validate properties of stochastic systems that employs statistical methods and random sampling to estimate the likelihood of a property being satisfied. In a seamless business setting, it is essential to validate and verify process models. The objective of this paper is to apply the SMC technique in process mining for the verification and validation of process models with stochastic behaviour and large state space, where probabilistic model checking is not feasible. We propose a novel methodology in this research direction that integrates SMC and PM by formally modelling discovered and replayed process models and apply statistical methods to estimate the results. The methodology facilitates an automated and proficient evaluation of the extent to which a process model aligns with user requirements and assists in selecting the optimal model. We demonstrate the effectiveness of our methodology with a case study of a loan application process performed in a financial institution that deals with loan applications submitted by customers. The case study highlights our methodology\u2019s capability to identify the performance constraints of various process models and aid enhancement efforts.<\/jats:p>","DOI":"10.3390\/fi15120378","type":"journal-article","created":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T03:35:06Z","timestamp":1701056106000},"page":"378","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Statistical Model Checking in Process Mining: A Comprehensive Approach to Analyse Stochastic Processes"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0379-5764","authenticated-orcid":false,"given":"Fawad Ali","family":"Mangi","sequence":"first","affiliation":[{"name":"School of Computing and Information Technology, University of Wollongong, Wollongong 2522, Australia"},{"name":"Department of Computer Systems Engineering, Mehran University of Engineering and Technology Jamshoro, Sindh 76062, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2087-4894","authenticated-orcid":false,"given":"Guoxin","family":"Su","sequence":"additional","affiliation":[{"name":"School of Computing and Information Technology, University of Wollongong, Wollongong 2522, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1326-1106","authenticated-orcid":false,"given":"Minjie","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computing and Information Technology, University of Wollongong, Wollongong 2522, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2023,11,26]]},"reference":[{"key":"ref_1","unstructured":"der Aalst, V., and Mining, W.P. (2011). Discovery, Conformance and Enhancement of Business Processes, Springer."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2229156.2229157","article-title":"Process mining: Overview and opportunities","volume":"3","year":"2012","journal-title":"ACM Trans. Manag. Inf. Syst. (TMIS)"},{"key":"ref_3","unstructured":"van Dongen, B. (2023, July 10). BPI Challenge 2017. Available online: https:\/\/data.4tu.nl\/articles\/_\/12696884\/1."},{"key":"ref_4","unstructured":"Mannhardt, F., De Leoni, M., Reijers, H.A., and Van Der Aalst, W.M. (2017). Advanced Information Systems Engineering: 29th International Conference, CAiSE 2017, Essen, Germany, 12\u201316 June 2017, Springer. Proceedings 29."},{"key":"ref_5","unstructured":"Dees, M., and van Dongen, B. (2023, July 15). BPI Challenge 2016: Clicks Logged In. Available online: https:\/\/data.4tu.nl\/articles\/_\/12674816\/1."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., and Vandin, A. (November, January 30). BProVe: A formal verification framework for business process models. Proceedings of the 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA.","DOI":"10.1109\/ASE.2017.8115635"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/s10844-017-0474-3","article-title":"Model mining: Integrating data analytics, modelling and verification","volume":"52","author":"Cerone","year":"2019","journal-title":"J. Intell. Inf. Syst."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"59843","DOI":"10.1109\/ACCESS.2018.2874937","article-title":"Formal Verification of Temporal Constraints for Mobile Service-Based Business Process Models","volume":"6","author":"Zhao","year":"2018","journal-title":"IEEE Access"},{"key":"ref_9","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_10","first-page":"639","article-title":"Model checking: Software and beyond","volume":"13","author":"Clarke","year":"2007","journal-title":"J. Univ. Comput. Sci."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Dumas, M., La Rosa, M., Mendling, J., and Reijers, H.A. (2018). Fundamentals of Business Process Management, Springer.","DOI":"10.1007\/978-3-662-56509-4"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1128","DOI":"10.1109\/TKDE.2004.47","article-title":"Workflow mining: Discovering process models from event logs","volume":"16","author":"Weijters","year":"2004","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"ref_13","unstructured":"Van der Aalst, W.M., de Beer, H.T., and van Dongen, B.F. (2005). On the Move to Meaningful Internet Systems 2005: CoopIS, DOA, and ODBASE: OTM Confederated International Conferences, CoopIS, DOA, and ODBASE 2005, Agia Napa, Cyprus, 31 October\u20134 November 2005, Springer. Proceedings, Part I."},{"key":"ref_14","unstructured":"R\u00e4im, M., Di Ciccio, C., Maggi, F.M., Mecella, M., and Mendling, J. (2014). On the Move to Meaningful Internet Systems: OTM 2014 Conferences: Confederated International Conferences: CoopIS, and ODBASE 2014, Amantea, Italy, 27\u201331 October 2014, Springer. Proceedings."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/j.dss.2003.12.001","article-title":"Model checking for design and assurance of e-Business processes","volume":"39","author":"Anderson","year":"2005","journal-title":"Decis. Support Syst."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Gu, R., Marinescu, R., Seceleanu, C., and Lundqvist, K. (2018, January 2). Formal verification of an autonomous wheel loader by model checking. Proceedings of the 6th Conference on Formal Methods in Software Engineering, Gothenburg, Sweden.","DOI":"10.1145\/3193992.3193999"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Munoz-Gama, J., Martin, N., Fernandez-Llatas, C., Johnson, O.A., Sep\u00falveda, M., Helm, E., Galvez-Yanjari, V., Rojas, E., Martinez-Millana, A., and Aloini, D. (2022). Process mining for healthcare: Characteristics and challenges. J. Biomed. Inform., 127.","DOI":"10.1016\/j.jbi.2022.103994"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Katoen, J.P. (2016, January 5\u20138). The probabilistic model checking landscape. Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, New York, NY, USA.","DOI":"10.1145\/2933575.2934574"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Bergami, G., Maggi, F.M., Montali, M., and Pe\u00f1aloza, R. (November, January 31). Probabilistic trace alignment. Proceedings of the 2021 3rd International Conference on Process Mining (ICPM), Eindhoven, The Netherlands.","DOI":"10.1109\/ICPM53251.2021.9576856"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Sala\u00fcn, G., and Zuo, A. (2022, January 7\u201310). Probabilistic model checking of BPMN processes at runtime. Proceedings of the International Conference on Integrated Formal Methods, Lugano, Switzerland.","DOI":"10.1007\/978-3-031-07727-2_11"},{"key":"ref_21","unstructured":"Mangi, F.A., Su, G., and Zhang, M. (2023, January 19\u201321). PM2PMC: A Probabilistic Model Checking Approach in Process Mining. Proceedings of the 2023 IEEE IAS Global Conference on Emerging Technologies (GlobConET), London, UK."},{"key":"ref_22","unstructured":"Mangi, F.A., Su, G., and Zhang, M. (2023, January 24\u201327). Integrating Process Mining with Probabilistic Model Checking via Continuous Time Markov Chains. Proceedings of the FCS\u201923, 19th International Conference on Foundations of Computer Science, Las Vegas, NV, USA. (forthcoming)."},{"key":"ref_23","unstructured":"Younes, H.L.S. (2004). Verification and Planning for Stochastic Processes with Asynchronous Events, Carnegie Mellon University."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Van Der Aalst, W., and van der Aalst, W. (2016). Data Science in Action, Springer.","DOI":"10.1007\/978-3-662-49851-4_1"},{"key":"ref_25","unstructured":"Petri, C.A. (1962). Kommunikation Mit Automaten. [Ph.D. Thesis, University of Bonn]."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Reisig, W., and Rozenberg, G. (1998). Lectures on Petri Nets I: Basic Models: Advances in Petri Nets, Springer Science & Business Media.","DOI":"10.1007\/3-540-65306-6"},{"key":"ref_27","unstructured":"OMG, B.P.M. (2023, July 15). Notation (BPMN) Version 2.0 (2011). Available online: http:\/\/www.omg.org\/spec\/BPMN\/2.0."},{"key":"ref_28","unstructured":"Ashok, P., K\u0159et\u00ednsk\u1ef3, J., and Weininger, M. (2019). Computer Aided Verification: 31st International Conference, CAV 2019, New York, NY, USA, 15\u201318 July 2019, Springer. Proceedings, Part I 31."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/s10009-022-00685-9","article-title":"Analyzing neural network behavior through deep statistical model checking","volume":"25","author":"Gros","year":"2022","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Agarwal, C., Guha, S., K\u0159et\u00ednsk\u1ef3, J., and Muruganandham, P. (2022, January 7\u201310). PAC Statistical Model Checking of Mean Payoff in Discrete-and Continuous-Time MDP. Proceedings of the International Conference on Computer Aided Verification, Haifa, Israel.","DOI":"10.1007\/978-3-031-13188-2_1"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158668","article-title":"A survey of statistical model checking","volume":"28","author":"Agha","year":"2018","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"key":"ref_32","unstructured":"Younes, H.L., and Simmons, R.G. (2002). Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, 27\u201331 July 2002, Springer. Proceedings 14."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Mooney, C.Z. (1997). Monte Carlo Simulation\/Christopher Z. Mooney, Sage Publications. No. 07-116.","DOI":"10.4135\/9781412985116"},{"key":"ref_34","unstructured":"Wald, A. (1992). Breakthroughs in Statistics: Foundations and Basic Theory, Springer."},{"key":"ref_35","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., and Peyronnet, S. (2004). Verification, Model Checking, and Abstract Interpretation: 5th International Conference, VMCAI 2004 Venice, Italy, 11\u201313 January 2004, Springer. Proceedings 5."},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Hoeffding, W. (1994). The collected works of Wassily Hoeffding, Springer Science & Business Media.","DOI":"10.1007\/978-1-4612-0865-5_38"},{"key":"ref_37","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., and Zuliani, P. (2009). Computational Methods in Systems Biology: 7th International Conference, CMSB 2009, Bologna, Italy, 31 August\u20131 September 2009, Springer. Proceedings 7."},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"100514","DOI":"10.1016\/j.accinf.2021.100514","article-title":"Embedding process mining into financial statement audits","volume":"41","author":"Werner","year":"2021","journal-title":"Int. J. Account. Inf. Syst."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10844-022-00759-9","article-title":"A natural language querying interface for process mining","volume":"61","author":"Barbieri","year":"2023","journal-title":"J. Intell. Inf. Syst."},{"key":"ref_40","unstructured":"Clarke, E.M., and Wang, Q. (2014, January 24\u201327). 25 Years of Model Checking. Proceedings of the Ershov Memorial Conference 2014, St. Petersburg, Russia. Perspectives of System Informatics."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"785","DOI":"10.1109\/TCSS.2018.2865217","article-title":"Applying probabilistic model checking to financial production risk evaluation and control: A case study of Alibaba\u2019s Yu\u2019e Bao","volume":"5","author":"Gao","year":"2018","journal-title":"IEEE Trans. Comput. Soc. Syst."},{"key":"ref_42","unstructured":"Van Dongen, B.F., de Medeiros, A.K.A., Verbeek, H., Weijters, A., and van Der Aalst, W.M. (2005). Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, FL, USA, 20\u201325 June 2005, Springer. Proceedings 26."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Leemans, S.J., Poppe, E., and Wynn, M.T. (2019, January 24\u201326). Directly follows-based process mining: Exploration & a case study. Proceedings of the 2019 International Conference on Process Mining (ICPM), Aachen, Germany.","DOI":"10.1109\/ICPM.2019.00015"},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Boltenhagen, M., Chatain, T., and Carmona, J. (November, January 31). An A-Algorithm for Computing Discounted Anti-Alignments in Process Mining. Proceedings of the 2021 3rd International Conference on Process Mining (ICPM), Eindhoven, The Netherlands.","DOI":"10.1109\/ICPM53251.2021.9576887"},{"key":"ref_45","unstructured":"Maggi, F.M., Westergaard, M., Montali, M., and van der Aalst, W.M. (2012). Runtime Verification: Second International Conference, RV 2011, San Francisco, CA, USA, 27\u201330 September 2011, Springer. Revised Selected Papers 2."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"101724","DOI":"10.1016\/j.is.2021.101724","article-title":"Stochastic process mining: Earth movers\u2019 stochastic conformance","volume":"102","author":"Leemans","year":"2021","journal-title":"Inf. Syst."},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"796","DOI":"10.1093\/logcom\/exad012","article-title":"Incrementally predictive runtime verification","volume":"33","author":"Ferrando","year":"2023","journal-title":"J. Log. Comput."},{"key":"ref_48","first-page":"312","article-title":"Automated simulation and verification of process models discovered by process mining","volume":"61","author":"Zakarija","year":"2020","journal-title":"Autom. \u010casopis Za Autom. Mjer. Elektron. Ra\u010dunarstvo I Komun."},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","article-title":"Statistical probabilistic model checking with a focus on time-bounded properties","volume":"204","author":"Younes","year":"2006","journal-title":"Inf. Comput."},{"key":"ref_50","unstructured":"Sen, K., Viswanathan, M., and Agha, G. (2004). Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, 13\u201317 July 2004, Springer. Proceedings 16."},{"key":"ref_51","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10009-015-0384-z","article-title":"Statistical model checking: Challenges and perspectives","volume":"17","author":"Legay","year":"2015","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_52","doi-asserted-by":"crossref","unstructured":"Casaluce, R., Burattin, A., Chiaromonte, F., and Vandin, A. (2022, January 11\u201316). Process Mining Meets Statistical Model Checking: Towards a Novel Approach to Model Validation and Enhancement. Proceedings of the International Conference on Business Process Management, M\u00fcnster, Germany.","DOI":"10.1007\/978-3-031-25383-6_18"},{"key":"ref_53","unstructured":"Van Der Aalst, W.M., and Pesic, M. (2006). Web Services and Formal Methods: Third International Workshop, WS-FM 2006 Vienna, Austria, 8\u20139 September 2006, Springer. Proceedings 3."},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1016\/j.is.2007.07.001","article-title":"Conformance checking of processes based on monitoring real behavior","volume":"33","author":"Rozinat","year":"2008","journal-title":"Inf. Syst."},{"key":"ref_55","unstructured":"Adriansyah, A. (2014). Aligning Observed and Modeled Behavior. [Ph.D. Thesis, Technische Universiteit Eindhoven]."},{"key":"ref_56","unstructured":"Kwiatkowska, M., Norman, G., and Parker, D. (2007). Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, 28 May\u20132 June 2007, Springer. Advanced Lectures 7."},{"key":"ref_57","unstructured":"Sen, K., Viswanathan, M., and Agha, G. (2005). Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, 6\u201310 July 2005, Springer. Proceedings 17."},{"key":"ref_58","unstructured":"Verbeek, H., Buijs, J., Van Dongen, B., and van der Aalst, W.M. (2010, January 14\u201316). Prom 6: The process mining toolkit. Proceedings of the Business Process Management Demonstration Track, Hoboken, NJ, USA."},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., and Parker, D. (2011, January 14\u201320). PRISM 4.0: Verification of Probabilistic Real-time Systems. Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), Snowbird, UT, USA.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref_60","unstructured":"Wald, A. (1949). The Annals of Mathematical Statistics, Edwards Bros."}],"container-title":["Future Internet"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-5903\/15\/12\/378\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T21:30:46Z","timestamp":1760131846000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-5903\/15\/12\/378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,26]]},"references-count":60,"journal-issue":{"issue":"12","published-online":{"date-parts":[[2023,12]]}},"alternative-id":["fi15120378"],"URL":"https:\/\/doi.org\/10.3390\/fi15120378","relation":{},"ISSN":["1999-5903"],"issn-type":[{"type":"electronic","value":"1999-5903"}],"subject":[],"published":{"date-parts":[[2023,11,26]]}}}