Home » Publication » 23502

Dettaglio pubblicazione

2021, IJCAI 2021, Pages 1859-1865

HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs (04b Atto di convegno in volume)

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

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.
© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma