Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2004.01859

Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces

Giuseppe De Giacomo·Riccardo De Masellis·Fabrizio Maria Maggi·Marco Montali
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Giuseppe De Giacomo, Riccardo De Masellis, Fabrizio Maria Maggi, Marco Montali. 2020-04-07. Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces. https://arxiv.org/abs/2004.01859

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Deciding Amalgamation Beyond Arity Two: The Semantic Horn Case

We study the amalgamation decision problem (ADP): given a universal first-order sentence $Φ$, decide whether the class $\mathrm{fm}(Φ)$ of its finite models has the amalgamation property. We call $Φ$ semantic Horn if $\mathrm{fm}(Φ)$ is closed under binary direct products. By McKinsey's theorem, this is equivalent to $Φ$ being logically equivalent to a universal Horn sentence. The distinction concerns the input representation: $Φ$ itself need not be given in Horn form, and converting it into an explicit Horn normal form can incur an exponential blow-up. We prove that the ADP is decidable under this semantic promise. To this end, we associate with $Φ$ a finite-domain CSP template, called its completion template, and a distinguished infinite family of CSP instances, called its atlas instances. The class $\mathrm{fm}(Φ)$ has the amalgamation property precisely when all atlas instances have a solution. For semantic Horn inputs, we prove that the completion template admits a semilattice polymorphism. Consequently, its CSP has bounded width and is decided by a fixed level of local consistency. We introduce uniform contextual strategies, finite certificates expressing this local-consistency condition simultaneously for all atlas instances, and give an effective fixed-point procedure for deciding whether such a certificate exists. The resulting algorithm runs in 2ExpTime in general and in ExpTime under any fixed bound on the arities of the input relations. More generally, the construction gives a decision procedure whenever the associated completion template has bounded width. These bounds are optimal: the semantic Horn ADP is 2ExpTime-complete in general and ExpTime-complete for every fixed arity bound of at least three. Both hardness results already hold for syntactic universal Horn sentences.

cs.LO↗
arXiv2026

Simplified proofs of Weak Normalization for propositional logic

We present a new proof of weak normalization for intuitionistic natural deduction. The distinguishing features of this proof are that it works only with cuts rather than cut segments, provides explicit local rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

cs.LO↗
arXiv2026

A Hybrid Dependency-Aware Framework for Task Decomposition and Dynamic Agent Generation in Oracle-to-PostgreSQL Migration

Large language model (LLM)-based database migration is often treated as direct code transformation, although enterprise Oracle systems contain heterogeneous SQL and PL/SQL artifacts with different dependencies, execution order, complexity, and validation needs. This paper proposes a hybrid dependency-aware framework that identifies migration tasks, builds a cross-file dependency graph, condenses cyclic dependencies, and uses task specifications to generate specialized migration agents at runtime. The deterministic path combines ANTLR-based parsing with typed dependency extraction, while an LLM fallback is invoked only for units that cannot be parsed reliably. On a corpus of 116 Oracle files, the pipeline produced 1,037 units with zero coverage gaps and 1,271 AST-derived dependencies. The fallback processed 165 parse-error units, recovered 496 additional validated dependencies, eliminated unresolved-dependency units, and increased resolved internal edges from 446 to 527. The graph contained four dependency-respecting phases, while cycle handling was validated separately using Tarjan SCC condensation. A complementary experiment on 1,006 PL/SQL files regenerated 623 scripts (~62%), of which 380 (~61%) executed successfully in PostgreSQL 16. Tables achieved about 85% regeneration success, whereas no query regenerations succeeded under the evaluated specification-mediated baseline, and procedural objects remained strongly dependent on schema context. These results motivate dependency-aware context delivery, task-specific validation, and differentiated agent routing. The paper also formalizes task-to-agent mapping, introduces monitoring and diagnostics for execution feedback, and defines a controlled comparison of monolithic, static-decomposition, dependency-aware, and dynamically orchestrated migration strategies.

cs.LO↗