Advancing verification of process mining models with quantitative model checking in stochastic environment

Abstract

The study of business process analysis and optimization has attracted significant scholarly interest in the recent past, due to its integral role in boosting organizational 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 identify process-related issues. The goal of the current study is to examine how Quantitative Model Checking (QMC) approaches might be applied in the context of PM. Model checking is a well-known verification approach that provides thorough analysis and validation of a system’s properties in comparison to a predetermined model. The adoption of QMC is aimed at improving the accuracy, reliability, and comprehensiveness of PM models in stochastic environment. We propose a novel methodology in this research direction, which integrates QMC with PM by formally modelling discovered and replayed process models and applying QMC methods to verify PM models. The potential of QMC to overcome significant drawbacks of the existing methodologies is the main driver for its use in PM. By including probabilistic model verification, it is possible to take into account the uncertainties and stochastic behaviour that are frequently present in systems that are used in real world; while statistical model checking methods utilized where probabilistic methods fails/not suitable, such as, to handle complex models and/or models with large state-spaces.

Keywords

• formal verification
• probabilistic model checking
• process mining
• process models
• quantitative model checking
• statistical model checking
• stochastic systems