Automated simulation and verification of process models discovered by process mining
Ivona Zakarija, Frano \v{S}kopljanac-Ma\v{c}ina, Bruno, Bla\v{s}kovi\'c

TL;DR
This paper introduces an automated framework combining process mining, inductive machine learning, and formal verification techniques to analyze, simulate, and verify process models derived from complex event logs in a hotel PMS environment.
Contribution
It presents a novel integrated approach for automatic transformation of process models into verifiable models and applies formal methods for process analysis and repair.
Findings
Successful application of Spin model checker for process simulation and verification
Effective transformation algorithm for process models into verification models
Use of LTL for specifying system requirements in process verification
Abstract
This paper presents a novel approach for automated analysis of process models discovered using process mining techniques. Process mining explores underlying processes hidden in the event data generated by various devices. Our proposed Inductive machine learning method was used to build business process models based on actual event log data obtained from a hotel's Property Management System (PMS). The PMS can be considered as a Multi Agent System (MAS) because it is integrated with a variety of external systems and IoT devices. Collected event log combines data on guests stay recorded by hotel staff, as well as data streams captured from telephone exchange and other external IoT devices. Next, we performed automated analysis of the discovered process models using formal methods. Spin model checker was used to simulate process model executions and automatically verify the process model.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
