## 4 Proposed Framework
### Modelling and Verification
* (4)[PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON] Data-driven process discovery-revealing conditional infrequent behavior from event logs. In _Advanced Information Systems Engineering: 29 th International Conference, CAISE 2017, Essen, Germany, 12-16 June 2017_; Proceedings 29; Springer: Cham, Switzerland, 2017; pp. 545-560. * (5) [PERSON]; [PERSON] [PERSON] BPI Challenge 2016: Clicks Logged In. 2016. Available online: [[https://data.ttu.nl/articles/_/12674816/1](https://data.ttu.nl/articles/_/12674816/1)]([https://data.ttu.nl/articles/_/12674816/1](https://data.ttu.nl/articles/_/12674816/1)) (accessed on 15 July 2023). * (6)[PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON] BProVe: A formal verification framework for business process models. In Proceedings of the 2017 32 nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 30 October-3 November 2017; pp. 217-228. * (7)[PERSON] Model mining: Integrating data analytics, modelling and verification. _J. Intell. Inf. Syst._**2019**, 52, 501-532. [CrossRef]
* (8)[PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] Formal Verification of Temporal Constraints for Mobile Service-Based Business Process Models. _IEEE Access_**2018**, 6, 59843-59852. [CrossRef]
* (9)[PERSON]; [PERSON] _Principles of Model Checking_; MIT Press: Cambridge, MA, USA, 2008. * (10)[PERSON]; [PERSON] Model checking: Software and beyond. _J. Univ. Comput. Sci._**2007**, 13, 639-649. * (11)[PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] _Fundamentals of Business Process Management_; Springer: Berlin/Heidelberg, Germany, 2018; Volume 2. * _[PERSON] et al. (2004)_ [PERSON] [PERSON]; [PERSON]; [PERSON] Workflow mining: Discovering process models from event logs. _IEEE Trans. Knowl. Data Eng._**2004**, _16_, 1128-1142. [CrossRef]
* _[PERSON] et al. (2005)_ [PERSON] [PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON] Process mining and verification of properties: An approach based on temporal logic. In _On the Move to Meaningful Internet Systems 2005: CooplS, DOA, and ODBASE: OTM Confedrated International Conferences, CooplS, DOA, and ODBASE 2005, Agia Napa, Cyprus, 31 October-4 November 2005_; Proceedings, Part I; Springer: Berlin/Heidelberg, Germany, 2005; pp. 130-147. * _[PERSON] et al. (2014)_ [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON] Log-based understanding of business processes through temporal logic query checking. In _On the Move to Meaningful Internet Systems: OTM 2014 Conferences: Confearted International Conferences: CooplS, and ODBASE 2014, Anamate, Italy, 27-31 October 2014_; Proceedings; Springer: Berlin/Heidelberg, Germany, 2014; pp. 75-92. * _[PERSON] et al. (2005)_ [PERSON]; [PERSON]; [PERSON]; [PERSON] Model checking for design and assurance of e-Business processes. _Decis. Support Syst._**2005**, _39_, 333-344. [CrossRef]
* _[PERSON] et al. (2018)_ [PERSON]; [PERSON]; [PERSON]; [PERSON] Formal verification of an autonomous wheel loader by model checking. In Proceedings of the 6 th Conference on Formal Methods in Software Engineering, Gothenburg, Sweden, 2 June 2018; pp. 74-83. * _[PERSON] et al. (2022)_ [PERSON] [PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] [PERSON]; et al. Process mining for healthcare: Characteristics and challenges. _J. Biomed. Inform._**2022**, _127_, 103994. [CrossRef] [PubMed]
* _[PERSON] (2016)_ [PERSON] The probabilistic model checking landscape. In Proceedings of the 31 st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, NY, USA, 5-8 July 2016; pp. 31-45. * _[PERSON] et al. (2021)_ [PERSON]; [PERSON]; [PERSON]; [PERSON] Probabilistic trace alignment. In Proceedings of the 2021 3 rd International Conference on Process Mining (ICPM), Eindhoven, The Netherlands, 31 October-4 November 2021; pp. 9-16. * _[PERSON] et al. (2022)_ [PERSON]; [PERSON] [PERSON]; [PERSON] Probabilistic model checking of BPMN processes at runtime.