Enhancing Verification and Validation of Process Mining Models under Uncertainty by Quantitative Model Checking Techniques

Process mining is an important sub-field of business process analysis and optimisation and has attracted significant scholarly interest in the recent past. Its purpose is extracting knowledge and insights from event logs of information systems, thereby discovering process models and identifying process-related issues, such as deviations from the standard process, performance bottlenecks, and opportunities for process improvement.

The quality of discovered models is crucial for the reliability of process mining in real-world scenarios. The four basic quality criteria fitness, precision, generalisation and simplicity, are used to evaluate how well the models align with the observed processes. Conformance checking is a more sophisticate process to validate whether the event logs conform to the model. Model checking, as an extrinsic approach to process mining, has also been utilised to formally verify the correctness of the discovered models as well as their compliance with pre-defined requirements. Model checking can confirm whether the model satisfies a broad range of temporal properties, for example, “in a loan application every invoice received must be followed by a payment process initiation within 30 days”.

Real-world business operations are surrounded by uncertainty. The discovered models from process mining inherently exhibit stochastic characteristics since they are derived from event logs of business operations. Therefore, it is essential to understand the model performance in stochastic environments. This motivates the employment of quantitative model checking (QMC), a collection of techniques extending the classical model checking, to verify the models against temporal properties, such as “what is the probability that every invoice received is followed by a payment process initiation within 30 days?”.