Monitoring Data-aware Temporal Properties

1 Introduction

Complex, dynamic AI systems increasingly comprise autonomous agents and heterogeneous components with unknown, inaccessible, or opaque internal specifications. This hampers the possibility of ascertaining their safety and trustworthiness through traditional design-time verification methods such as model checking and testing. A remedy in such situations is to keep track of desired properties at runtime, by monitoring the executions of the black-box system under scrutiny. A widely known, solid approach to monitoring is that of runtime verification (RV), where given a logical property, a corresponding monitor can be automatically constructed, with the guarantee that it will emit a provably correct verdict [Leucker and Schallhart, 2009]. These advantages have fostered the application of RV in various AI contexts, including multiagent systems [Dastani et al., 2018; Alechina et al., 2018], robotics [Begemann et al., 2023], cyber-physical systems [Tracy et al., 2020], and business processes [Ly et al., 2015; Calvanese et al., 2022a]. The vast majority of such approaches specify properties using variants of linear-time temporal logic (LTL).

Leucker and Schallhart (2009) point out two key insights in monitoring: First, since the trace τ seen so far is necessarily of finite length, this calls for a finite-trace semantics for LTL. However, as the system evolves, τ is only the prefix of a (yet unknown) continuation. Different variants of LTL then have to be studied depending on whether such a continuation eventually terminates, or continues forever. In many AI-relevant settings (e.g., planning and business processes [Bacchus and Kabanza, 2000; Baier et al., 2009; De Giacomo and Vardi, 2013; De Giacomo et al., 2014]) the monitored system operates for an unbounded, yet finite, number of steps. This means that also each one of the (infinitely many) possible suffixes of τ has a finite length, making LTLf (LTL over finite traces [De Giacomo and Vardi, 2013]) a natural candidate logic for monitoring [De Giacomo et al., 2020; De Giacomo et al., 2022; Calvanese et al., 2022a].

A key limitation of many of these approaches is that propositional LTLf cannot express properties about structured data. However, such properties are ubiquitous in AI systems, as witnessed by the new agentic wave, where agents executing business tasks and processes have to deal with different types of structured data, such as numbers with arithmetic, sets, lists, and uninterpreted functions. Recently, Geatti et al. (2022) brought forward LTLf modulo theories (LTLMT f ) to enrich LTLf with the full spectrum of theories supported by state-of-the-art SMT [Barrett et al., 2021] solvers, which include all the datatypes mentioned before. The following example illustrates the need for such rich properties:

Example 1. Consider an online marketplace for concert tickets. A buyer agent dynamically receives ticket offers, and is tasked by its human principal with the goal of selecting the best offer (that is, the ticket with the lowest price) for a given concert (indicated by constant myc below). Every ticket has two properties: its price, and the concert it refers to.

Formally, this setting is captured by three datatypes Ticket, Concert (with myc∈Concert), and the real numbers R, a dedicated constant undef of type Ticket and functions price: Ticket → R and con: Ticket → Concert that resp. assign to each ticket its price and the concert it is for. Such two functions conceptually model a database table with three columns, where each record stores a ticket id (primary key) with its price and concert. The agent should select the cheapest ticket. An execution consists of a trace where at each time step the values of two variables of type Ticket are specified: t, the ticket currently offered by the marketplace; and b, the ticket currently bookmarked by the agent.

Since the agent specification is not accessible, its human principal wants to formalise the expected behavior and check whether the agent indeed adheres to it. To this end, the principal constructs a suitable LTLMT f formula composed of different parts. The first part ψchange captures the situation where the bookmarked ticket must be changed to the currently received one, because it has a lower price. The notation ◁b is used here to refer to the previous value of variable b, i.e., the value b held in the instant before the current one. With this notation at hand, we set ψchange as

con(t) = myc ∧ (◁b = undef ∨ price(t) < price(◁b)) → b = t Next, the formula ψkeep deals with the case where the bookmarked ticket is kept, since the currently received ticket either refers to a concert of no interest, or has a higher price than the bookmarked one. Formally, ψkeep is given by

(con(t) ̸= myc∨(◁b ̸= undef∧price(t)> price(◁b))) → b=◁b To bundle everything together, we assume for simplicity that the ticket stream starts at the second instant. We can hence require that b is initially undef, while the formulae ψkeep and ψchange must hold in every instant of the trace, starting from the next one. 1 The latter condition is captured using the LTLf operators X and G, yielding

Differently from the simpler settings of propositional LTLf [De Giacomo et al., 2022], or of LTLf extended with numerical variables [Felli et al., 2023], where a trace is simply a sequence of assignments, dealing with LTLMT f also requires to keep track of a first-order model M. In Ex. 1, this corresponds to the set of tickets seen in the trace, as well as their prices and concerts. Therefore, different interpretations of the monitoring problem are conceivable: the model underlying a trace can be considered as fixed, or it may be assumed to change in every step. In this work, we adopt the following: given a trace τ with model M, a continuation of τ provides an extension of M - a notion that we later anchor precisely to the model-theoretic concept of embeddings. This interpretation has the following advantages: (1) the current model, dealing with the trace seen so far, is extended only conservatively, in that facts concerning the previous elements must be kept throughout the trace, and no new fact concerning those elements can be added, but (2) in continuations of the trace, new elements may appear, along with additional facts involving these. This is fully in par with the expected interpretation of settings like that of Ex. 1, where the prices and referred concerts of tickets seen in the past are fixed, while new information on unseen tickets can be acquired later.

1 We assume for simplicity that if a ticket with the same price appears, the agent keeps the one already bookmarked.

Leucker and Schallhart (2009) also emphasize another central monitoring desideratum, namely the identification of violations in the earliest possible instant, which in turn calls for anticipatory monitors [Bartocci et al., 2018]. These monitors return their verdict not only considering the prefix seen so far, but also by reasoning on all its (infinitely many) possible suffixes. The next example makes a clear case for this.

Example 2. Consider formula ψ from Ex. 1. Monitoring ψ essentially amounts to check, at every instant, whether the expected relationship between b and t holds. Consider now

It expresses that at some point the agent selection stabilizes 2 to the ticket identified by t123. A monitor checking only the trace prefix seen so far would detect a violation of ψt123 only if ψ is violated, or at the end of the trace if the selected ticket is not t123. However, note that the price of ticket t123 must be known, say price(t123) = 100, and due to the behaviour of the agent, it is clear that t123 will never be selected as soon as the agent finds a ticket with a price below 100 euros. In this respect, an anticipatory monitor for ψt123 would immediately recognize that ψt123 is permanently violated (i.e., it will stay so independently on how the trace evolves) if in the current instant b points to a ticket with a price < 100.

In this paper, we tackle for the first time anticipatory monitoring described in Ex. 2. In fact, anticipatory monitoring for LTLMT f is a completely open problem. It is indeed a challenging one, as already in the case where LTLf is equipped with numeric datatypes with simple forms of arithmetic, it incurs in undecidability [Felli et al., 2023], and therefore relevant monitorable fragments of the logic have to be singled out. We bring a fourfold contribution: (1) We formally introduce the anticipatory monitoring problem for LTLMT f specifications. (2) We focus on the quantifier-free fragment of LTLMT f , an expressive logic called dataLTLf that has been previously studied for process analysis [Gianola et al., 2025] and verification [Gianola et al., 2024] tasks, but never for monitoring. We provide a monitoring technique that combines an automata-theoretic component to deal with the temporal dimension, with an SMT component to tackle the data part. (3) We identify expressive classes of properties combining arithmetic with references to a database, in the style of Ex. 1, where we show that our monitoring task becomes effectively solvable. (4) Feasibility of our method is witnessed by a prototype implementation with preliminary evaluation. Some additional material can be found in an extended version [Gianola et al., 2026].

Related work A rich body of work studies RV of arithmetic temporal properties, notably Lola [D'Angelo et al., 2005] (which also supports anticipation [Hipler et al., 2024]), TeSSLa [Kallwies et al., 2022], and Eagle [Goldberg and Havelund, 2005]. From [Felli et al., 2023], which considers anticipatory monitoring for LTLf with arithmetic. We borrow in the present work the idea to abstract variable configurations by sets of formulae arranged in a graph, and the resulting approach to identify decidable fragments. However, dealing with richer theories substantially changes both the setting and the techniques needed to construct monitors.

2 This is captured by the LTLf operators F and G, where FGγ models that there exists an instant from which γ always holds; it is known that, over finite traces, this is logically equivalent to γ holding in the last instant of the trace [De Giacomo and Vardi, 2013].

Decker et al. (2016) propose an approach for monitoring modulo theories, but use an incomparable logic where variables cannot be compared across states, and models change at each trace instant. In Ex. 1, this would essentially mean that the price and referred concert of already seen tickets non-deterministically change at every instant. Also, no decidable fragments are identified. In another line of work [Schneider et al., 2021; Basin et al., 2015; Lima et al., 2024], monitoring with metric first-order temporal logic is considered, but in the non-anticipatory setting. Havelund et al. (2020) present a monitoring approach for first-order past time temporal logic without anticipation. This work shares with the present paper that infinitely many assignments are represented by logical formulas, in this case by BDDs. However, in both [Havelund et al., 2020; Basin et al., 2015] the model is supposed to change at every instant, as predicates model events rather than facts.

The logic dataLTLf we consider here has previously been studied for process analysis and verification. Specifically, [Gianola et al., 2024] verifies data-aware dynamic systems against dataLTLf properties, using automata-based techniques that are however too weak to be ported to monitoring.

2 Preliminaries

LTLMT f syntax. We consider a first-order multi-sorted signature Σ = ⟨S,P,F, V,U⟩, where S is a set of sorts; P is a set of predicate and F a set of function symbols over S; V is a set of data variables; and U is a set of variables disjoint from V that will be used for quantification; where all variables have a sort in S. below, we consider a fixed signature Σ that contains equality predicates for all sorts in S.

A term t is generated by the following grammar:

where x ∈ V and y ∈ U are variables, f ∈ F is a function symbol of arity k, each ti, 1 ≤ i ≤ k, is a term, and ◁ is the previous constructor. The grammar of LTLMT f formulas over Σ is the following:

where y ∈ U, p ∈ P is an k-ary predicate symbol, each ti is a term, and X, Xw, U, and R are the next, weak next, until, and release temporal operators, respectively. Formulas of type φ as defined above are called first-order (FO) formulas. In the definition of ψ, we force φ to have no free variables from U. We use the usual shortcuts Fψ ≡ ⊤ U ψ and Gψ ≡ ⊥ R ψ. By the grammar above, LTLMT f formulas are always in negation normal form, and we assume them to be well-typed with regard to the sorts of all the involved symbols. The set of all LTLMT f formulas is denoted L.

For instance, ψ and ψt123 in Ex. 1 are LTLMT f formulas over the signature where V = {t, b}, there are no quantified variables so U can be chosen empty, P contains the arithmetic predicates, and F consists of arithmetic functions, equality, price, concert, undef, myc, and t123.

A FO formula φ is a state formula if it does neither contain free variables from U nor ◁ operators. A state formula without free variables is a sentence, and a set of sentences is a Σ-theory T . It is universal if all its sentences are over Σ and have the form ∀u1, . . . , ul. ψ with ψ quantifier-free.

LTLMT f semantics. To define semantics, we use the standard notion of a Σ-structure M, which associates each sort s ∈ S with a domain sM , and each predicate p ∈ P and function symbol f ∈ F with a suitable interpretation pM and f M . The equality predicates have the standard interpretation given by the identity relation. The carrier of M, i.e., the union of all domains of sorts in S, is denoted by |M|. A total function α: V → |M| is called a state variable assignment. We always assume that variables are mapped to an element of their respective domain. A trace τ = (M, ⟨α0, . . . , αn-1⟩) consists of a model M and a sequence of state variable assignments αi with codomain |M|. We call n the length of τ, denoted |τ|. For two traces τ = (M, ⟨α0, . . . , αn⟩) and τ ′ = (M ′ , ⟨α′0 , . . . , α′m⟩) with M = M ′ , their concatenation is given by τ · τ ′ := (M, ⟨α0, . . . , αn, α′0 , . . . , α′m⟩).

Given a trace τ = (M, ⟨α0, . . . , αn-1⟩), and a variable evaluation function ξ : U → |M| for the variables in U, the evaluation [t]iτ,ξ of a term t is well-defined if i < |τ|, and either i > 0 or t does not contain ◁ operators, namely as

where v ∈ V and u ∈ U. Satisfaction of a first-order formula φ with respect to an environment ξ in the run τ with i < |τ|, denoted τ |=iξ φ, is defined as:

where y is assumed to have sort s, and e is in the domain for s in |M|. Satisfaction w.r.t. τ is extended to a general LTLMT f formula ψ as follows:

Finally, τ satisfies ψ, denoted by τ |= ψ, if τ |=0 ψ holds.

Example 3. For φ from Ex. 1, consider a model M where Concert M = {c0, c1, c2, c3}, mycM = c1, Ticket has carrier {⊥, t1, t2, . . . , t1000}, undefM = ⊥, with an interpretation that satisfies con(t2) = con(t4) = con(t5) = c1 and con(t1) = c2, price(t2) = 100, and price(t4) = 110, price(t5) = 95. Then the trace (M, α) satisfies φ, where

Our logic differs from [Geatti et al., 2022] in two respects: we define LTLMT f with a lookback operator ◁ instead of lookahead, i.e., the logic allows to refer to values of V in the previous trace instant, not in the next. However, every formula with lookahead can be equivalently expressed with lookback [Felli et al., 2023, Lem. 37]. Moreover, we have the strong version of the cross-state operator (but not its weaker version), so that atoms with not well-defined terms are false.

First-order logic. Next, we need to repeat some preliminaries from FO logic and model theory. If φ is a state formula, we simply write M, α |= φ instead of ⟨(M, α)⟩ |=i∅ φ, and if φ is a sentence, we write M |= φ for M, ∅ |=0∅ φ. We adopt a common SMT perspective and view a Σ-theory T as the set of all Σ-structures that satisfy all axioms of T , and write M ∈ T if M is a model of T , i.e., M |= φ holds for all sentences φ in T . A state formula φ is T -satisfiable if there is some M ∈ T and state variable assignment α: V → |M| such that M, α |= φ; whereas φ is T -valid if M, α |= φ for all M ∈ T and α. Moreover, formulas φ1 and φ2 are T -equivalent, denoted φ1 ≡T φ2, if φ1 ↔ φ2 is T -valid.

A Σ-theory T has quantifier elimination (QE) if for every Σ-formula φ there is a quantifier-free formula φ′ that is T -equivalent to φ. As QE is a strong requirement, we exploit in this paper the weaker notion of a theory having a model completion. In this context, an embedding is a mapping µ: M →M ′ between two Σ-structures M and M ′ that preserves the truth of Σ-literals. It is easy to see that a composition of embeddings is again an embedding. A universal Σ-theory T has model completion [Ghilardi, 2004] iff there exists a Σ-theory T ∗ , i.e., a theory over the same signature, where T ∗ ⊇ T , such that (i) every model of T can be embedded in a model of T ∗ , and (ii) T ∗ has QE.

It follows from this definition that every model of T ∗ can be embedded in a model of T . We will later exploit the following properties [Calvanese et al., 2020b, Sec. 2]:

Lemma 4. Let T have model completion T ∗ .

1. Let M ∈ T , φ be an existential Σ-formula and α an assignment of values in M such that M, α |= φ. Then there is an embedding µ: M →M ′ for some M ′ ∈ T ∗ such that M ′ , µ ◦ α |= φ.
2. Let M ∈ T , M ′ ∈ T ∗ , µ: M →M ′ be an embedding, φ a quantifier-free Σ-formula, and α be an assignment of values inM. If M ′ , µ ◦ α |= φ thenM, α |= φ.

For a trace τ = (M, ⟨α0, . . . , αn-1⟩) and an embedding µ: M →M ′ , let µ(τ) = (M ′ , ⟨µ ◦ α0, . . . , µ ◦ αn⟩).

We will sometimes refer to common SMT theories [Barrett et al., 2021]: the theory of equality and uninterpreted functions (EUF) for a given Σ, and linear arithmetic over rationals (LRA), integers (LIA), or both (LIRA). While the arithmetic theories have QE [Presburger, 1929], EUF admits model completion and so do certain tame combinations of LIRA and EUF [Calvanese et al., 2020a; Calvanese et al., 2022b]. In the remainder, we make the following assumptions on the theory:

Assumptions 5. (a) Satisfiability of existential T -formulas is decidable; (b) T is either universal and has a model completion T ∗ ; or has QE, in this case let T ∗ :=T .

We will show later that these assumptions are satisfied by several theories which are highly relevant in practice.

Monitoring. We now define our main task, namely determining how the satisfaction of a given property changes along a trace. Throughout the paper, we consider anticipatory monitoring, taking into account both the trace seen so far and all its finite future continuations. Following the literature [Bauer et al., 2010], we consider the set RV = {PS, CS, CV, PV} of four distinct monitoring states: current satisfaction (CS), permanent satisfaction (PS), current violation (CV) and permanent violation (PV). We call a trace τ ′ is an extension of a trace τ = (M, ⟨α0, . . . , αn-1⟩) if there is some M ′ such that there is an embedding µ: M →M ′ and assignments α′i such that τ ′ = (M ′ , ⟨µ(α0), . . . , µ(αn), α′0 , . . . , α′m⟩).

Definition 6. An LTLMT f property ψ is in monitoring state s ∈ RV after a trace τ , written τ |= [[ψ = s]], if

• s = CS, τ |= ψ but τ ′ ̸|= ψ for some extension τ ′ of τ;
• s = PS, τ |= ψ, and τ ′ |= ψ for every extension τ ′ of τ;
• s = CV, τ ̸|= ψ but τ ′ |= ψ for some extension τ ′ of τ;
• s = PV, τ ̸|= ψ, and τ ′ ̸|= ψ for every extension τ ′ of τ.

After each trace, a property ψ is in exactly one possible monitoring state. E.g. for the trace τ from Ex. 3 and ψ, ψt123 from Ex. 1 we have τ |= [[ψ = CS]]: the property is currently satisfied but could be violated in an extension of τ. Considering ψt123, let t123M = t123. If we have price(t123) = 80 then τ |= [[ψt123 = CV]] as t123 could still be selected in the future; but if price(t123) = 100 then τ |= [[ψt123 = PV]].

Given τ and ψ, the monitoring problem is to compute the state s ∈ RV s.t. τ |= [[ψ = s]]. It is solvable if one can construct a procedure for ψ that computes the monitoring state for any given trace. It is known that the monitoring problem is not solvable if T is the theory of linear arithmetic over the reals [Felli et al., 2023], and hence also not for the much more general logic LTLMT f .

3 Automata for Properties

In the remainder of the paper we assume a theory T that satisfies Assumptions 5, and the quantifier-free fragment of LTLMT f , that is, the logic dataLTLf from [Gianola et al., 2025; Gianola et al., 2024]. Excluding quantifiers is here an essential restriction when applying reasoning with model completion to the automaton, which is needed to construct the monitors. As e.g. shown in Ex. 1, dataLTLf still supports expressive queries over the theories, provided that they are formulated referring to the monitored variables.

It is well-known that LTLf properties can be captured by non-deterministic automata (NFA) [De Giacomo and Vardi, 2013]. Our monitoring approach relies on such an NFA for a given LTLMT f property ψ. While the construction is rather standard, the correctness proofs are more complicated due to the FO setting. We only sketch here our construction, details and proofs can be found in [Gianola et al., 2026]. Let λ be an additional proposition to mark the last element of a trace. Given a dataLTLf property ψ, let C be the set of FO formulas in ψ and C ± = C ∪{¬c | c ∈C} the set of FO formulas in ψ together with their negations. The alphabet of the NFA will be Θ = 2C±∪{λ,¬λ} , so that a symbol is a set of FO formulas.

The NFA Nψ is built using an auxiliary function δ, which has as input a property ψ ∈ L ∪ {⊤,⊥} and outputs a set of pairs (ψ′ , ς) where ψ′ ∈ L ∪ {⊤,⊥} is again a property and ς ∈ Θ. Intuitively, (ψ′ , ς) ∈ δ(ψ) means that a word ςw satisfies ψ iff the suffix w satisfies ψ′ , for its definition see [Gianola et al., 2026]. Nψ is then defined as follows:

Definition 7. Given a property ψ ∈ L, let Nψ =(Q,Θ, ϱ, q0,QF ) where q0 =ψ is the initial state, QF = {⊤, q+} is the subset of final states, q- is an additional non-final state, and Q, ϱ are the smallest sets such that q0, qF , q+, q- ∈ Q and whenever q ∈ Q \ {q+, q-} and (q′ , ς) ∈ δ(q) then q′ ∈ Q and

• (i) if λ ̸∈ ς then (q, ς, q′ ) ∈ ϱ, and
• (ii) whenever λ ∈ ς, if q′ = ⊤ then (q, ς, q+) ∈ ϱ, and if q′ = ⊥ then (q, ς \ {λ}, q-) ∈ ϱ.

Example 8. Consider ψ from Ex. 1. We abbreviate A := (b = undef), B := (con(t) = myc), C := (price(t) > price(◁b)), D := (b = t), E := (b = ◁b), and φ′ := G(φchange ∧ φkeep). Then the NFA Nψ is as follows:

We denote by V ◁ the set of variables V ◁={◁v | v ∈V }. A word w = ς0, ς1, . . . , ςn-1 ∈ Θ+ is well-formed if ς0 contains no variable in V ◁. We next define the notion of consistency, which serves to capture that a trace τ satisfies all formulas in a word w∈Θ+ as above. To that end, for assignments α and α′ with domain V , we define the assignment [α⊛α′ ] with domain V ◁ ∪ V as [α⊛α′ ](◁v) = α(v) and [α⊛α′ ](v) = α′ (v), for all v ∈ V . For simplicity, we write M, α |= ς instead of M, α |= ∧ ς.

Definition 9. A well-formed word ς0, ς1, . . . , ςn-1 ∈ Θ+ is consistent with a trace (M, ⟨α0, . . . , αn-1⟩) if M, α0 |= ς0 and M, [αi-1 ⊛αi] |= ςi for all 0 < i < n, and moreover λ ∈ ςn-1, and ¬λ ∈ ςi for all 0 ≤ i < n - 1.

To state the main result about the NFA Nψ below, we need to restrict to properties that use lookback in a valid way, i.e., that do not enforce constraints with lookback variables in the first trace instant. To that end, let an dataLTLf property ψ have safe lookback if no edge from the initial state has a label that contains V ◁. The following is the main result about Nψ:

Theorem 10. Given ψ∈L with safe lookback and trace τ, (1) if Nψ accepts a well-formed word w ∈Θ+ consistent with

τ, then τ |= ψ, and (2) if τ |= ψ then there exists a wellformed word w ∈Θ+ consistent with τ and accepted by Nψ.

For w = ς0, . . . , ςn-1, we write q0 w -→ qn if there is a sequence of states q1, . . . , qn-1 such that (qi, ςi, qi+1) ∈ ϱ for all 0 ≤ i < n. We have the following determinism property:

Lemma 11. Given a trace τ there are a unique word w∈Θ∗ and state q s.t. q0 w -→ q in Nψ and w is consistent with τ .

Note that while it is possible to postprocess Nψ to an NFA for ψ that does not mention λ [Felli et al., 2023], the resulting automaton requires an explicit determinization step to obtain a property akin to Lem. 11, so we prefer to keep the λ's.

4 Monitoring Technique

We next present our monitoring algorithm. Throughout this section, we assume a dataLTLf property ψ with NFA Nψ = (Q, Θ, ϱ, q0, QF ) as defined in the previous section.

For a formula φ with free variables V , let φ(V /X) denote the formula where V is replaced by X (we denote by V a fixed ordering of V as a vector). For a set of constraints C with free variables V ◁ ∪ V , let C(X/V ◁, Y /V ) denote the constraints where V ◁ is replaced by X and V by Y . Moreover, for a set of constraints C ∈ Θ, we denote by [C] its conjunction where λs are omitted, i.e., [C] = ∧ C \ {λ, ¬λ}; so [C] is a formula with free variables V ◁ ∪ V .

Definition 12. For a state formula φ and C∈Θ, let regress(φ, C) = ∃Y .[C](V /V ◁, Y /V ) ∧ φ(Y /V ), where Y is a set of fresh variables of the same size and sorts as V .

Note that since φ has free variables V , also regress(φ, C) has free variables V . The regress operation defined above allows us to "propagate backwards" the verification obligation expressed by φ through the constraint C: in formal verification, this corresponds to the classic notion of preimage when performing backward search in a transition system, cf. e.g. [Abdulla et al., 1996]. We collect these verification obligations in a structure called coreachability graph, which is one of the technical novelties of this paper, defined next:

Definition 13. Given NFA Nψ for ψ, the coreachability graph CG+(Nψ) for Nψ is a tuple ⟨S, γ⟩ where S is a set of nodes of the form (q, φ) for q ∈ Q and φ a quantifier-free Σ-formula with free variables V , and γ ⊆ S × Θ × S is a transition relation. It is inductively defined as follows:

• (i) for all final states q ∈ QF , a node (q,⊤) ∈ S, and
• (ii) if s ∈ S is of the forms = (q, φ) and there is a transition q′ ς-→ q in Nψ such that regress(φ, ς) is T -satisfiable, there is some node s′ = (q′ , φ′ ) ∈ S such that φ′ ≡T ∗ regress(φ, ς), and s′ ς-→ s is in γ.

Note that we use model completion to obtain quantifierfree formulas, which is the main technical novelty of our approach; the fact that all formulas in CGs are quantifier-free allows us to identify decidable fragments in the next section. Note that as regress(φ, ς) is existential, by Assumptions 5 some quantifier-free χ s.t. χ ≡T ∗ regress(φ, ς) indeed exists, by applying quantifier elimination in T ∗ .

Intuitively, if CG+(Nψ) has a node (q, φ) then this means that from NFA state q a final state can be reached under the condition that the current variable assignment satisfies φ. It is called 'coreachability graph' because it is is constructed by regressing from the final states of the system, rather than by forward exploration from the initial states as customary in standard reachability graphs [Desel and Esparza, 1993; Chiola et al., 1997]. The non-coreachability graph CG-(Nψ) is defined dually, but where in condition (i) of Def. 13 we have (q, ⊤) ∈ S for all q ∈ Q \ QF .

The construction in Def. 13 need not terminate as infinitely many formulas may occur, but we will show in the next section that termination is guaranteed for several relevant classes of properties. For cases where CG+(Nψ) and CG-(Nψ) are finite, we define the following formulas which express, intuitively, under which conditions a final (resp. non-final) state is reachable from state q in the NFA.

This leads to the following monitoring procedure, where the trace τ is assumed to have positive length:

• 1: procedure MONITOR(ψ, τ)
• 2: compute Nψ
• 3: q ← state in Nψ such that q0 →∗w q for some wellformed w ∈ Θ∗ consistent with τ ▷ cf. Lem. 11
• 4: let M be the model of τ and αn its last assignment
• 5: if q is accepting in Nψ then
• 6: return CS if M, αn |= EXTVIOL(q) else PS
• 7: else return CV if M, αn |= EXTSAT(q) else PV

Thanks to Thm. 10, Line 5 is equivalent to checking whether the property ψ holds on the prefix τ. If so, the possible monitoring states are restricted to CS and PS; therefore, in Line 7 it suffices to check whether the extension leads to a violation, which is achieved by checking whether αn satisfies EXTVIOL(q). If τ does not satisfy ψ, dual reasoning applies.

The NFA, CGs, and formulas EXTSAT and EXTVIOL should only be computed when required but can be cached for later use, to avoid re-computation. This is especially useful when monitoring multiple traces w.r.t. the same property.

Correctness. To prove correctness, we need some additional notation. First of all, regression constraints are formulas obtained from nested regress operations:

Definition 15. For w=ς0, . . . , ςn-1 in Θ∗ , the regression constraint RC(w) is given by RC(w) = ⊤ if n = 0, and if n>0 then RC(w) = regress(RC(⟨ς1, . . . , ςn-1⟩), ς0).

Crucial for our verification technique is the fact that there is a correspondence between satisfying assignments of RC(w), and traces that satisfy the verification obligations given by the constraints in w, as stated next:

Lemma 16. For w∈Θ∗ , a model M and assignment α, (1) if M, α |=RC(w) there is a trace τ with model M s.t. ⟨∅⟩ · w is consistent with (M, ⟨α⟩) · τ, and (2) if ⟨∅⟩ ·w is consistent with some (M, ⟨α⟩) · τ then M, α |= RC(w).

There is a close relationship between paths in CGs and regression constraints, as stated in the next lemma. For a word w=ς1, . . . , ςn, we write (q, φ) →∗w (q′ ,⊤) if there is a path (q, φ) ς1 -→ . . . · · · ςn -→ (q′ , ⊤) in CG+(Nψ) or CG-(Nψ).

Lemma 17. Let G be CG+(Nψ) (resp. CG-(Nψ)).

1. If G has a path (q, φ) →∗w (qf ,⊤) then q →∗w qf in Nψ such that qf is a final (resp. non-final) state, φ is T -satisfiable, and φ ≡T ∗ RC(w).
2. If q →∗w qf in Nψ such that qf is final (resp. non-final), and RC(w) is T -satisfiable, there is a path (q, φ) →∗w (qf , ⊤) in G for some φ such that φ ≡T ∗ RC(w).

At this point we are ready to prove our main theorem, which strongly exploits the two properties of model completions: embeddability of T - models into T ∗ -models, and QE in T ∗ . The proof can be found in [Gianola et al., 2026].

Theorem 18. If MONITOR(ψ, τ) returns s then τ |=[[ψ=s]].

5 Solvability Criteria

In this section, we identify classes of dataLTLf properties where MONITOR is guaranteed to terminate; we use the terminology that the monitoring task is solvable in this case. We focus on properties that combine references to a database with arithmetic, a combination that is very common in practice, in particular in data-aware BPM [Ghilardi et al., 2023] and when observing database-driven systems [Boja´nczyk et al., 2013; Calvanese et al., 2013; Deutsch et al., 2018];

To define databases in a symbolical context, we rely on the notion of static DB schemas from [Ghilardi et al., 2023], where relational databases with integer and real values are formalized in an algebraic way. Static DB schemas use the combination of two FO theories, Tdb and Tar. The theory Tdb models read-only DB relations with primary and foreign key constraints by employing function symbols to represent the key dependencies: formally, this can be captured in SMT via constants and functions subject to multi-sorted EUF, as done in our ticketing Ex. 1. The theory Tar is LIA, LRA or their combination; it is used to formalize arithmetic constraints.

DB-driven theories Let a DB-LTLf property be a property in LTLMT f where the signatureΣconsists of arbitrary relation, and unary function symbols. The associated theory Tdb is defined as EUF, possibly extended with a set of ground facts to model an initial DB. This theory enjoys model completion [Calvanese et al., 2020b]. In the case with arithmetic, Σ supports in addition operations from an arithmetic theory Tar as above, and its theory is T := Tdb ∪ Tar. To ensure that T has model completion, we assume that the signature is tame, which intuitively means that no uninterpreted function symbol has an arithmetic domain (see below).

Note that the presence of only finitely many terms guarantees that the procedure MONITOR always terminates. However, in general both the DB and the arithmetic perspective can give rise to infinitely many terms, so in classes of properties where the monitoring task is solvable, both must be suitably restricted. Next, we explore different ways to do so.

I. Acyclic signature. First, we consider DB-LTLf without arithmetic. Acyclicity of the signature Σ is defined via the sort graph of Σ, which has as node set the sorts S, and an edge from s to s′ iff there is a function symbol f : s → s′ in Σ (as we have only unary functions); we say that Σ is acyclic if the sort graph is so. For instance, the non-arithmetic part of the signature of Ex. 1 is acyclic. In this case, only finitely many Σ-terms exist [Abadi et al., 2010]. Thus, there are also only finitely many non-equivalent quantifier-free formulas over the finite set of variables V [Calvanese et al., 2020b]. and hence there are only finitely many regression constraints, so that the coreachability graph construction in Def. 13 terminates. Hence, we obtain the following decidability result:

Theorem 19. If Σ is acyclic, the monitoring task for DBLTLf is solvable.

II. Acyclic signature and monotonicity constraints. Next, we consider DB-LTLf with arithmetic. To obtain decidability, we make multiple restrictions. First, we assume that the signature Σ is tame, i.e., in the sort graph of Σ, sorts rat and int are leaves. In this case, the combined theory T is known to enjoy model completion [Calvanese et al., 2022b, Thm. 7]. Second, we require that Σ is acyclic. Third, we restrict arithmetic constraints to monotonicity constraints (MCs), i.e., constraints of the form t ⊙ t′ where t, t′ are Σ-terms of sort rat over free variables V and ⊙ is one of =, ̸=, ≤, or <. MCs have been repeatedly considered in the verification literature [Demri and D'Souza, 2007; Felli et al., 2019] and are important in BPM since transition guards of this shape can be learned automatically from data [de Leoni and van der Aalst, 2013]. We call the class of properties that adhere to these restrictions DB-LTLf -MC. For instance, the properties of Ex. 1 are in this class. We obtain the following result, subsuming [Felli et al., 2023, Thm. 20]:

Theorem 20. The monitoring task is solvable for DB-LTLf - MC properties.

Proof (idea). As shown in [Gianola et al., 2024], under the assumptions of tame signature and MCs, the procedure TameCombCover [Calvanese et al., 2022b, Sec. 8] has finitely many possible results of the form φ1(X) ∧ φ2(Y , t(X)), up to equivalence. Hence there are finitely many regression constraints up to equivalence, so the coreachability graph construction in Def. 13 terminates.

III. Local Finiteness. Next, we consider decidability beyond acyclic signatures for DB-LTLf without arithmetic, using the concept of local finiteness [Lipparini, 1982]. A Σtheory T is called k-locally finite, for some k∈N, if for every finite set of variables X, the number of Σ-terms with free variables X is upper-bounded by k, up to T -equivalence. As local finiteness directly ensures that there are only finitely many non-equivalent quantifier-free formulas in T ∗ , we get:

Theorem 21. If T is a k-locally finite Σ-theory that admits model completion, the monitoring task is solvable for any property ψ over Σ.

One way to ensure in Thm. 21 that T has a model completion is to restrict axioms in T to single-variable sentences [Calvanese et al., 2020b]:

Corollary 22. The monitoring task is solvable for a DBLTLf property ψ over Σ and if T is a k-locally finite Σ-theory axiomatized by single-variable axioms.

One can also obtain decidability by replacing acyclicity in the combination result of Thm. 20 by local finiteness, using in the proof local finiteness to ensure that up to equivalence there are only finitely many formulas without arithmetic.

IV. Bounded lookback. The above criteria achieve decidability mostly by syntactic restrictions. However, finite coreachability graphs can also be achieved by controlling interaction of constraints in properties, as it was already shown for the arithmetic case [Felli et al., 2023]: Bounded lookback expresses, intuitively, that the verification obligations in an LTLMT f property can be evaluated in a sliding window and depend on only boundedly many steps from the past; it generalizes the feedback freedom property [Damaggio et al., 2012]. Bounded lookback is defined via computation graphs: Let w = ⟨ς0, . . . , ςn-1⟩ ∈ Θ∗ such that q →∗w q′ in Nψ, for some states q, q′ . For each 0≤i<n, let Vi be a fresh set of variables of the same size and sorts as V , and V = ⋃n-1 i=0 Vi. Consider the formulas ς0(V/V0), i.e., the formula obtained from ς0 by systematically replacing V with V0; and ςi(V ◁/Vi-1, V/Vi), i.e., the formula obtained from ςi by replacing V ◁ with Vi-1 and V with Vi, for 0 < i < n. The computation graph Gw of w is the undirected graph with nodes V and an edge from u ∈ V to v ∈ V iff the two variables occur in a common literal of ς0(V/V0) ∧ ∧i≥1 ςi(V ◁/Vi-1, V/Vi). Finally, [Gw] denotes the graph obtained from Gw by collapsing all edges corresponding to equality literals u = v for u, v ∈ V.

Definition 23. The property ψ has K-bounded lookback if for all states q, q′ in the NFA Nψ and all w ∈ Θ∗ such that q →∗w q′ , all acyclic paths in [Gw] have length at most K.

E.g., (x=f(y)) U P(◁x, x) has 1-bounded lookback, but the property φ in Ex. 1 does not because it requires to compare prices of unboundedly many tickets. We show next that the monitoring task for bounded lookback properties is solvable. The proof shows that every formula occurring in a coreachability graph comes from a finite set of formulas since it has bounded quantifier depth and a finite vocabulary.

Theorem 24. For every K > 0, the monitoring task is solvable for K-bounded-lookback properties.

6 Conclusions

We have studied for the first time anticipatory monitoring of data-aware temporal properties expressed in LTLMT f , and identified expressive fragments of the logic for which monitors can be effectively constructed. Specifically, we show monitoring to be solvable for DB-LTLf , an expressive class of first-order temporal properties where the data part combines arithmetic and references to a database. Our approach is fully implemented in the tool MONTHE, which employs CVC5 [Barbosa et al., 2022] for dealing with data (SMT checks and quantifier elimination). Source code and web interface are available via https://monitoring.adatool.dev. The tool takes as input a property, and a trace (given by a sequence of assignments and a set of atoms to define the model); as output, MONTHE reports the monitoring state. Preliminary experiments are reported in the appendix, leaving for future work a more extensive empirical evaluation. Another interesting continuation is to consider dynamic systems where the data component partially changes over time. This is essential to capture controlled updates over a database, like updating the price of a ticket in our running example.

Acknowledgments

1. Montali was partially supported by the NextGenerationEU FAIR PE0000013 project MAIPM (CUP C63C22000770006). This work was also partly supported by Portuguese national funds through Fundac¸˜ao para a Ciˆencia e a Tecnologia, I.P. (FCT) under projects UID/50021/2025 (DOI: https://doi.org/10.54499/UID/50021/2025) and UID/PRR/50021/2025 (DOI: https://doi.org/10.54499/UID/ PRR/50021/2025).