# Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces

arXiv: https://arxiv.org/abs/2004.01859 · HTML: https://mlsanity.com/paper/2004.01859/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Apr 2020.

## Built on by (most cited first, 7 of 7)

- [Conformance Checking of Fuzzy Logs against Declarative Temporal Specifications](https://mlsanity.com/paper/2406.12078/) (2024)
- [Computing unsatisfiable cores for LTLf specifications](https://mlsanity.com/paper/2203.04834/) (2022)
- [Generating Counterfactual Explanations Under Temporal Constraints](https://mlsanity.com/paper/2503.01792/) (2025)
- [Enjoy the Silence: Analysis of Stochastic Petri Nets with Silent Transitions](https://mlsanity.com/paper/2306.06376/) (2023)
- [Current and Future Challenges in Knowledge Representation and Reasoning](https://mlsanity.com/paper/2308.04161/) (2023)
- [Monitoring Data-aware Temporal Properties (Extended Version)](https://mlsanity.com/paper/2605.14666/) (2026)
- [Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)](https://mlsanity.com/paper/2609.32912/) (2026)

## Abstract (arXiv)

Runtime monitoring is one of the central tasks in the area of operational decision support for business process management. In particular, it helps process executors to check on-the-fly whether a running process instance satisfies business constraints of interest, providing an immediate feedback when deviations occur. We study runtime monitoring of properties expressed in LTL on finite traces (LTLf), and in its extension LDLf. LDLf is a powerful logic that captures all monadic second order logic on finite traces, and that is obtained by combining regular expressions with LTLf, adopting the syntax of propositional dynamic logic (PDL). Interestingly, in spite of its greater expressivity, LDLf has exactly the same computational complexity of LTLf. We show that LDLf is able to declaratively express, in the logic itself, not only the constraints to be monitored, but also the de-facto standard RV-LTL monitors. On the one hand, this enables us to directly employ the standard characterization of LDLf based on finite-state automata to monitor constraints in a fine-grained way. On the other hand, it provides the basis for declaratively expressing sophisticated metaconstraints that predicate on the monitoring state of other constraints, and to check them by relying on standard logical services instead of ad-hoc algorithms. In addition, we devise a direct translation of LDLf formulae into nondeterministic finite-state automata, avoiding to detour to Buchi automata or alternating automata. We then report on how this approach has been effectively implemented using Java to manipulate LDLf formulae and their corresponding monitors, and the well-known ProM process mining suite as underlying operational decision support infrastructure.