Finite vs. Infinite Traces in Temporal Logics

Abstract

The first-order temporal language that we consider in this paper, TU QL [10], is obtained by extending the classical first-order language with the until temporal operator U . This language can be interpreted over infinite linear structures, often based on the strict linear order of the natural numbers, in which case we speak of infinite traces (for more details on syntax and semantics of TU QL, see [3] and references therein). Decidable fragments of first-order temporal logic [11, 10], and in particular temporal description logics [14, 1, 13] (combining linear temporal logic operators with description logics (DLs)) on infinite traces have been extensively investigated as temporal formalisms for knowledge representation. Besides this semantics defined on infinite linear structures, attention has been devoted also to finite traces, which are temporal structures based on time-flows isomorphic to (finite) initial segments of the natural numbers [6, 8, 9]. The finiteness of the time dimension is indeed a natural restriction in many application domains (planning, process modelling, runtime verification, etc.). Moreover, the two semantics behave quite differently, as witnessed by the following examples. The TU QL formula

-

Introduction 2+∀x(P (x)→

2+(¬P (x) ∧ ∃yR(x, y) ∧ P (y))), which admits only models with an infinite domain of objects [ 13 ], is unsatisfiable over finite traces (here 2+ and 3+ are the reflexive versions of the usual future-time operators box 2 and diamond 3, while is the strong next operator). On the other hand, the formula last, defined as ¬ > (or, equivalently, 2⊥), is satisfied only at the last instant of a finite trace, and thus it never holds on models with an infinite ascending chain of instants, while ⊥ cannot be satisfied, neither on finite nor on infinite traces. Therefore, on finite traces, differently from the infinite case, we have that formulas of the form ϕ are not equivalent to ¬ ¬ϕ, and the strong next behaves differently from its weak counterpart, (abbreviating ¬ ¬), for which it holds that ϕ is satisfied at a given instant iff ϕ or last is satisfied.

Given the differences with the infinite case, the main purpose of our line of research is to establish semantic and syntactic conditions which characterise when the distinction between reasoning on finite and infinite traces can be loosened. Several approaches have been considered to preserve the satisfiability of formulas from the finite to the infinite case, so to reuse algorithms developed for the infinite case [ 5, 7 ]. We focus on equivalences between formulas, determining conditions that guarantee when it is preserved from finite to infinite traces, as well as conditions preserving equivalences in the other direction, from infinite to finite traces. This approach opens interesting research directions towards the application of efficient finite traces reasoners [ 12 ] to the infinite case.

After a summary of results contained in a paper published at IJCAI 2019 [ 3 ], where we also provide a uniform framework for semantic notions to bridge finite and infinite trace semantics, in Section 2 below we present original work on formulas for which satisfiability from finite to infinite traces is preserved. Finally, we report in Section 3 previously obtained [ 2, 4, 3 ] complexity results for temporal DLs on finite traces. 2

Finite vs. Infinite Traces There are examples of temporal formulas, such as 2>, that are satisfiable both on finite and infinite traces. Others, however, are satisfiable only on finite traces, witness 3last, or only on infinite traces, as 2+ >. It is then natural to ask under which circumstances we can ensure that satisfiability on finite and infinite traces coincide, so that solvers can limit themselves to the construction of a finite trace and avoid the step of building the lasso of an infinite trace. We are also interested in an analogous question concerning equivalences between formulas. For instance, we have that 32(ϕ ∨ ψ) and 32 ψ, which are not equivalent on infinite traces, are equivalent on finite traces [ 5 ]. Similarly, formulϕas∨23+23+ϕ and 3+2+ϕ are both equivalent to 3+(last ∧ ϕ) on finite traces [ 8 ], but are not equivalent on infinite traces. On the other hand, we have that last is satisfiable on finite traces, thus ⊥ and last turn out to be equivalent only on infinite traces. In the following, we report selected (although slightly rephrased) results from [ 3 ], where we additionally propose a uniform framework of semantic properties that ensure when formula satisfiability and equivalences between formulas are preserved between the finite and the infinite case. The properties help to understand in which cases the distinction between the two can be harmlessly blurred.

We start by observing that, for first-order formulas (FOL) without temporal operators but interpreted on traces, there is no distinction between reasoning over finite or infinite traces.

Theorem 1 (Cf. [3]). Formulas without temporal operators (FOL) are equivalent (resp., satisfiable) on finite traces if, and only if, they are equivalent (resp., satisfiable) on infinite traces.

As a further step, we study cases where diamond and box operators (reflexive or not) are allowed and consider the problem of equivalences between formulas. We provide classes of formulas whose syntactic structure ensures that being equivalent on finite traces implies being equivalent also on infinite traces, or, vice-versa, formulas for which, given their construction, it is guaranteed that equivalences on infinite traces are preserved for the finite case. In the following, given TU QL formulas ϕ, ψ, we write ϕ ≡F ψ (resp., ϕ ≡I ψ) if ϕ is equivalent to ψ on finite (resp., infinite) traces.

Let 3+-formulas ϕ, ψ be constructed according to the following grammar, where P is a predicate: 3+ϕ | ϕ ∨ ψ | ϕ ∧ ψ | ∃xϕ | P (~τ) | ¬P (~τ). 3M+or-feoorvmeru,laws,ewchaillle33-+fo∀r-mfourlmasultahseafroerombutalainsegdenbyeraaltleodwibnyg aalllsoow∀ixnϕg fiunrtthheergr3ammar rule for 3+-formulas. ϕ in the grammar rule for We have the following result for the formulas so constructed.

Theorem 2 (Cf. [3]). The following holds:

1. for all 3+-formulas ϕ, ψ, ϕ ≡F ψ if and only if ϕ ≡I ψ;

2. for all 3+∀-formulas ϕ, ψ, ϕ ≡I ψ implies ϕ ≡F ψ;

3. for all 3-formulas ϕ, ψ, ϕ ≡F ψ implies ϕ ≡I ψ.

In [ 3 ], we provide examples showing that the results of Theorem 2 are tight, meaning that it is not possible to extend the grammar rule for 3+-formulas with ∀xϕ, and we cannot extend the grammar rule for 3+∀-formulas with 3ϕ.

We define now the 2+-formulas ϕ, ψ, constructed according to the rule (with P being a predicate): 2+ϕ | ϕ ∨ ψ | ϕ ∧ ψ | ∀xϕ | P (~τ) | ¬P (~τ).

The set generated by further allowing 2ϕ in the construction of 2+-formulas is the set of 2-formulas, and we call 2+∃-formulas those obtained by allowing ∃xϕ in the grammar rule for 2+-formulas.

Theorem 3 (Cf. [3]). The following holds:

1. for all 2+-formulas ϕ, ψ, ϕ ≡F ψ if and only if ϕ ≡I ψ;

2. for all 2+∃-formulas ϕ, ψ, ϕ ≡I ψ implies ϕ ≡F ψ;

3. for all 2-formulas ϕ, ψ, ϕ ≡F ψ implies ϕ ≡I ψ.

Again, it can be seen in [ 3 ] that the results of Theorem 3 are tight, in that we cannot extend the grammar rule for 2+-formulas with ∃xϕ, and it is not possible to extend the grammar rule for 2+∃-formulas with 2ϕ.

Finally, in the rest of this section (that contains original material), we investigate which fragments of first-order temporal logic have the property that satisfiability on finite traces is preserved on infinite traces. As already mentioned, in these cases, reasoners can be more efficient and avoid the steps to construct the lasso that shows that an infinite trace satisfying a given formula exists.

We show that satisfiability from finite to infinite traces is preserved for a class of formulas containing both 3+ and 2+. Given a finite trace F = (ΔF, (In)n∈[0,l]), we denote by Fω the infinite trace that results from extending F with (Il)ω—an infinite repetition of the last instant Il of F. We say that ϕ is Fω if for all finite traces F and all assignments a, it satisfies: ω =a ϕ.

F |=a ϕ ⇔ F |

Clearly, for any Fω formula ϕ, satisfiability is preserved from finite to infinite traces. Syntactically, we have that this property is satisfied by a class of formulas constructed as follows. Let 3+2+-formulas ϕ, ψ be constructed according to the following rule (with P predicate symbol):

3+ϕ | 2+ϕ | ϕ ∨ ψ | ϕ ∧ ψ | ∃xϕ | ∀xϕ | P (~τ) | ¬P (~τ).

The next theorem shows that the language generated by the grammar rule for 3+2+-formulas contains only formulas whose satisfiability on finite traces implies satisfiability on infinite traces.

+ +-formula is Fω.

Theorem 4. Any 3 2 Proof. Our theorem is a consequence of the following claims, where we write Fn for the suffix of a finite trace F starting from time point n.

Claim 1. For all finite traces F, all assignments a, and all 3+2+-formulas ϕ, if F |=a ϕ then Fω |=a ϕ. Proof of Claim 1. We show that F |=a ϕ implies Fω |=a ϕ. The proof is by induction. For the base case, it is straightforward to see that the statement holds for all formulas of the form P (~τ) and ¬P (~τ), with P predicate symbol. Assume now that the claim holds for ϕ and there is a finite trace F and an assignment a such that F |= ϕ0. We argue that Fω |=a ϕ0, where ϕ0 is as follows.

• oFtohreϕr0w=or3d+s,ϕF:nb|y=aasϕsu. mBpytitohneFin|=duac3ti+veϕ.hyTphoitshmeseias,nsiftFhant|=thaeϕre tihsenn∈(F[0n,)lω] s|=ucahϕt.haStoFF,ωn|=|=aa 3ϕ+. ϕIn. • For ϕ0 = 2+ϕ: by assumption F |=a 2+ϕ. This means that for all n ∈ [0, l] we have that F, n |=a ϕ.

In other words, Fn |=a ϕ for all n ∈ [0, l]. By the inductive hypothesis, for all such n, if Fn |=a ϕ then (Fn)ω |=a ϕ. So Fω |=a 2+ϕ. • For ϕ0 = ∃xϕ: by assumption F |=a ∃xϕ. This means that there is d ∈ Δ such that F |=a[x7→d] ϕ.

By the inductive hypothesis, Fω |=a[x7→d] ϕ. Then, by the semantics of ∃, Fω |=a ∃xϕ. • For ϕ0 = ∀xϕ: by assumption F |=a ∀xϕ. This means that for all d ∈ Δ we have that F |=a[x7→d] ϕ.

By the inductive hypothesis, Fω |=a[x7→d] ϕ for all d ∈ Δ. Then, by the semantics of ∀, Fω |=a ∀xϕ. • The remaining cases can be proved by a straightforward application of the inductive hypothesis. + +-formulas ϕ, if Fω |=a ϕ then F |=a ϕ.

Claim 2. For all finite traces F, all assignments a, and all 3 2

Proof of Claim 2. We show that Fω |=a ϕ implies F |=a ϕ. The proof is by induction. For the base case, it is again easy to check that the statement holds for all formulas of the form P (~τ) and ¬P (~τ), with P predicate symbol. Assume that the claim holds for ϕ and there is a finite trace F and an assignment a such that Fω |= ϕ0. We argue that F |=a ϕ0, where ϕ0 is as follows. • For ϕ0 = 3+ϕ: by assumption Fω |=a 3+ϕ. This means that there is n ∈ [0, ∞) such that Fω, n |=a ϕ. In other words, Fω,n |=a ϕ, where Fω,n is the suffix of Fω starting from time point n. If n ≥ l (the last time point of F) then, by definition of Fω, since Fω,n = Fω,l, we have that Fω,l |=a ϕ. Let Fl be the finite trace with only the last time point of F. As Fω,l = (Fl)ω, we have that (Fl)ω |=a ϕ. By the inductive hypothesis, Fl |=a ϕ. So F |=a 3+ϕ. If n < l then, by the inductive hypothesis, Fn |= ϕ, where Fn is the suffix of F starting from time point n. So F |=a 3+ϕ. • For ϕ0 = 2+ϕ: by assumption Fω |=a 2+ϕ. This means that for all n ∈ [0, ∞) we have that Fω, n |=a ϕ. In other words, Fω,n |=a ϕ for all n ∈ [0, ∞), where Fω,n is the suffix of Fω starting from time point n. For all n ∈ [0, l] (recall that l is the last time point of F), we have that Fω,n = (Fn)ω and so, (Fn)ω |=a ϕ. By applying the inductive hypothesis on all n ∈ [0, l], we conclude that Fn |=a ϕ for all such n. In other words, F, n |=a ϕ for all n ∈ [0, l]. This means that F |=a 2+ϕ. • The remaining cases can be proved by a straightforward application of the inductive hypothesis. 3

Complexity Results We briefly mention here the complexity results recently obtained for different fragments of TU QL [ 2, 4 ]. In [ 2 ], we consider the fragment with a single free variable, unary and binary predicates, and temporal operators applied just to unary predicates (contained in the so-called monodic fragment [ 10 ]), in particular the description logic (DL) TU ALC—the temporal extension of the DL ALC with the until temporal operator on concepts. A TU ALC concept is an expression of the form:

C, D ::= A | ¬C | C u D | ∃R.C | C U D, where A is a concept name (unary predicate) and R is a role name (binary predicate). A TU ALC axiom is either a concept inclusion (CI) of the form C v D, or an assertion of the form A(a) or R(a, b). Formulas in TU ALC have the form: ϕ, ψ ::= α | ¬ϕ | ϕ ∧ ψ | ϕ U ψ, where α is a TU ALC axiom. We studied the complexity of checking satisfiability of formulas in: TU ALC interpreted over finite traces; TU ALC interpreted over k-bounded traces, i.e., finite traces with at most k (given in binary) instants; and in TU (g)ALC, the restriction of TU ALC to global CIs (GCIs), i.e., with formulas only of the form 2+(T ) ∧ φ, where T is a conjunction of CIs (now true at all time points) and φ does not contain CIs, interpreted over k-bounded traces. We obtained the following.

Theorem 5 (Cf. [ 2 ]). Formula satisfiability in TU ALC on finite traces is ExpSpace-complete, while it reduces to NExpTime-complete in TU ALC on k-bounded traces, and to ExpTime-complete in TU (g)ALC on k-bounded traces.

In [ 4 ], we consider temporal extensions of DL-Lite, i.e., the logic TU DL-LitebNool with roles and concepts so defined:

R ::= L | L− | G | G−,

C ::= ⊥ | A | ≥ qR | ¬C | C1 u C2 | C1 U C2 2 where now roles can be either local (L, varying in time) or global (G, not varying in time), and can have inverses (L−, G−). Formulas are as before, with either CIs or GCIs. We consider various FO fragments (core, krom, horn) and the case where just 2, are in front of concepts. We obtain the following. TTExhpeSo(grp)eaDmcLe--L6coitm(eChNpolfre.nte[4o.]n)A.fillnToiwUteiDntgLra-oLcneitlsyeabNGoroeClPIasSn,pdTaUTc(e2g-)cDoDmLL-pL-lLeititteeebN.ohNoolr,nTfUor(gm)uDlLa-Ls aitteiscNofiraeb,iTlit2y o(gn)DfiLni-tLeitetrbNaooclesanids

For traces with at most k time points, given in binary as part of the input, the following holds. Theorem 7 (Cf. [ 4 ]). TU DL-LitebNool and TU DL-LitehNorn formula satisfiability on k-bounded traces are NExpTime-complete. Allowing only GCIs, TU (g)DL-LitecNore and TU (g)DL-LitebNool on k-bounded traces are PSpace-complete.

References

[1] A. Artale and E. Franconi . Temporal description logics . In Handbook of Temporal Reasoning in Artificial Intelligence , pages 375 - 388 . Elsevier, 2005 .

[2] A. Artale , A. Mazzullo , and A. Ozaki . Temporal description logics over finite traces . In 31st International Workshop on Description Logics, (DL'18) , 2018 .

[3] A. Artale , A. Mazzullo , and A. Ozaki . Do you need infinite time? In Proc. of the 28th Int. Joint Conference on Artificial Intelligence (IJCAI-19) , Macao, China, August 10-16 , 2019 . AAAI Press.

[4] A. Artale , A. Mazzullo , and A. Ozaki . Temporal DL-Lite over finite traces (preliminary results) . In 32nd International Workshop on Description Logics, (DL'19) , Oslo, Norway, 18 - 21 June, 2019 .

[5] A. Bauer and P. Haslum . LTL goal specifications revisited . In ECAI , pages 881 - 886 , 2010 .

[6] S. Cerrito , M. C. Mayer , and S. Praud . First order linear temporal logic over finite time structures . In LPAR , pages 62 - 76 , 1999 .

[7] G. De Giacomo , R. De Masellis, and M. Montali . Reasoning on LTL on finite traces: Insensitivity to infiniteness . In AAAI , pages 1027 - 1033 , 2014 .

[8] G. De Giacomo and M. Y. Vardi . Linear temporal logic and linear dynamic logic on finite traces . In IJCAI , pages 854 - 860 , 2013 .

[9] V. Fionda and G. Greco. The complexity of LTL on finite traces: Hard and easy fragments . In AAAI , pages 971 - 977 , 2016 .

[10] D. M. Gabbay , A. Kurucz , F. Wolter , and M. Zakharyaschev. Many-dimensional Modal Logics: Theory and Applications , volume 148 . Elsevier , 2003 .

[11] I. M. Hodkinson , F. Wolter , and M. Zakharyaschev . Decidable fragment of first-order temporal logics . Annals of Pure and Applied Logic , 106 ( 1-3 ): 85 - 134 , 2000 .

[12] J. Li , L. Zhang , G. Pu, M. Y. Vardi , and J. He. LTLf Satisfiability Checking . In ECAI , pages 513 - 518 , 2014 .

[13] C. Lutz , F. Wolter , and M. Zakharyaschev . Temporal description logics: A survey . In TIME , pages 3 - 14 , 2008 .

[14] F. Wolter and M. Zakharyaschev . Temporalizing description logics . In FroCoS , pages 104 - 109 , 1998 .