# CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version)

arXiv: https://arxiv.org/abs/2103.10507 · HTML: https://mlsanity.com/paper/2103.10507/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 27 references that are in the map.
- First posted on arXiv 18 Mar 2021.

## Builds on (most cited first, 6 of 6)

- [Process Mining for Python (PM4Py): Bridging the Gap Between Process- and Data Science](https://mlsanity.com/paper/1905.06169/) (2019)
- [Conformance Checking Based on Multi-Perspective Declarative Process Models](https://mlsanity.com/paper/1503.04957/) (2015)
- [Petri Nets with Parameterised Data: Modelling and Verification (Extended Version)](https://mlsanity.com/paper/2006.06630/) (2020)
- [A Holistic Approach for Soundness Verification of Decision-Aware Process Models (extended version)](https://mlsanity.com/paper/1804.02316/) (2018)
- [DB-Nets: on The Marriage of Colored Petri Nets and Relational Databases](https://mlsanity.com/paper/1611.03680/) (2016)
- [Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN (Extended Version)](https://mlsanity.com/paper/1906.07811/) (2019)

## Built on by (most cited first, 4 of 4)

- [Conformance Checking with Uncertainty via SMT (Extended Version)](https://mlsanity.com/paper/2206.07461/) (2022)
- [Current and Future Challenges in Knowledge Representation and Reasoning](https://mlsanity.com/paper/2308.04161/) (2023)
- [Data Petri Nets meet Probabilistic Programming (Extended version)](https://mlsanity.com/paper/2406.11883/) (2024)
- [Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended)](https://mlsanity.com/paper/2507.00094/) (2025)

## Abstract (arXiv)

Conformance checking is a key process mining task for comparing the expected behavior captured in a process model and the actual behavior recorded in a log. While this problem has been extensively studied for pure control-flow processes, conformance checking with multi-perspective processes is still at its infancy. In this paper, we attack this challenging problem by considering processes that combine the data and control-flow dimensions. In particular, we adopt data Petri nets (DPNs) as the underlying reference formalism, and show how solid, well-established automated reasoning techniques can be effectively employed for computing conformance metrics and data-aware alignments. We do so by introducing the CoCoMoT (Computing Conformance Modulo Theories) framework, with a fourfold contribution. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case, using SMT as the underlying formal and algorithmic framework. 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 provide a proof-of-concept implementation that uses a state-of-the-art SMT solver and report on preliminary experiments. Finally, we discuss how CoCoMoT directly lends itself to a number of further tasks, like multi- and anti-alignments, log analysis by clustering, and model repair.