Proceedings

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

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

Download BibTeX Cite

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 1859-1865.

https://doi.org/10.24963/ijcai.2021/256

Keywords

  • Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
  • Knowledge Representation and Reasoning: Action, Change and Causality

Abstract

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.

Giuseppe De Giacomo, Paolo Felli, Marco Montali, and Giuseppe Perelli. 2021. HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 1859–1865. https://doi.org/10.24963/ijcai.2021/256
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards