PM2PMC: A Probabilistic Model Checking Approach in Process Mining

The field of process mining is experiencing rapid growth, utilizing data science techniques to analyze business processes and uncover insights about their performance, efficiency, and compliance. The process mining approach begins with process discovery, which involves creating process models based on event logs; and depending on the type of models discovered, the correctness of models needs to be guaranteed. Traditional model checking methods are good approaches to verify the correctness of process models, but those methods cannot model the probabilistic nature of the discovered process models. We define an approach and provides an implementation that enables probabilistic property checking of process mining models. The proposed method extracts a skeleton model by process mining, transforms the extracted model into a formal model, and verifies requirements by a probabilistic model checking technique. The PM2PMC approach has several advantages including its ability to analyze systems with uncertain behavior, ability to identify rare but critical scenarios that may be missed by other techniques like in traditional model checking. In this paper we aim at enriching probabilistic model checking (PMC) by explaining why there is a need of probabilistic verification for process mining models.