LTL-based conformance checking of fuzzy event logs

While traditional process mining techniques assume that the event data used for analysis are faithful and complete, the field is increasingly recognizing the need of novel techniques able to accommodate uncertainty on events and the activities they refer to. The vast majority of approaches proposed so far adopts a probabilistic interpretation of uncertainty, where every event comes with a probability distribution on the possible activities. Motivated by scenarios where event data are obtained through event recognition pipelines starting from raw, unstructured data, in this work we argue for the first time for a different interpretation of uncertainty, akin to a fuzzy semantics. Under this interpretation, every event comes with an indication of the “intensity” of execution of each activity. In this novel setting, we study a form of conformance checking where fuzzy events are verified against declarative temporal rules specified using linear temporal logic over finite traces (LTLf), the logic underlying the well-known Declare declarative process specification language. Dealing with fuzzy events requires to relax the assumption that at each instant only one activity is executed, and in turn to adopt a fuzzy semantics for the state formulae of the logic. Technically, we tackle LTL-based conformance checking of fuzzy event logs with a fourfold contribution. First, we introduce a fuzzy counterpart of LTLf tailored to our purpose. Second, we define conformance checking over fuzzy event logs as a verification problem in this logic. Third, we provide an efficient implementation based on the PyTorch Python library, suited to check conformance of multiple fuzzy traces at once. Finally, we show feasibility and scalability through an extensive experimental evaluation.