Data-aware conformance checking with SMT

Paolo Felli, Alessandro Gianola, Marco Montali, Andrey Rivkin, Sarah Winkler*

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

34 Downloads (Pure)

Abstract

Conformance checking is a key process mining task to confront the normative behavior imposed by a process model with the actual behavior recorded in a log. While this problem has been extensively studied for pure control-flow processes, data-aware conformance checking has received comparatively little attention. In this paper, we tackle the conformance checking problem for the challenging scenario of processes that combine data and control-flow dimensions. Concretely, we adopt the formalism of data Petri nets (DPNs) and show how solid, well-established automated reasoning techniques from the area of Satisfiability Modulo Theories (SMT) can be effectively harnessed to compute conformance metrics and optimal data-aware alignments. To this end, we introduce the CoCoMoT (Computing Conformance Modulo Theories) framework, with a fourfold contribution. First, we show how SMT allows to leverage SAT-based encodings for the pure control-flow setting to the data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering, to speed up the computation of conformance checking outputs. Third, we show how our approach extends seamlessly to the more comprehensive conformance checking artifacts of multi- and anti-alignments. Fourth, we describe a proof-of-concept implementation based on state-of-the-art SMT solvers, and report on experiments. Finally, we discuss how CoCoMoT directly lends itself to further process mining tasks like log analysis by clustering and model repair, and the use of SMT facilitates the support of even richer multi-perspective models, where, for example, more expressive DPN guards languages are considered or generic datatypes (other than integers or reals) are employed.

Original languageEnglish
Article number102230
JournalInformation Systems
Volume117
Number of pages19
ISSN0306-4379
DOIs
Publication statusPublished - 2023

Keywords

  • Conformance checking
  • Data Petri nets
  • SMT

Fingerprint

Dive into the research topics of 'Data-aware conformance checking with SMT'. Together they form a unique fingerprint.

Cite this