Conformance Checking with Uncertainty via SMT (Extended Version)

TL;DR

This paper introduces an SMT-based method for conformance checking of uncertain process logs against reference models, accommodating various uncertainties and cost functions, validated through a proof-of-concept implementation.

Contribution

It extends data-aware SMT conformance checking to handle uncertainty in logs, providing a modular and flexible approach for different uncertainty types and tasks.

Findings

Method is correct and feasible

Handles multiple types of uncertainty

Supports various conformance tasks

Abstract

Logs of real-life processes often feature uncertainty pertaining the recorded timestamps, data values, and/or events. We consider the problem of checking conformance of uncertain logs against data-aware reference processes. Specifically, we show how to solve it via SMT encodings, lifting previous work on data-aware SMT-based conformance checking to this more sophisticated setting. Our approach is modular, in that it homogeneously accommodates for different types of uncertainty. Moreover, using appropriate cost functions, different conformance checking tasks can be addressed. We show the correctness of our approach and witness feasibility through a proof-of-concept implementation.