Conformance Checking of Fuzzy Logs against Declarative Temporal Specifications
Ivan Donadello, Paolo Felli, Craig Innes, Fabrizio Maria Maggi, Marco Montali
TL;DR
The paper tackles uncertainty in event logs by proposing $FLTL_f$, a fuzzy LTL over finite traces, to express declarative temporal constraints such as $\mathsf{G} ((\mathtt{CH} \land \mathtt{HG}) \rightarrow \mathsf{F} (\mathtt{QC}))$. It defines a formal semantics with fuzzy truth values in $[0,1]$, and engineers a tensor-based PyTorch implementation to evaluate formulae across many traces in parallel, supporting $\mathsf{F}$, $\mathsf{G}$, $\mathsf{X}_w$, and $\mathsf{U}_w$. The approach yields scalable conformance checking: complex FLTL_f formulae can be computed in the order of seconds for logs with up to $10^5$ traces each containing $3\times 10^3$ events. This work enables uncertainty-aware conformance checking against declarative temporal specs and suggests paths toward neuro-symbolic integration and Declare-compatible tooling.
Abstract
Traditional conformance checking tasks assume that event data provide a faithful and complete representation of the actual process executions. This assumption has been recently questioned: more and more often events are not traced explicitly, but are instead indirectly obtained as the result of event recognition pipelines, and thus inherently come with uncertainty. In this work, differently from the typical probabilistic interpretation of uncertainty, we consider the relevant case where uncertainty refers to which activity is actually conducted, under a fuzzy semantics. In this novel setting, we consider the problem of checking whether fuzzy event data conform with declarative temporal rules specified as Declare patterns or, more generally, as formulae of linear temporal logic over finite traces (LTLf). This requires to relax the assumption that at each instant only one activity is executed, and to correspondingly redefine boolean operators of the logic with a fuzzy semantics. Specifically, we provide a threefold contribution. First, we define a fuzzy counterpart of LTLf tailored to our purpose. Second, we cast conformance checking over fuzzy logs as a verification problem in this logic. Third, we provide a proof-of-concept, efficient implementation based on the PyTorch Python library, suited to check conformance of multiple fuzzy traces at once.