Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

1 Introduction

Data-aware dynamic systems are, essentially, transition systems (TS) whose states are labelled by first-order (FO) interpretations, here referred to as relational TSs (RTS). Initially studied in database theory [Bhattacharya et al., 2007; Deutsch et al., 2009; Bagheri Hariri et al., 2013b], the AI community has paid growing attention to these systems in the last decade, adopting them as models for logically-specified systems, e.g., action theories in the situation calculus [McCarthy and Hayes, 1969; Reiter, 2001], possibly operating over description-logic knowledge bases [Bagheri Hariri et al., 2013a; Calvanese et al., 2016; Borgwardt et al., 2022]. Such interest concerns, in particular, verification [Calvanese et al., 2018; Belardinelli et al., 2014; Bagheri Hariri et al., 2013b; De Giacomo et al., 2012; De Giacomo et al., 2016] and synthesis (typically, planning) [Baier and McIlraith, 2006; Calvanese et al., 2016; Borgwardt et al., 2022].

This paper focuses on verification of RTSs. Several temporal logics have been previously proposed, and in particular a FO extension of the propositional µ-calculus, the FO µcalculus, for which decidability results have been obtained, under a condition of state-boundedness and genericity of the RTS, and syntactic restrictions on the logic which limit the power of quantifiers [Calvanese et al., 2018; Bagheri Hariri et al., 2013b]. State-boundedness holds when the interpretations labeling the states of an RTS contain only a bounded number of distinct objects; genericity essentially captures the inability of distinguishing isomorphic interpretations.

Previous works (see references above) provide a complete picture for branching-time logics (all virtually subsumed by FO µ-calculus) but are poorly conclusive for linear-time. In particular, Calvanese et al. [2018] show that verification is undecidable for the FO extension of linear-time temporal logic (LTL-FO) but do not investigate decidable fragments. This work completes the picture for LTL-FO interpreted over both infinite [ ] and finite traces [De Giacomo and Vardi, 2013]. While, for concreteness, we assume RTSs are described by situation calculus BATs, our results can be applied also to other logical formalisms which guarantee genericity (and boundedness, when needed).

Our approach mirrors the one adopted by Calvanese et al. [2018]. Starting from the most expressive logic, LTL-FO, we consider two increasingly stricter fragments, LTL-FOa and LTL-FOp, obtained by increasingly limiting the power of quantifiers: in LTL-FOa, they range over active objects (i.e., occurring in the interpretation of some fluent); in LTL-FOp, they range over active persisting objects (i.e., remaining active in consecutive states). After re-establishing undecidability of LTL-FOa, thus of LTL-FO, with a proof which, differently from the one by Calvanese et al. [2018], isolates the source of undecidability, we investigate LTL-FOp and prove its decidability. Interestingly, LTL-FOa undecidability contrasts with the decidability of its branching-time counterpart µLa (FO µ-calculus with quantification over active objects) proven by Calvanese et al. [2018].

Decidability of verification paves the way to monitoring, i.e., the problem of checking whether a trace stemming from the execution of an unknown dynamic system does or does not satisfy an LTL-FO property and/or may/will in the future. We show that, for LTL-FOp, this can be done via a direct application of the obtained results, again under a boundedness assumption, naturally fulfilled in the context of Process Mining [van der Aalst, 2016], thus making the obtained results interesting also in that context.

2 Relational Transition Systems

We recall notions and results by Calvanese et al. [2018]. A (first-order) vocabulary is a pair σ = ⟨F, C⟩, where F is the set of predicate fluents and C the set of active (object) constants. Given an interpretation (object) domain ∆ with standard names s.t. C ⊆ ∆, we denote by Int σ∆ the set of all F and C interpretations over ∆ that are the identity on every c ∈ C.

Definition 1 (Relational Transition System, RTS). Given a vocabulary σ = ⟨F, C⟩ and an object domain ∆ s.t. C ⊆ ∆, an RTS (over σ and ∆) is a tuple T = ⟨∆, S, s0,→, I⟩, s.t.: (i) S is a set of states; (ii) s0 ∈ S is the initial state; (iii) → ⊆ S ×S is a transition relation; and (iv) I : S ↦→ Int σ∆ is a labeling function associating each state s ∈ S with an interpretation I(s) = ⟨∆, ·I(s) ⟩ (s.t. cI(s) = c, c ∈ C). ◁

For an RTS T = ⟨∆, S, s0,→, I⟩, a T -run is a (possibly infinite) sequence ρ = s0 s1 · · · of states, s.t.: (i) s0 is T 's initial state, and (ii) si → si+1, for all si, si+1 in ρ. A trace over Int σ∆ is a possibly infinite sequence τ = I0 I1 · · · s.t. each Ii ∈ Int σ∆. By τ(i) we denote Ii and by |τ| the length of τ, i.e., the (possibly infinite) number of FO interpretations in τ. A trace of T is a trace τ = I0 I1 · · · over Int σ∆ s.t. Ii = I(si), for some run ρ = s0 s1 · · · ; in this case, we also say that ρ induces τ. A maximal T -run is either an infinite run or a run s0 · · · sℓ s.t. for no state sℓ+1 ∈ S it holds that sℓ → sℓ+1. A trace of T is maximal if it is induced by a maximal T -run.

We denote by adom(I(s)) the active domain of I(s), i.e., the set of objects occurring in the interpretation of some fluent in s, plus the constants in C. By ˜ I(s) = ⟨adom(I(s)), ·I(s) ⟩, we denote the restriction of I(s) to its active domain. Two interpretations I1 = ⟨∆1, ·I1 ⟩ and I2 = ⟨∆2, ·I2 ⟩ over vocabulary σ = ⟨F, C⟩ are said to be isomorphic, written I1 ∼ I2, if there exists a bijection (called isomorphism) h : ∆1 ↦→∆2 s.t.: (i) for every F ∈ F, it holds that ⃗o ∈ F I1 if and only if h(⃗o) ∈ F I2 ; and (ii) for every c ∈ C, cI2 = h(cI1 ). Intuitively, isomorphic interpretations are the same modulo renaming of the objects in the interpretation domain. When needed, we write I1 ∼h I2, to make the isomorphism h between I1 and I2 explicit. We can now define generic RTSs.

Definition 2 (Generic RTS). An RTS T = ⟨∆, S, s0,→, I⟩ is generic if: for every s1, s′1 , s2 ∈ S and every bijection h : ∆ ↦→ ∆, if I(s1) ∼h I(s2) and s1 → s′1 , then there exists s′2 ∈ S such that s2 → s′2 and I(s′1 ) ∼h I(s′2 ). ◁

Intuitively, this says that if s1 and s2 have the same interpretations modulo renaming, then every successor s′1 of s1 has the same interpretation, modulo renaming, of a successor s′2 of s2, and vice-versa (as states are quantified universally and isomorphisms are invertible). That is, if two states are isomorphic, they induce the same transitions modulo object renaming. As discussed by Calvanese et al. [2018], genericity arises when transitions stem from logical specifications, such as in the situation calculus, when no extra-logical properties are involved that require predefined domains and relations (e.g., integers and their order).

Next we introduce state-bounded RTSs, i.e., RTSs containing a bounded number of objects in the active domain of states, a property that turned out essential for the verification of various temporal logics [Belardinelli et al., 2014; Bagheri Hariri et al., 2013b; De Giacomo et al., 2012; De Giacomo et al., 2016; Calvanese et al., 2018].

Definition 3 (State-Bounded RTS). An RTS T = ⟨∆, S, s0,→, I⟩ is (state-)bounded by b ∈ N if |adom(I(s))| ≤ b, for every s ∈ S. We say that T is state-bounded if it is state-bounded by b for some b. ◁

Notice that state-boundedness allows for the occurrence of infinitely many objects along a run, although only boundedly many at each state. This is a semantic property that naturally arises in situations of practical interest [De Giacomo et al., 2016; Bagheri Hariri et al., 2014].

RTSs can be specified with several formalisms, such as the situation calculus [De Giacomo et al., 2016; Calvanese et al., 2018], which we use here; the obtained results, however, can be applied to any other formalisms for representing RTSs. We briefly recall the situation calculus, referring the reader to the book by Reiter [2001] for a more detailed introduction.

The situation calculus includes terms from three disjoint sorts: objects, i.e., entities in the domain of interest; actions, i.e., events that trigger world changes; and situations, i.e., sequences of actions applied in the situation resulting from previous applications. The constant S0 denotes the initial situation (no action performed) and the function symbol do allows for building situation terms: do(a, s) denotes the situation resulting from the execution of action a in situation s. We assume countably infinitely many object constants under the unique name assumption (UNA, distinct constants denote distinct objects), but do not assume domain closure for objects (not all objects are denoted by a constant).

Fluents are predicates and functions whose value depends on the situation. The situation is, by convention, the last argument, as in Holding(o, s) (object o is being held in situation s). W.l.o.g., we assume no functions other than constants and no non-fluent predicates. All (but the last) fluent arguments are of sort object. Finally, we assume a finite number of action types, each taking a tuple of objects as arguments.

Situation calculus (action) theories describe dynamic domains. We focus on basic action theories (BATs). A BAT D is the union of the following disjoint sets of first-order (FO) and second-order (SO) axioms:

1. D0: (FO) initial situation description axioms describing the initial configuration (may or may not be complete);
2. Dposs: one (FO) precondition axiom Poss(A(⃗x), s) ≡ ϕA(⃗x, s) per action type A, stating the precondition ϕA(⃗x, s) for legal execution of action A(⃗x) in situation s, with special predicate Poss(a, s) expressing that action a is executable in s and with ϕA(⃗x, s) a situation calculus formula uniform in s [Reiter, 2001], i.e., mentioning only s as a situation term and not mentioning Poss ;
3. Dssa: one (FO) successor state axiom F(⃗x, do(a, s)) ≡ ϕF (⃗x, a, s) per fluent F, describing how F changes

when action a is executed in s, with ϕF (⃗x, a, s) uniform in s;

1. Dca: (FO) unique name axioms for actions and (FO) domain closure on action types;
2. Duno: (FO) unique name axioms for object constants;
3. Σ: (SO) foundational, domain independent, axioms of the situation calculus [Reiter, 2001].

A situation s is executable if every action performed in reaching s is executable in the situation where it is performed.

Consider a model M of a BAT D, with object domain ∆ and executable situation domain S. Intuitively, this is obtained by fixing an interpretation of the initial situation (which is unique, modulo object renaming, if the description is complete), and then using precondition and successorstate axioms to generate the model. Let C be the set of constants mentioned in D and assume, w.l.o.g., they all occur in D0. For every situation s ∈ S, define the FO interpretation IM(s) .= ⟨∆, ·I ⟩, where: (i) for every c ∈ C, cI = cM and (ii) for every (situation-suppressed) fluent F of D, F I = {⃗o | ⟨⃗o, s⟩ ∈ F M }. The RTS induced by M [Calvanese et al., 2018] is defined as the RTS TM = ⟨∆, S, s0, I,→⟩, where: (i) S = S; (ii) s0 = SM 0 ∈ S; (iii) → ⊆ S × S is s.t. s → s′ iff there exists some action a s.t. ⟨a, s⟩ ∈ Poss M and s′ = doM (a, s); (iv) For every s ∈ S, I(s) = IM(s). Intuitively, TM is the tree of M's executable situations with each situations s labelled by an interpretation of fluents (and constants), corresponding to the interpretation that M associates to s. As such, TM contains, in general, infinitely many states (i.e., as many as the executable situations of D). Notice that transitions do not carry information about actions. BATs enjoy the following key result.

Theorem 1 (Calvanese et al. 2018). For every model M of a BAT D, the induced RTS TM is generic.

This result states that every RTS induced by a BAT D (through its models) is generic. Unfortunately, an analogous result does not hold for the other critical property of RTS, i.e., state-boundedness. To capture this, De Giacomo et al. [2016] introduce a semantical definition. For a situation s, let Executable(s) be a situation calculus formula expressing that s is executable. Given a model M of a BAT D and a situation s, let Boundedb(s) be a situation calculus formula expressing that the extensions of all fluents at s according to M contain, overall, at most b ∈ N distinct objects (in the original definition, the bound was on the number of tuples for each fluent). Then, a BAT D is said to be bounded, if all of its models M yield that all executable situations are bounded.

Definition 4 (Bounded BAT [De Giacomo et al., 2016]). A BAT D is said to be bounded by b ∈ N, if:

The following is an immediate consequence of Definition 4. Theorem 2. If D is a BAT bounded by b, then every model M of D induces a state-bounded RTS TM.

3 Linear-time Temporal Logic FOVariants

We focus on languages that combine linear-time and FO properties, obtaining a hierarchy that mirrors, in the lineartime setting, that of FO µ-calculi studied by Calvanese et al. [2018]. In the literature, the semantics of linear-time temporal (LTL) logics is typically provided in two alternative variants, over either infinite traces [Pnueli, 1977; Baier and Katoen, 2008] or finite traces [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013]. We adopt both at once. For a FO vocabulary ⟨F, C⟩, LTL-FO (FO linear-time logic) is as follows:

where ϕ is an atomic FO formula F(t1, . . . , tr), with F ∈ F and each ti a variable or a constant from C. Formulae where all variables are quantified, which are the only ones of interest here, are said to be closed. We use the standard abbreviations: (i) ⊥ = ¬⊤, (ii) φ1 ∨ φ2 = ¬(¬φ1 ∧ ¬φ2), (iii) φ ⊃ ψ = ¬φ∨ψ, (iv) ∀x.φ = ¬∃x.¬φ, (v) Fφ = ⊤Uφ, (vi) Gφ = ¬ F ¬φ.

LTL-FO formulae are interpreted over finite or infinite traces over Int σ∆, for some domain ∆, with all constants in C interpreted rigidly, and equality interpreted as the identity. The interpretation is relative to a position i ≥ 0 and a valuation v mapping variables into ∆. By v[x/o] we denote a valuation that matches v on all variables except x, with v[x/o](x) = o. We inductively define when a trace τ satisfies an LTL-FO formula φ at position i ≥ 0 under valuation v, written (τ, i, v) |= φ, as follows (|τ | = ∞ for inifinite τ ):

1. (τ, i, v) |= ⊤, if 0 ≤ i < |τ|;
2. (τ, i, v) |= ϕ, if 0 ≤ i < |τ| and (τ(i), v) |= ϕ;
3. (τ, i, v) |= ¬φ, if (τ, i, v) ̸|= φ;
4. (τ, i, v) |= φ1 ∧φ2, if (τ, i, v) |= φ1 and (τ, i, v) |= φ2;
5. (τ, i, v) |= ∃x.φ, if there exists o ∈ ∆τ(i) s.t. (τ, i, v[x/o]) |= φ;

• there exists i ≤ k < |τ| s.t. (τ, k, v) |= φ2, and
• for every j, if i ≤ j < k then (τ, j, v) |= φ1;

If φ is closed, we omit v and simply write (τ, i) |= φ. Observe that the next operator X is interpreted as strong next, which requires existence of a successor state in τ . This is important if τ is finite and irrelevant otherwise. If needed, the weak next operator Xw, which does not require existence of the successor state, can be expressed as Xw φ = ¬X¬φ.

As we shall see, the central problem of this paper, i.e., checking whether the maximal traces of an RTS satisfy an LTL-FO formula, is undecidable. Thus, the need arises for identifying decidable classes. Following the same approach as the one by Bagheri Hariri et al. [2013b] and Calvanese et al. [2018], by imposing syntactic restrictions, we define two notable fragments of LTL-FO. The fragment LTL-FOa is as follows:

where LIVE is a FO-definable predicate denoting membership of x to the active domain, defined as an abbreviation for the disjunction ∨ P (. . . , x, . . .) over all predicates P ∈ F and all positions of x in P(. . . , x, . . .). Observe that quantification in LTL-FOa is allowed only on objects in the active domain. For instance, the logic cannot express that some object not occurring in the current state will occur in a future state.

Example 1. The following LTL-FOa formula expresses that along a trace, it is always the case that if for some live object x, P(x) holds, then eventually there exists a live object y s.t. Q(x, y) holds:

The other fragment of interest is LTL-FOp, which restricts quantification to persisting objects, i.e., occurring in the active domain of consecutive states. For example, one cannot say that some object enters and leaves the active domain in different states. Formulae of LTL-FOp are defined as follows, where ⃗x and ⃗y can have common variables:

Example 2. The following LTL-FOp formula expresses a property analogous to that of φa in Example 1, except that it requires x to persist in the active domain, until a state is reached where there exists y s.t. Q(x, y) holds:

Observe that φa, instead, does not require x to persist, i.e., x can leave and re-enter the active domain along the trace (although it must eventually show up to make Q(x, y) true).◁

Notice that LTL-FOp can express properties over objects that are present in the current state but disappear in the next one, while it cannot predicate over the same object in nonadjacent states, unless that object is asserted to persist in between.

Example 3. Formula ∃x.LIVE(x) ∧ X¬LIVE(x) is a legal LTL-FOp formula expressing that an object in the current active domain disappears next. Instead, the LTL-FOa formula ∃x.LIVE(x) ∧ XX¬LIVE(x) (with two unrestricted nested strong next operators) is not a legal LTL-FOp formula. ◁

Finally, observe that the case of the until operator U works analogously to that of strong next. In fact, formulae of the form (LIVE(⃗x, ⃗y) ∧ φ1(⃗x))Uφ2(⃗y) require objects ⃗x and ⃗y to persist in the active domain in all states from the current one up to the one immediately preceding the state in which φ2(⃗y) holds.

4 Model Checking

We now focus on model checking (or verification) of RTSs against LTL-FO. For concreteness, we assume RTSs are specified by BATs (and fixed object domains), but the obtained results can be applied to any logical formalism that yields genericity and boundedness (when needed) in the induced RTS. In order to specify RTSs, we use BATs with a complete initial situation description (i.e., s.t. D0 admits exactly one model up to object renaming), interpreted over a given object domain ∆. This implies that the BAT D has a unique model (up to object renaming), thus defines a unique RTS.

Given an RTS T and an LTL-FO formula φ, we say that T satisfies φ, written T |= φ, if τ |= φ, for all maximal traces τ of T . Model checking φ over T consists in checking whether T |= φ. Observe that, since LTL-FO can express trace finiteness with formula φfin = F¬X⊤ (there exists a point with no successor), one can specialize model checking to consider either finite or infinite traces only. This leads to the definitions of finite and infinite model checking, which respectively amount to checking whether T |= φfin ⊃ φ and T |= φfin ∨φ.

4.1 Undecidability

Unsurprisingly, verification is undecidable in general, even for RTSs specified by severely restricted BATs and formulae.

Theorem 3. Model checking of a formula Fp, with p a proposition, is undecidable over RTSs of the form T = ⟨∆, S, s0,→, I⟩ induced by BATs over ∆ with complete initial situation description and two unary fluents.

Proof (Sketch). By reduction from non-emptiness of deterministic 2-counter Minsky automata [Minsky, 1967], which is undecidable. A BAT D that models a generic counter automaton A can be written s.t.: (i) each counter is modeled by a unary fluent; (ii) the number of objects in each fluent represents the value of the counters; (iii) the automaton states are modeled as propositions, with all counters null in the initial state and the final state denoted by special proposition p; (iv) BAT actions simulate increment, conditional decrement, and zero-testing over counters. It can be proven that A is non-empty iff T |= Fp, for T the (unique) RTS induced by D. □

Notice that Theorem 3 seamlessly applies also to finite and infinite model checking. In all cases, undecidability is ultimately due to the possibility of storing unboundedly many objects in fluents, which allows for modeling counters. It is natural to ask oneself whether limiting this ability by requiring state-boundedness [Belardinelli et al., 2012; Bagheri Hariri et al., 2013b] yields decidability, as is the case in the branching-time setting for FO µ-calculus [Calvanese et al., 2018]. Unfortunately, this is not the case: model checking for LTL-FOa, thus LTL-FO, is undecidable even for statebounded BATs. This is proven by Calvanese et al. [2018, Thm. 18] by a reduction from satisfiability of LTL with freezequantifiers over infinite data-words and using one register only [Demri and Lazic, 2009]. With a minimal variation, that reduction can be lifted to encode satisfiability of LTL with freeze-quantifiers over finite data-words, which is also undecidable, but requires two registers [Demri and Lazic, 2009]. This leads us to the following undecidability result, which holds in particular for finite model checking.

Theorem 4. There exists 1-bounded BAT D with complete initial situation description and two unary fluents P1, P2 s.t. finite model checking an LTL-FOa formula using P1 and P2 is undecidable over the RTS T = ⟨∆, S, s0,→, I⟩ induced by D over ∆.

Calvanese et al. [2018, Thm. 18] and Theorem 4 do not help in singling out the essential features of LTL-FOa that cause undecidability, as encoding LTL with freeze-quantifiers requires to employ the whole LTL-FOa logic, with the only restriction that atomic FO formulae are unary. For infinite model checking, we can actually identify a more restricted, informative undecidable fragment of LTL-FOa. To this end, we propose an alternative proof that recasts the proof by Demri and Lazic [2009, Thm. 5.2] into our setting. This allows us to show undecidability of infinite model checking for a fixed 1-bounded BAT already for the fragment of LTL-FOa consisting of unary recurrence formulae, defined next.

Unary recurrence formulae are LTL-FOa formulae as below, where p, q1, q2, q3 are propositional formulae, P is a unary fluent, both occurrences of ⊙ denote either XF or F, and [·] denotes optionality (observe that P(x) implies LIVE(x)):

Theorem 5. There exists 1-bounded BAT D with complete initial situation description and a unary fluent P s.t. infinite model checking unary recurrence formula using P is undecidable over the RTS T = ⟨∆, S, s0,→, I⟩ induced by D over ∆.

Proof (Sketch). By reduction from non-emptiness of counter automata with incrementing errors over infinite executions, which is undecidable even though these automata are weaker than Minsky automata [Demri and Lazic, 2009]. D overapproximates the infinite executions of all counter machines with incrementing errors, operating over a given set of control states. Unary recurrence formulae are used to isolate the executions that encode those of a given automaton, and to express its non-emptiness. □

4.2 Persistence-Preserving Trace Equivalence

Unary recurrence formulae exploit the essential feature of LTL-FOa to quantify over objects across states. In this section, we investigate whether limiting further this ability, as done in LTL-FOp, which restricts quantification to persisting objects only, is beneficial for obtaining decidability. This will turn out to be the case.

We start by introducing a notion of equivalence among traces which captures the intuition that two traces match modulo renaming of the active objects wrt every pair of consecutive states. In other words, only persisting objects are required to maintain their renaming.

Definition 5. Two traces τ1 and τ2 over σ and ∆ are persistence-preserving equivalent (p-equivalent) under a sequence η = h0 h1 · · · of bijections, written τ1 ≍pη τ2, if:

1. for every i ≥ 0, we have τ1(i) ∼hi τ2(i);
2. for every i > 0, the restriction hi+1|adom(τ1(i)) of hi+1 to adom(τ1(i)) coincides with hi|adom(τ1(i)). ◁

We write τ1 ≍p τ2 if τ1 and τ2 are p-equivalent under some sequence of bijections. It is immediate to see that ≍p is an equivalence relation.

P-equivalence preserves the identity of an object across adjacent states only if that object is present in both of them. This implies that those objects that persist along a sequence of pairwise adjacent states also preserve their identity throughout that sequence. At the same time, p-equivalence allows us to single out objects in the current active domain that may disappear in the next one, as well as objects that appear in the next active domain but are not present in the current one. However, p-equivalence cannot distinguish an object that is not present in the current state and appears in the next one from any other object exhibiting the same pattern.

This leads to an interesting property of p-equivalence, namely that it cannot distinguish between globally and locally fresh objects, in the sense formalized next. Let the historical active domain at position i of τ , denoted hadomτ (i), be the set hadomτ(i) = ⋃j∈{0,...,i} adom(τ(j)) of objects that have been active in some interpretation at position j ≤ i. The set of globally fresh objects at position i of τ is ∆ \ hadomτ (i). The set of locally fresh objects at position i of τ is ∆ \ adom(τ(i)). While a locally fresh object at position i might have occurred in some position j < i - 1, this cannot be the case for globally fresh objects. The following remark, a direct consequence of Definition 5, shows that ≍p does not distinguish global and local freshness. Hence, past active objects that have been forgotten can be "recycled" and used as if globally fresh.

Remark 1. Consider two finite traces τ1 and τ2 of length n and such that τ1 ≍pη τ2. Let τ ′1 and τ ′2 be the extensions of such traces with one further interpretation each. If there is a bijection h s.t.: (i) τ ′1 (n) ∼h τ ′2 (n); (ii) h(o) = η(n-1)(o) for o ∈ adom(τ ′1 (n-1)), and h(o) ∈ ∆ \ adom(τ ′2 (n-1)) for o ∈ ∆ \ hadomτ ′1 (n-1), then τ ′1 ≍pηh τ ′2 . ◁

Example 4. Consider the following traces:

Let τ ′1 be the extension of τ1 with {P(o3)}, and τ ′2 the extension of τ2 with {P(o2)}. Since τ ′1 and τ ′2 match but in the last position, o3 is globally fresh at position 2 of τ1, and o2 is locally fresh at position 2 of τ2, by Remark 1, τ ′1 ≍p τ ′2 . ◁

We now connect the notion of p-equivalence to the notion of persistence-preserving bisimulation (p-bisimulation) studied by Bagheri Hariri et al. [2013b] and Calvanese et al. [2018]. This will in turn prove essential when studying p-equivalence of traces induced by RTSs.

Definition 6 (Calvanese et al. 2018). Let T1 = ⟨∆1, S1, s10,→1, I1⟩ and T2 = ⟨∆2, S2, s20,→2, I2⟩ be two RTSs over the same vocabulary, and let H be the set of all possible bijections h : D1 ↦→ D2, for all possible D1 ⊆ ∆1 and D2 ⊆ ∆2. A relation R ⊆ S1 × H × S2 is a p-bisimulation between T1 and T2, if ⟨s1, h, s2⟩ ∈ R implies that:

1. ˜ I1(s1) ∼h ˜ I2(s2);
2. for each s′1 ∈ S1, if s1 →1 s′1 , there exists s′2 ∈ S2 s..t.: (a) s2 →2 s′2 , and
3. for each s′2 ∈ S2, if s2 →2 s′2 , there exists s′1 ∈ S1 s.t.: (a) s1 →1 s′1 , and
4. (b) there exists a bijection h′ : adom(I1(s1)) ∪ adom(I1(s′1 )) ↦→ adom(I2(s2)) ∪ adom(I2(s′2 )) s.t its restriction h′ |adom(I1(s1)) coincides with h|adom(I1(s1)) and ⟨s′1 , h′ |adom(I1(s′1 )), s′2 ⟩ ∈ R;
5. (b) there exists a bijection h′ : adom(I1(s1)) ∪ adom(I1(s′1 )) ↦→ adom(I2(s2)) ∪ adom(I2(s′2 )) s.t its restriction h′ |adom(I1(s1)) coincides with h|adom(I1(s1)) and ⟨s′1 , h′ |adom(I1(s′1 )), s′2 ⟩ ∈ R. ◁

A state s1 ∈ S1 is p-bisimilar to s2 ∈ S2, written s1 ≈p s2, if there exists a p-bisimulation R between T1 and T2 such that ⟨s1, h, s2⟩ ∈ R, for some h; when needed, we also write s1 ≈ph s2, to explicitly name h. Finally, T1 and T2 are pbisimilar, written T1 ≈p T2, if s10 ≈p s20. P-bisimilarity is obviously an equivalence relation.

We are now ready to relate p-equivalence to p-bisimilarity and to the LTL-FOp logic.

Lemma 1. Let T1 and T2 be two RTSs s.t. T1 ≈p T2. Then, for every maximal trace τ1 of T1 there exists a maximal trace τ2 of T2 s.t. τ1 ≍p τ2.

Theorem 6. Let τ1 and τ2 be traces s.t. τ1 ≍p τ2. Then, for every LTL-FOp formula φ, we have τ1 |= φ iff τ2 |= φ.

By Theorem 6 and Remark 1 we get that LTL-FOp cannot capture global freshness, and by combining Lemma 1 with Theorem 6, we obtain the following key result.

Theorem 7. Let T1 and T2 be two RTSs s.t T1 ≈p T2. Then, for every LTL-FOp formula φ, we have T1 |= φ iff T2 |= φ.

4.3 Decidability

We are now ready to address decidability of model checking. Using Theorem 7, we can import in our setting the data abstraction techniques studied by Bagheri Hariri et al. [2013a] and De Giacomo et al. [2016] for state-bounded, generic RTSs. For such systems, it is shown that for every RTS T there exists a p-bisimilar, finite-state T ′ , referred to as an abstraction of T . Interestingly, T ′ can be obtained by recycling, as much as possible, locally fresh objects whenever fresh ones are needed; the bound on the active domain of each state guarantees that boundedly many old objects are enough to ensure that no further globally fresh objects are needed, in turn guaranteeing that the resulting abstraction RTS is finite-state.

Theorem 8 (De Giacomo et al. 2016). For every generic and state-bounded RTS T = ⟨∆, S, s0,→, I⟩ over a vocabulary σ, there exists a finite-state and state-bounded RTS T ′ = ⟨∆′ , S′ , s′0 ,→′ , I ′ ⟩ over σ with finite ∆′ , s.t. T ≈p T ′ .

Observe that since the abstract RTS T ′ of Theorem 8 is finitestate and state-bounded, T ′ is essentially a transition system with propositional labeling. While it can be shown that checking whether T ′ |= φ, for φ an LTL-FOp formula, is decidable, this does not imply decidability of T |= φ, as Theorem 8 does not state effective computability of T ′ . To obtain such a desirable result, we need to take advantage of the (logical) representation of T , in our case as a BAT. Specifically, let D be the BAT used, together with the infinite object domain ∆, to specify T . De Giacomo et al. [2016] show that, in order to achieve decidability, it is enough to replace the infinite object domain ∆ with a suitable finite subset ∆′ ⊂ ∆ and then use this and the BAT D to specify T ′ . Under this condition, one can effectively compute the desired T ′ , thus obtaining decidability of model checking.

Theorem 9 (De Giacomo et al. 2016). Let D be a BAT bounded by b with complete initial situation description, M its model (unique, up to object renaming) for an infinite object domain ∆, and TM the corresponding induced RTS. Moreover, let n be the maximal number of parameters occurring in the action types of D. Then, for any possibly finite ∆′ s.t. |∆′ | ≥ 2b + n + |C|, one can effectively compute a finitestate RTS T ′ s.t. TM ≈p T ′ .

Intuitively, the construction of T ′ consists in constructing a finite fragment of M, starting from the initial situation and expanding all situations currently in the fragment by applying all executable actions. State-finiteness is obtained by including a new situation only if the corresponding interpretation does not match any other of some situation already in the fragment. By finiteness of ∆′ and boundedness of D, the procedure terminates, as there exist only finitely many distinct interpretations. T ′ is then easily obtained from the constructed fragment. An analogous result can be obtained with some care, also for BATs with incomplete initial situation description [De Giacomo et al., 2016]. This leads to the following main result, which, we stress once again, holds for every logical formalism other than the situation calculus, as long as it guarantees genericity of the modeled RTS.

Theorem 10. Model checking LTL-FOp formulae over statebounded, generic RTSs specified by BATs is decidable.

5 Monitoring

Monitoring amounts to verifying whether the ongoing execution of an unknown dynamic system satisfies a property of interest, considering also its possible future continuations [Bauer et al., 2010; Ly et al., 2015]. A 4-valued semantics, called RV-LTL, has been introduced by Bauer et al. [2010], recast by De Giacomo et al. [2014] over finite traces, and employed by De Giacomo et al. [2020] for reinforcement learning.

We lift RV-LTL to our FO setting. The current (finite) execution is modeled as a finite trace τ. For simplicity, we consider as possible execution continuations only finite, unbounded extensions of τ, but our results hold also for infinite extensions. Let RV = {CS, PS, CV, PV} be the set of 4 RV-LTL states, with the following meaning: (i) CS (current satisfaction): (formula) satisfied now but violable in some future; (ii) PS (permanent satisfaction): satisfied now and in all futures; (iii) CV (current violation): violated now but satisfiable in some future; and (iv) PV (permanent violation): violated now and in all futures. This is formalized below.

Definition 7. Given a finite trace τ, an LTL-FO formula φ over σ, and an interpretation domain ∆, we say that φ is in monitoring state s ∈ RV after τ , written τ |= �φ = s�, if:

· s = CS, τ |= φ, and ττ ′ ̸|= φ, for some finite trace τ ′ ; · s = PS, τ |= φ, and ττ ′ |= φ, for every finite trace τ ′ ; · s = CV, τ ̸|= φ, and ττ ′ |= φ for some finite trace τ ′ ; · s = PV, τ ̸|= φ, and ττ ′ ̸|= φ for every finite trace τ ′ . ◁

It is immediate to see that, for a finite trace τ and an LTL-FO formula φ, there exists exactly one s ∈ RV such that τ |= �φ = s�. LTL-FO monitoring consists in computing the monitoring state s ∈ RV s.t. τ |= �φ = s�.

By Definition 7 it follows that monitoring is at least as hard as LTL-FO satisfiability and validity. To see this, it is enough to apply Definition 7 when τ is the empty trace. As a consequence, we can obtain for monitoring a strong undecidability result analogous to Theorem 4. To this end, we first need to adapt to traces the notion of state-boundedness for RTSs (Definition 3).

Definition 8. A trace τ is (state-)bounded by b ∈ N if |adom(τ(i))| ≤ b, for 0 ≤ i < |τ|. We say that τ is (state-)bounded if it is bounded by b for some b. ◁

Theorem 11. LTL-FOa monitoring over 1-bounded traces is undecidable.

Again, however, analogously to the case of model checking, we obtain decidability for state-bounded traces and LTL-FOp.

Theorem 12. LTL-FOp monitoring over state-bounded traces is decidable.

Proof (Sketch). Consider a finite trace τ bounded by b and an LTL-FOp formula φ. The proof consists in characterizing the RV-LTL states through two verification problems on φ or ¬φ, based on the state under consideration. Checking whether τ |= φ or τ |= ¬φ can be done via LTL-FOp model checking, by replacing τ with a trivial generic state-bounded RTS with τ as unique trace, which is decidable by Theorem 10. For the extensions of τ , we define a BAT D state-bounded by b, with a unique model M s.t. the sequence of interpretations assigned by M to each path in the tree of executable situations corresponds either to a prefix or a possible b-bounded extension of τ, over the given vocabulary σ. We then check whether D |= φfin ⊃ φ, using φfin to restrict to finite extensions (recall that φfin expresses trace finiteness), which is decidable by Theorem 10. □

Example 5. Consider formula φp1 from Example 2, and the following formula φp2 expressing that at some point in the trace, there must be a live object x for which P(x) holds and then, as long as x persists, S(x) should never hold:

The table below shows the result of the monitoring of φp1 and φp2 for the following trace:

Bounded traces are not only induced by state-bounded systems, but naturally arise also in the context of Process Mining (PM) [van der Aalst, 2016]. An integral part of PM deals with operational support for running operational processes instantiated on case objects, such as orders, packages, or claims. Such objects spawn executions, producing traces whose positions contain logged events, which are essentially tuples of instantiated attributes. Since each position in a case trace contains exactly one logged event, every trace is state-bounded by the maximum number of attributes of the events occurring therein. Hence, by Theorem 12, LTL-FOp can be effectively used to monitor operational processes, a main task in operational support [van der Aalst, 2016; Ly et al., 2015]. We can also extend the application of our technique in this setting by considering a bounded set of related cases, using LTL-FOp to express so-called instance spanning constraints [Fdhila et al., 2016].

6 Conclusions

We have addressed the problem of verification of FO extensions of temporal logics in the linear-time setting, for both infinite and finite traces, left almost unexplored by previous work, which focused mainly on branching-time. We have shown that, for generic and state-bounded RTSs, verification of LTL-FOp is decidable, whereas it is undecidable for LTL-FOa. The latter contrasts with a previous result for branching-time, which states that restricting quantification to the active domain yields decidability. To obtain our results, we have isolated the undecidability source for the most expressive logic LTL-FO, a point left unclear so far, and then have investigated the increasingly stricter fragments LTL-FOa and LTL-FOp. While our work focuses on RTSs specified as situation calculus basic action theories, the obtained results seamlessly apply to all formalisms that induce generic RTSs.

The decidability result opens the way to monitoring for LTL-FOp, a problem of practical interest naturally arising in Process Mining, which consists in checking whether the ongoing execution of an unknown system currently satisfies an LTL-FOp formula and/or will do in the future, as the execution carries on. We have recasted the problem in our setting and shown its decidability under state-boundedness.

As future work, we intend to develop automata-based techniques for verification and monitoring of LTL-FOp. To this end, thanks to the abstraction techniques exploited here, we can directly import algorithmic approaches based on FO extensions of LTL interpreted over fixed, finite domains, such as those by Baier and McIlraith [2006] and by De Masellis and Su [2013].

Acknowledgements

This work is partly supported by the ERC Advanced Grant WhiteMech (No. 834228), the EU ICT-48 2020 project TAILOR (No. 952215), the Sapienza Project DRAPE, the Italian Basic Research (PRIN) projects HOPE and PINPOINT, the unibz ID 2020 project SMART-APP, and the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.