SMT Techniques for Data-Aware Process Mining

Abstract Process mining is witnessing a shift from pure control-flow process models to richer, data-aware process models where the acceptable executions are not only characterised by the process control-flow, but also by the data carried by cases, and how they dynamically interact with the process activities and decisions. Even under the typical assumption that the process control-flow is bounded, the presence of data makes the overall state space infinite, a difficulty that transfers to process analysis and process mining tasks. In this article, we review how the challenges posed by data-aware process mining can be effectively tackled through AI techniques grounded in automated reasoning, and more specifically in Satisfiability and Optimisation Modulo Theories (SMT/OMT). To this end, we discuss data-aware logs and traces merging events with a payload. We then recall Data Petri Nets as an expressive process modelling approach matching this multi-perspective setting, and the logic $$\textsf {data-}{\textsf {LTL}_f}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>data</mml:mi> <mml:mo>-</mml:mo> <mml:msub> <mml:mi>LTL</mml:mi> <mml:mi>f</mml:mi> </mml:msub> </mml:mrow> </mml:math> to formulate correctness properties and to represent declarative process constraints enriched with data. We then summarize how key process analysis and mining tasks can be addressed in this setting using SMT and OMT, with a particular focus on correctness and conformance checking, model repair, and monitoring. We overview the obtained results, presenting them under an integrated lens and providing corresponding pointers to the technical literature. In the conclusion, we outlook open challenges.