arrow
Return

SMT Techniques for Data-Aware Process Mining

delete2025-04-29
delete0
delete
OA
AI
A
Alessandro Gianola
M
Marco Montali *
S
Sarah Winkler
DOI:10.1007/s13218-025-00890-zdelete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
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 data-LTLf\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textsf {data-}{\textsf {LTL}_f}$$\end{document} 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.
Keywords:
SOUNDNESS
VERIFIER
TOOL

Journal

K
Kunstliche Intelligenz
IF:
3.6
Papers:
29
Citations:
977

Organization

F
Free Univ Bozen Bolzano
Scholars:
139
Papers: 66
Citations: 21
U
Univ Lisbon
Scholars:
1.2K
Papers: 644
Citations: 247
Cited Papers

Cited Papers

Balanced multi-perspective checking of process conformance
err2015-02-20
err146
errOAAI
errMannhardt, Felix; de Leoni, Massimiliano; Reijers, Hajo A.; van der Aalst, Wil M. P.
errShare
errSave
errShare
errSave
Z3: An Efficient SMT Solver
err2008-01-01
err0
PREAI
errLeonardo de Moura; Nikolaj Bjørner
errShare
errSave
errShare
errSave
err
IF0
err
err0
errOAAI
err
errShare
errSave
err
IF0
err
err0
errOAAI
err
errShare
errSave
err
IF0
err
err0
errOAAI
err
errShare
errSave
Computing Unsatisfiable Cores for LTLf Specifications
err2024-06-11
err0
errOAAI
errMarco Roveri; Claudio Di Ciccio; Chiara Di Francescomarino; Chiara Ghidini
errShare
errSave
researcher View more