HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs

HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs

Giuseppe De Giacomo, Paolo Felli, Marco Montali, Giuseppe Perelli

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Main Track. Pages 1859-1865. https://doi.org/10.24963/ijcai.2021/256

Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isolation, however, especially in BPM it is also of interest to express properties over the entire log, i.e., properties that relate multiple traces of the log at once. In the case of infinite-traces, HyperLTL has been proposed to express these ``hyper'' properties. In this paper, motivated by BPM, we introduce HyperLDLf, a logic that extends LDLf with the hyper features of HyperLTL. We provide a sound, complete and computationally optimal technique, based on DFAs manipulation, for the model checking problem in the relevant case where the set of traces (i.e., the log) is a regular language. We illustrate how this form of model checking can be used for verifying log of business processes and for advanced forms of process mining.
Keywords:
Knowledge Representation and Reasoning: Action, Change and Causality
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis