Do You Need Infinite Time?

1 Introduction

Since the introduction of linear temporal logic (LTL), several propositional and first-order LTL-based formalisms have been developed for applications such as automated planning [Bacchus and Kabanza, 2000; Baier and McIlraith, 2006], process modelling [van der Aalst and Pesic, 2006; Maggi et al., 2011] and verification of programs [Manna and Pnueli, 1995]. Related research in knowledge representation has focused on decidable fragments of first-order temporal logic, TUQL [Hodkinson et al., 2000; Gabbay et al., 2003], and in particular on temporal description logics [Wolter and Zakharyaschev, 1998; Artale and Franconi, 2005] that combine LTL operators with description logics (DLs). These logics usually lie within the two-variable monodic fragment of TUQL, TUQL221 , obtained by restricting to formulas having at most two variables, and so that the temporal operators are applied only to subformulas with at most one free variable. The complexity of the satisfiability problem ranges from EXPSPACE-complete, for TUQL221 [Gabbay et al., 2003; Hodkinson et al., 2003], down to NEXPTIME- or EXPTIME-complete, for temporal extensions of ALC without temporalised roles and with restrictions on the application of temporal operators [Lutz et al., 2008;

Baader et al., 2012], or even in NP or NLOGSPACE, by modifying further both the temporal and the DL components, as in some temporal extensions of DL-Lite for conceptual data modelling [Artale et al., 2014].

Besides the usual LTL semantics defined on infinite linear structures, attention has been devoted also to finite traces, which are linear temporal structures with only a finite number of time points [Cerrito et al., 1999; De Giacomo and Vardi, 2013; Fionda and Greco, 2016]. Indeed, the finiteness of the time dimension is a fairly natural restriction. In automated planning, or when modelling business processes with a declarative formalism, we consider finite action plans and terminating services, often within a given temporal bound [Bauer and Haslum, 2010; De Giacomo et al., 2014a; De Giacomo et al., 2014b; Camacho et al., 2017]. In runtime verification, only the current finite behaviour of the system is taken into account. Infinite models are then considered to check whether a given requirement is satisfied in the infinite extensions of this finite trace [Giannakopoulou and Havelund, 2001; Bauer et al., 2010]. Although some recent work has considered temporal extensions of DLs in the context of runtime verification [Baader and Lippmann, 2014] and business process modelling [van der Aalst et al., 2017], the proposals developed so far are based on the usual infinite trace semantics and are limited in expressivity.

This work focuses on first-order temporal logic on finite traces [Cerrito et al., 1999], defined by extending the firstorder language with temporal operators interpreted on finite traces. We obtain the following main results.

• The complexity of TUQL221 remains EXPSPACEcomplete on finite traces, but lowers down to NEXPTIME if we restrict to traces with a bound k on the number of instants. Moreover, it has the bounded model property.
• Similar results (including the bounded model property) also hold for the temporal DL TUALC on finite traces, where the complexity further reduces to EXPTIME if only global axioms and finite traces with a fixed bound on instants are allowed.
• We establish semantic and syntactic conditions which characterise when the distinction between reasoning on finite and infinite traces can be completely blurred, providing connections with planning and verification.

Concerning this last point, several approaches have been considered to preserve satisfiability of formulas from the finite to the infinite case, so to reuse algorithms developed for the infinite case [Bauer and Haslum, 2010; De Giacomo et al., 2014b]. Here, we determine conditions that preserve satisfiability also in the other direction, from infinite to finite traces. This opens interesting research directions towards the application of efficient finite traces reasoners [Li et al., 2014] to the infinite case. We provide a uniform framework for these notions, bridging finite and infinite trace semantics. Full proofs are available in our technical report [Artale et al., 2019].

2 First-order Temporal Logics

The first-order temporal language, TUQL [Gabbay et al., 2003], is obtained by extending the usual first-order language with the temporal operator until (U) interpreted over discrete linear structures, called traces.

Syntax The alphabet of TUQL consists of countably infinite and pairwise disjoint sets of predicates NP (with ar(P) ∈ N being the arity of P ∈ NP), constants (or individual names) NI, and variables Var; the logical operators ¬, ∧; the existential quantifier ∃, and the temporal operator U (until). The formulas of TUQL are of the form:

where P ∈ NP, ¯ τ = (τ1, . . . , τar(P)) is a tuple of terms, i.e., constants or variables, and x ∈ Var. Formulas without the until operator are called non-temporal. We write ϕ(x1, . . . , xm) to indicate that the free variables of a formula ϕ are in {x1, . . . , xm}. For p ∈ N, the p-variable fragment of TUQL, denoted by TUQLp , consists of TUQL formulas with at most p variables (TUQL0 is simply propositional LTL). The monodic fragment of TUQL, denoted by TUQL21 , consists of formulas such that all subformulas of the form ϕ U ψ have at most one free variable.

Semantics A first-order temporal interpretation is a structure M = (∆M, (In)n∈T), where T is an interval of the form [0,∞) or [0, l], with l ∈ N, and each In is a classical firstorder interpretation with domain ∆M (or simply ∆): we have P In ⊆ ∆ar(P) , for each P ∈ NP, and aIi = aIj ∈ ∆ for all a ∈ NI and i, j ∈ N, i.e., constants are rigid designators (with fixed interpretation, denoted simply by aI ). The stipulation that all time points share the same domain ∆ is called the constant domain assumption (meaning that objects are not created or destroyed over time), and it is the most general choice in the sense that increasing, decreasing, and varying domains can all be reduced to it [Gabbay et al., 2003]. An assignment in M is a function a from terms to ∆: a(τ) = a(x), if τ = x, and a(τ) = aI , if τ = a ∈ NI (given a tuple of m terms ¯ τ = (τ1, . . . , τm), we set a(¯ τ) = (a(τ1), . . . , a(τm)). Satisfaction of a formula ϕ in M at time point n ∈ T under assignment a (written M, n |=a ϕ) is inductively defined as:

We say that ϕ is satisfied in M (and M is a model of ϕ), writing M |= ϕ, if M, 0 |=a ϕ, for some a. Moreover, ϕ is said to be satisfiable if it is satisfied in some M. A formula ϕ logically implies a formula ψ if every M that satisfies ϕ satisfies also ψ, and we write ϕ |= ψ. We say that ϕ and ψ are equivalent, writing ϕ ≡ ψ, if ϕ |= ψ and ψ |= ϕ.

In the following, we call finite trace a first-order temporal interpretation with T = [0, l], often denoted by F = (∆F, (Fn)n∈[0,l]), while infinite traces, based on T = [0,∞), will be denoted by I = (∆I , (In)n∈[0,∞)). We say that a TUQL formula ϕ is satisfiable on infinite, finite, or k-bounded traces, if it is satisfied in a trace in the class of infinite, finite, or finite traces with at most k ∈ N, k > 0 (given in binary) time points, respectively.

Let F = (∆F, (Fn)n∈[0,l]) and I = (∆I , (In)n∈[0,∞)) be, respectively, a finite and an infinite trace s.t. ∆F = ∆I (writing ∆) and aF = aI , for all a ∈ NI. We denote by F · I = (∆F·I , (F · In)n∈[0,∞)) the extension of F with I, defined as the infinite trace with ∆F·I = ∆, aF·I = aF , for all a ∈ NI, and for P ∈ NP, n ∈ N:

In addition to the standard Boolean equivalences, we will use the following equivalences for formulas: ⊥ ≡ ∃x(P(x) ∧ ¬P (x)), ⊤ ≡ ¬⊥; ©ϕ ≡ ©1ϕ ≡ ⊥ U ϕ; ©q ϕ ≡ ©©q-1ϕ, with q > 1; 3ϕ ≡ ⊤ U ϕ; 2ϕ ≡ ¬3¬ϕ; 3+ϕ ≡ ϕ ∨ 3ϕ; and 2+ϕ ≡ ¬3+¬ϕ. Over finite traces, last ≡ ¬©⊤ is satisfiable in the last time point.

3 Satisfiability over Finite Traces

In the following we show how to reduce the formula satisfiability problem over finite traces to the same problem over infinite traces. Similar to the encoding proposed in [De Giacomo and Vardi, 2013] for propositional LTL, to capture the finiteness of the temporal dimension, we introduce a fresh predicate E (standing for the end of time) with the following properties: (i) there is a least one instant before the end of time; (ii) the end of time comes for all objects; (iii) the end of time comes at the same time for every object; (iv) the end of time never goes away. We axiomatise these properties as follows:

We now characterise models satisfying the end of time formula ψf = ψf1 ∧ ψf2 ∧ ψf3 . Let F = (∆, (Fn)n∈[0,l]) and I = (∆, (In)n∈[0,∞)) be, respectively, a finite and an infinite trace with the same domain ∆ and such that aF = aI , for all a ∈ NI. We denote by F ·E I the end extension of F with I, defined as the extension F · I, for all P ∈ NP \ {E}, such that:

Clearly, the extension of E characterises the satisfiability of ψf . We formalise this in the next lemma.

Lemma 1. For every infinite trace I, I |= ψf iff I = F ·E I′ , for some finite trace F and some infinite trace I′ .

We now introduce a translation ·† for TUQL formulas, used together with the end of time formula, ψf , to capture satisfiability on finite traces. More formally, a TUQL formula ϕ is satisfiable on finite traces if and only if its translation ϕ† is satisfied in an infinite trace that also satisfies the formula ψf . The translation ·† is defined as:

Lemma 2 states the correctness of ·† .

Lemma 2. Let F ·E I be an end extension of a finite trace F. For every TUQL formula ϕ and every assignment a, F |=a ϕ iff F ·E I |=a ϕ† .

From the previous lemmas, we obtain a reduction of the TUQL satisfiability problem to the same problem for TUQL.

Theorem 3. Let ϕ be a TUQL formula. Then ϕ is satisfiable on finite traces iff ϕ† ∧ ψf is satisfiable on infinite traces.

We use the translation to transfer the EXPSPACE upper bound for TUQL221 over infinite traces to finite traces [Hodkinson et al., 2003]. The lower bound can be proved using similar ideas as those used to prove hardness of TUQL221 .

Theorem 4. TUQL221 satisfiability on finite traces is EXPSPACE-complete.

We now study TUQL221 satisfiability on traces with at most k time points, with k given in binary, as part of the input. We show that in this case the complexity of the satisfiability problem decreases from EXPSPACE to NEXPTIME. Hardness follows from the fact that: (1) one can translate ALC-LTL with rigid concepts to TUQL221 ; and (2) satisfiability in ALC-LTL with rigid concepts on k-bounded traces is NEXPTIME-hard, as for infinite traces [Baader et al., 2012, Lemma 6.2]. For the upper bound, we resort to a classical abstraction of models called quasimodels [Gabbay et al., 2003]. One can show that there is a model with at most k time points iff there is a quasimodel with a sequence of states (sets of subformulas with certain constraints) of length at most k. Then, our upper bound is obtained by guessing an exponential size sequence of states which serves as a certificate for the existence of a quasimodel (and therefore a model) for the input formula.

Theorem 5. TUQL221 satisfiability on k-bounded traces is NEXPTIME-complete.

We end this section by establishing that TUQL221 on finite traces enjoys the bounded trace property and the bounded domain property. If there is a finite trace which satisfies a TUQL221 formula ϕ then there is a finite trace with at most k time points, with k double exponentially large w.r.t. the size of ϕ. This bound follows from the fact that (1) if there is a quasimodel for ϕ then there is a quasimodel for ϕ where there is no repetition of states [Gabbay et al., 2003], except for the last state; and (2) the fact that the length of the finite non-repeting sequence of states is correlated with the number of time points in a finite trace. The number of distinct states of a TUQL221 formula on finite traces is the same as in the infinite case, where it is known to be double exponential [Gabbay et al., 2003]. This directly implies that TUQL221 enjoys the bounded trace property.

Theorem6. TUQL221 satisfiability of ϕon finite traces implies TUQL221 satisfiability of ϕ on k-bounded traces, with k double exponential in |ϕ|.

We now establish that a TUQL221 formula has the bounded domain property: if it is satisfiable, then there is a model with the size of the domain exponential in k (meaning that it is double exponential in the binary representation of k).

Theorem 7. TUQL221 satisfiability of ϕ on k-bounded traces implies the existence of a model with domain size exponential in k and ϕ.

Since TUQL221 satisfiability on finite traces implies satisfiability on k-bounded traces, for some k > 0, the formula

which only admits models with an infinite domain [Lutz et al., 2008], is unsatisfiable over finite traces.

4 Finite vs. Infinite Traces

While certain formulas, such as 2⊤, are satisfiable both on finite and infinite traces, others, e.g., 3last and 2+©⊤, are only satisfiable on finite traces and on infinite traces, respectively. One then wonders, when does satisfiability on finite and infinite traces coincide, so that solvers can simply stop trying to build the lasso of an infinite trace when a finite trace is built? A similar question can be posed for the problem of equivalences between formulas. For example, 32(ϕ∨ψ) and (32ϕ) ∨ (32ψ) are equivalent on finite traces but not on infinite traces [Bauer and Haslum, 2010]. Moreover, 2+3+ϕ and 3+2+ϕ are not equivalent on infinite traces, whereas on finite traces they are both equivalent to 3+(last ∧ ϕ) [De Giacomo and Vardi, 2013]. Conversely, ⊥ and last are only equivalent on infinite traces.

In this section we address these questions and investigate the distinction between reasoning on finite and on infinite traces. More specifically, we propose semantic properties which guarantee that formula satisfiability and equivalences between formulas are preserved, and thus, the distinction can be blurred. Given a finite trace F, we define the set of extensions of F as the set Ext(F) = {I | I = F · I′ , for some I′ }. Instead, given an infinite trace I, the set of prefixes of I is the set Pre(I) = {F | I = F · I′ , for some I′ }. For a TUQL formula ϕ and a quantifier Q ∈ {∃, ∀}, we say that ϕ is FQ if, for all finite traces F and all assignments a, it satisfies the finite trace property:

and, similarly, ϕ is IQ if, for all infinite traces I and all assignments a, it satisfies the infinite trace property:

Examples of formulas satisfying F∃ and I∀ are formulas of the form 2+ϕ, where ϕ is a formula without temporal operators

2+P (x) ∨ 3+(P (x) ∧ ©last).

Table 1: Formulas satisfying exactly one of the finite/infinite trace properties (Formula (*) is from Section 3).

(formulas of the form 2ϕ are also I∀ but not F∃ because of, e.g., 2⊥). On the other hand, the properties F∀ and I∃ capture formulas of the form 3+ϕ, where ϕ is again a formula without temporal operators (formulas of the form 3ϕ are also I∃ but

not F∀ because of, e.g., 3⊤). The semantic properties, FQ and IQ, capture different classes of TUQL formulas, as we illustrate in Table 1. We formalise this statement with the following theorem.

Theorem 8. Let TUQL(P) denote the set of TUQL formulas which satisfy property P. The sets TUQL(F∃), TUQL(F∀), TUQL(I∃), and TUQL(I∀) are mutually incomparable.

One can also restrict to the 'one directional' version of the above properties. We denote by F◦Q and I◦Q, where ◦ ∈ {⇒ ,⇐}, the corresponding '⇒' and '⇐' directions of the FQ and IQ properties, respectively. On the relationship between these one directional properties, we have the following. Given two different quantifiers Q and Q′ (among ∃ and ∀), a TUQL formula ϕ is F⇒Q if, and only if, its negation ¬ϕ is F⇐Q′ . Similarly, ϕ is I⇒Q if, and only if, ¬ϕ is I⇐Q′ . Moreover, if a TUQL formula ϕ is F⇒∀, then it is also F⇒∃, and if ϕ is I⇒∀, it is I⇒∃ as well. However, the sets of formulas satisfying F⇒∀ and I⇒∃ are incomparable. Indeed, the formula 2+©⊤ is F⇒∀ and not I⇒∃. On the other hand, the sets of formulas satisfying I⇒∃ and F⇒∀ are also incomparable. To see this,

consider 3last, which is I⇒∃ but not F⇒∀. In Theorem 3, we have proved that TUQL formulas interpreted on finite traces can be translated into equisatisfiable formulas on infinite traces. Such translation is not always needed, since for some classes of formulas satisfiability is already preserved. Indeed, for a TUQL formula ϕ: if ϕ is F⇒∃, then it is satisfiable on finite traces only if it is satisfiable on infinite traces; moreover, if ϕ is I⇒∃, then it is satisfiable on infinite traces only if it is satisfiable on finite ones.

We now consider the problem of formula equivalence, by showing under which semantic properties equivalence between formulas can be blurred. Given TUQL formulas ϕ and ψ, we write ϕ ≡I ψ if ϕ and ψ are equivalent on infinite traces, and ϕ ≡F ψ if they are equivalent on finite traces. The following theorem provides sufficient conditions to preserve formula equivalence from the infinite to the finite case (cf. the notion of LTL compliance in [Bauer et al., 2010]).

Theorem 9. Given TUQL formulas ϕ and ψ, ϕ ≡I ψ implies ϕ ≡F ψ whenever both ϕ and ψ are (1) F∃; or (2) F∀; or (3) F⇒∃ and I⇒∀.

Theorem 9 does not hold for formulas that satisfy only I∃ or I∀. Consider the formulas 2©⊤ ∨ last and 2©⊤ ∨ ©last, which are I∃. These formulas are equivalent only on infinite traces. Also, 2+P (x) ∨3+(P (x) ∧ last) and 2+P (x) ∨3+(P (x) ∧ ©last) are I∀, and equivalent on infinite but not on finite traces. This example also shows that the condition I⇒∀ alone is not sufficient for Theorem 9. Moreover, F⇒∃ alone is also not sufficient. To see this, consider, e.g., 2+3⊤∨(P(x)∧3last) and 2+3⊤∨ (3last) , which are F⇒∃ but are equivalent only over infinite traces. We now present sufficient conditions to preserve equivalences from the finite to the infinite case.

Theorem 10. Given TUQL formulas ϕ and ψ, ϕ ≡F ψ implies ϕ ≡I ψ whenever both ϕ and ψ are (1) I∃; or (2) I∀; or (3) F⇒∀ and I⇒∃.

We point out that F∃ or F∀ are not sufficient to ensure that formula equivalence on finite traces implies formula equivalence on infinite traces. To illustrate this, consider for example the formulas Φ = 3+last ∨ 3P (x), and the union of Φ and Formula (*) from Section 3. These formulas are F∃, however, they are only equivalent on finite traces. Moreover, if we take 3+P(x) and the union of 3+P(x) with Formula (*), we have that they are both F∀, though equivalent only on finite traces. This example also shows that the condition F⇒∀ alone is not sufficient for Theorem 10. We now argue that I⇒∃ alone is also not sufficient. To see this, consider, e.g., (P(x) ∧2+3⊤) ∨3last and 2+3⊤∨3last, which are I⇒∃ but are equivalent only on finite traces.

From Theorems 9 and 10 we have that if both ϕ and ψ are F∃ or F∀, and I∃ or I∀ TUQL formulas, then, ϕ ≡F ψ iff ϕ ≡I ψ. In particular, the above examples show that if, from a given pair of conditions FQ and IQ′ , we remove any of the two properties, then formula equivalences on finite and infinite traces may not coincide. We now analyse syntactic features of the properties introduced so far, providing a class of formulas satisfying them.

Theorem 11. All non-temporal TUQL formulas satisfy the finite/infinite trace properties F∃, F∀, I∃, and I∀.

3+-formulas ϕ, ψ are built according to (with P ∈ NP):

We now show that the language generated by the grammar rule for 3+-formulas contains only formulas which are F∀ and I∃. We call 3-formulas the set of formulas generated by the result of further allowing 3ϕ in the grammar rule for 3+-formulas; and call 3+∀-formulas the result of allowing ∀xϕ in the grammar rule for 3+-formulas.

Theorem 12. All 3+-formulas are F∀ and I∃. Moreover, all 3+∀-formulas are F∀ and all 3-formulas are I∃.

The results of Theorem 12 are tight in the sense that we cannot extend the grammar rule for 3+-formulas with ∀xϕ; and we cannot extend the grammar rule for 3+∀-formulas with 3ϕ. Simple counterexamples are ∀x3+P(x) and 3⊤, which are not I∃ and F∀, respectively. To see that ∀x3+P(x) is not I∃ consider the model with an infinite (and countable) domain, where one element is in P exactly at time point n ∈ N, another one exactly at time point n + 1 and so on. There is no finite prefix where ∀x3+P (x) holds.

2+-formulas ϕ, ψ are built according to (with P ∈ NP):

We call 2-formulas the set of formulas generated by the result of further allowing 2ϕ in the grammar rule for 2+-formulas; and call 2+∃-formulas the result of allowing ∃xϕ in the grammar rule for 2+-formulas.

Theorem 13. All 2+-formulas are F∃ and I∀. Moreover, all 2+∃-formulas are F∃ and all 2-formulas are I∀.

The results of Theorem 13 are also tight in the sense that we cannot extend the grammar rule for 2+-formulas with ∃xϕ; and we cannot extend the grammar rule for 2+∃-formulas with 2ϕ. Simple counterexamples are ∃x2+¬P(x) and 2⊥, which are not I∀ and F∃, respectively. To see that ∃x2+¬P(x) is not I∀, consider again the model described above with an infinite (and countable) domain, where each element is in P at a specific time point n ∈ N. The formula ∃x2+¬P(x) holds in every finite prefix but it does not hold in this infinite trace.

It follows from our results that there is no distinction between reasoning on finite and infinite traces whenever a formula is either a 3+- or a 2+-formula. As already pointed out, 3+2+ϕ and 2+3+ϕ are only equivalent on finite traces, and so, the distinction between reasoning on finite and infinite traces cannot be blurred for the class of formulas that allow both 3+ and 2+.

5 Applications

The problem considered so far, to determine when the differences between finite and infinite traces can be safely blurred, is of interest for several applications. Here we show how it can be related to planning and verification. Moreover, for knowledge representation scenarios, we introduce temporal DLs on finite traces, providing complexity results for the satisfiability problem.

Planning. In automated planning, the sequence of states generated by actions is usually finite [Cerrito and Mayer, 1998; Bauer and Haslum, 2010; De Giacomo and Vardi, 2013; De Giacomo et al., 2014b]. To reuse temporal logics based on infinite traces for specifying plan constraints, one approach, developed by De Giacomo et al. 2014b for LTL, is based on the notion of insensitivity to infiniteness. This property is meant to capture those formulas that can be equivalently interpreted on infinite traces, provided that, from a certain instant, these traces satisfy an end event forever and falsify all other atomic propositions. The motivation for this comes from the fact that propositional letters represents atomic tasks/actions that cannot be performed anymore after the end of a process.

In order to lift this notion of insensitivity to our first-order temporal setting, and to provide a characterisation analogous to the propositional one, we introduce the following definitions. Let F = (∆F, (Fn)n∈[0,l]) be a finite trace, and let E = (∆E, (En)n∈[0,∞)) be the infinite trace such that ∆E = ∆F (we write just ∆), aE = aF for all a ∈ NI, and for all P ∈ NP \ {E}, P En = ∅, while EEn = ∆, where n ∈ [0,∞). The end extension (see Section 2) of F with E, F ·E E, will be called the insensitive extension of F. A TUQL formula ϕ is insensitive to infiniteness (or simply insensitive) if, for every finite trace F and all assignments a, F |=a ϕ iff F ·E E |=a ϕ. Clearly, all insensitive TUQL formulas are also F⇒∃.

Now, let Σ be a finite subset of NP. Assume w.l.o.g. that the TUQL formulas we mention in this subsection have predicates in Σ, and that Σ contains the end of time predicate E. Recalling the definition of ψf , we define χf = ψf ∧χf1 , with

The next characterisation result extends Theorem 4 in [De Giacomo et al., 2014b] to TUQL.

Theorem 14. A TUQL formula ϕ is insensitive to infiniteness iff χf |= ϕ↔ϕ† holds on infinite traces.

Insensitive formulas allow us to blur the distinction between finite and infinite traces as soon as infinite traces satisfy χf . Thus, we can check satisfiability of insensitive TUQL221 (or other decidable languages) formulas on finite traces by using satisfiability algorithms for the infinite case without the need to apply the ·† translation.

We now analyse some syntactic features of this property. Firstly, non-temporal TUQL formulas, are insensitive. Moreover, this property is preserved under non-temporal operators. We generalise Theorem 5 in [De Giacomo et al., 2014b] in our setting as follows.

Theorem 15. Let ϕ, ψ be insensitive TUQL formulas. Then ¬ϕ, ∃xϕ, and ϕ ∧ ψ are insensitive.

Concerning temporal operators, in [De Giacomo et al., 2014b] it is shown how several standard temporal patterns derived from the declarative process modelling language DECLARE [van der Aalst and Pesic, 2006] are insensitive. On the other hand, negation affects the insensitivity of temporal formulas. For instance, given a TUQL formula P(x), we have that 3+P(x) is insensitive while 3+¬P(x) is not. Dually, 2+¬P(x) is insensitive, while 2+P(x) is not. Therefore, if a TUQL formula ϕ is insensitive, it cannot be concluded that formulas of the form 3+ϕ or 2+ϕ are insensitive.

Finally, as a consequence of Theorem 14, we show that insensitivity is sufficient to ensure that if formulas are equivalent on infinite traces then they are equivalent on finite traces.

Theorem 16. Let ϕ and ψ be insensitive TUQL formulas. Then ϕ ≡I ψ implies ϕ ≡F ψ.

However, the viceversa does not hold. Consider, e.g., Formula (*), which is trivially insensitive: this formula is equivalent to ⊥ only on finite traces. We can obtain the converse direction using Theorem 10. For instance, 3+P (x)∨3+R(x) and 3+(P(x) ∨ R(x)) are insensitive and I∃ formulas for which equivalence on finite and infinite traces coincides.

Verification. In this section we show how our comparison between finite and infinite traces can be related to the literature on temporal logics for verification. We point out some connections between the finite/infinite trace properties and: (i) the definition of safety in LTL on infinite traces; (ii) some notions related to the construction of monitoring functions in runtime verification.

(i) Safety. Recall that a safety property intuitively asserts that bad things never happen during the execution of a program. In verification, LTL is often used as a specification language for such properties, and the notion of safety is defined accordingly on infinite traces [Sistla, 1994]. Let ϕ be a TUQL formula asserting that some "bad thing" never happens. According to the literature, we say that ϕ denotes a safety property if, whenever ϕ does not hold for an infinite run of a program, then it must be violated already after a finite execution. That is, the infinite trace contains a finite prefix in which the bad thing (the violation of ϕ) has already happened. More formally, we say that a TUQL formula ϕ expresses a safety property iff, for an infinite trace I and an assignment a:

In other words, safety is captured in TUQL by I⇐∀ formulas. In particular, all 2+-formulas of Section 4 are I∀ and thus they express safety properties.

• (ii) Runtime verification. We recall that in runtime verification the task is to evaluate a property with respect to the current history (which is finite at each given instant) of a dynamic system, and to check whether this property is satisfied in all its possible future evolutions [Bauer et al., 2010; Baader and Lippmann, 2014; De Giacomo et al., 2014a]. Here we discuss the relationship between our semantic conditions and the maxims for runtime verification introduced by Bauer et al. 2010, which relate finite trace semantics to the infinite case. The authors suggest that every semantics to be used in runtime verification should satisfy the following requirements.
• Impartiality: never evaluate to true or false a formula on a finite trace, if one of its infinite extensions can possibly change its value.
• Anticipation: if a formula has the same truth value on every infinite extension of a finite trace, then it is equally evaluated also on that finite prefix.

Impartiality cannot be guaranteed for TUQL: 2+P(x) is an example of a formula violating this maxim. On the other hand, 3⊤ is a formula that violates anticipation. Impartiality, as formalised in [Bauer et al., 2010], is captured by F⇒∀ and F⇐∃ properties. Instead, the formal version of anticipation corresponds to properties F⇐∀ and F⇒∃ in our setting. Therefore, any set of TUQL formulas satisfying both impartiality and anticipation should belong to the intersection of F∀ and F∃ formulas. Concerning the possibility to syntactically characterise these formulas, we have that, due to Theorems 12 and 13, impartiality and anticipation are not guaranteed to be preserved for 3+- or 2+-formulas.

Temporal Description Logics. We now consider temporal description logics. We define the temporal language TUALC as a temporal extension of the description logic ALC [Gabbay et al., 2003]. Let NC,NR ⊆ NP be, respectively, sets of unary and binary predicates called concept and role names. A TUALC concept is an expression of the form:

where A ∈ NC and R ∈ NR. A TUALC axiom is either a concept inclusion (CI) of the form C ⊑ D, or an assertion, α, of the form A(a) or R(a, b), where C, D are TUALC concepts, A ∈ NC, R ∈ NR, and a, b ∈ NI. TUALC formulas have the form:

Since a TUALC formula can be mapped into an equisatisfiable TUQL221 formula [Gabbay et al., 2003] we can transfer the upper bounds of Theorems 4 and 5 to TUALC and TUALC; the lower bounds can be obtained in a similar way as in the mentioned theorems. Moreover, from Theorems 6 and 7, we obtain immediately that TUALC on finite traces has both the bounded trace and domain properties.

We now consider the TUALC satisfiability problem on k-bounded traces restricted to global CIs, defined as the fragment of TUALC in which formulas can only be of the form T ∧ 2(T ) ∧ φ, where T is a conjunction of CIs and φ does not contain CIs. The EXPTIME upper bound we provide has a rather challenging proof that uses a form of type elimination [Gabbay et al., 2003; Lutz et al., 2008; Gutiérrez-Basulto et al., 2016], but in a setting where the number of time points is bounded by a natural number k > 0. The main challenge in solving this problem when the number of time points is arbitrarily large but finite is mainly due to the presence of last sub-formulas (i.e., formulas of the form ¬©⊤) that can hold just in the last instant of the model. The complexity is tight since satisfiability in ALC is already EXPTIME-hard [Gabbay et al., 2003].

Theorem 17. TUALC satisfiability is EXPSPACE-complete on finite traces, and NEXPTIME-complete on k-bounded traces. Moreover, TUALC satisfiability on k-bounded traces restricted to global CIs is EXPTIME-complete.

6 Conclusion

We investigated first-order temporal logic over finite traces, studying satisfiability of its two-variable monodic fragment, TUQL221 . While being EXPSPACE-complete over arbitrary finite traces, it lowers down to NEXPTIME in case of TUQL221 , interpreted over traces with at most k time points. Similar results have been shown for a temporal extension of the description logic ALC, with TUALC restricted to global CIs being EXPTIME-complete. Moreover, in an effort to systematically clarify the correlations between finite vs. infinite reasoning we introduced various semantic conditions that allow to formally specify when it is possible to blur the distinction between finite and infinite traces. Grammars for TUQL formulas satisfying some of these conditions have been provided as well. In particular, we have shown that for 3+- and 2+- formulas, equivalence over finite and infinite traces coincide. Some notions used in planning (particularly, insensitivity to infiniteness [De Giacomo et al., 2014b]) and verification have been lifted to the first-order setting, and related to our semantic conditions for blurring the distinction between reasoning over finite and infinite traces.

As future work, we plan to apply the semantic conditions to study the specific case where infinite extensions of finite traces are obtained by repeating the last instant forever [Bauer and Haslum, 2010], as well as to the analysis of monitoring functions for runtime verification [Bauer et al., 2010; Baader and Lippmann, 2014; De Giacomo et al., 2014a]. It would also be interesting to study the precise complexity of the satisfiability problem for TUALC with just global CIs.