HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs
Authors: Giuseppe De Giacomo, Paolo Felli, Marco Montali, Giuseppe Perelli
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, motivated by BPM, we introduce Hyper LDLf, a logic that extends LDLf with the hyper features of Hyper LTL. 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 to specify and verify sophisticated properties within BPM and process mining. The model-checking problem for a Hyper LDLf formula with k alternations of trace quantifiers is k-EXPSPACE-complete. |
| Researcher Affiliation | Academia | Giuseppe De Giacomo,1, Paolo Felli 2, Marco Montali, 2, Giuseppe Perelli 1 1 Sapienza University of Rome 2 Free University of Bozen-Bolzano |
| Pseudocode | Yes | Algorithm 1 Automata construction Automaton( , ). Algorithm 2 Model checking Hyper LDLf over Log DFAs. |
| Open Source Code | No | The paper does not provide any concrete access information for open-source code for the described methodology. |
| Open Datasets | No | The paper is theoretical and does not use datasets in the empirical sense. It refers to "logs" as abstract sets of traces that can be recognized by a DFA, but no specific publicly available datasets are mentioned for training or evaluation. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical experiments with dataset splits for training, validation, or testing. |
| Hardware Specification | No | The paper is theoretical and does not report on empirical experiments. Therefore, no specific hardware specifications for running experiments are provided. |
| Software Dependencies | No | The paper is theoretical and describes a logical framework and algorithms. It does not mention any specific software dependencies with version numbers required to replicate experiments. |
| Experiment Setup | No | The paper is theoretical and does not describe empirical experiments. Therefore, no specific experimental setup details, such as hyperparameters or training configurations, are provided. |