# do_you_need_infinite_time__c81e7dd6.pdf

Do You Need Inﬁnite Time?

Alessandro Artale , Andrea Mazzullo and Ana Ozaki KRDB Research Centre Free University of Bozen Bolzano {artale, mazzullo, ozaki}@inf.unibz.it

Linear temporal logic over ﬁnite traces is used as a formalism for temporal speciﬁcation in automated planning, process modelling and (runtime) veriﬁcation. In this paper, we investigate ﬁrst-order temporal logic over ﬁnite traces, lifting some known results to a more expressive setting. Satisﬁability in the two-variable monodic fragment is shown to be EXPSPACE-complete, as for the inﬁnite trace case, while it decreases to NEXPTIME when we consider ﬁnite traces bounded in the number of instants. This leads to new complexity results for temporal description logics over ﬁnite traces. We further investigate satisﬁability and equivalences of formulas under a model-theoretic perspective, providing a set of semantic conditions that characterise when the distinction between reasoning over ﬁnite and inﬁnite traces can be blurred. Finally, we apply these conditions to planning and veriﬁcation.

1 Introduction

Since the introduction of linear temporal logic (LTL), several propositional and ﬁrst-order LTL-based formalisms have been developed for applications such as automated planning [Bacchus and Kabanza, 2000; Baier and Mc Ilraith, 2006], process modelling [van der Aalst and Pesic, 2006; Maggi et al., 2011] and veriﬁcation of programs [Manna and Pnueli, 1995]. Related research in knowledge representation has focused on decidable fragments of ﬁrst-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, TUQL2 2 1 , 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 satisﬁability problem ranges from EXPSPACE-complete, for TUQL2 2 1 [Gabbay et al., 2003; Hodkinson et al., 2003], down to NEXPTIMEor 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 deﬁned on inﬁnite linear structures, attention has been devoted also to ﬁnite traces, which are linear temporal structures with only a ﬁnite number of time points [Cerrito et al., 1999; De Giacomo and Vardi, 2013; Fionda and Greco, 2016]. Indeed, the ﬁniteness of the time dimension is a fairly natural restriction. In automated planning, or when modelling business processes with a declarative formalism, we consider ﬁnite 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 veriﬁcation, only the current ﬁnite behaviour of the system is taken into account. Inﬁnite models are then considered to check whether a given requirement is satisﬁed in the inﬁnite extensions of this ﬁnite trace [Giannakopoulou and Havelund, 2001; Bauer et al., 2010]. Although some recent work has considered temporal extensions of DLs in the context of runtime veriﬁcation [Baader and Lippmann, 2014] and business process modelling [van der Aalst et al., 2017], the proposals developed so far are based on the usual inﬁnite trace semantics and are limited in expressivity. This work focuses on ﬁrst-order temporal logic on ﬁnite traces [Cerrito et al., 1999], deﬁned by extending the ﬁrstorder language with temporal operators interpreted on ﬁnite traces. We obtain the following main results.

The complexity of TUQL2 2 1 remains EXPSPACEcomplete on ﬁnite 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 ﬁnite traces, where the complexity further reduces to EXPTIME if only global axioms and ﬁnite traces with a ﬁxed bound on instants are allowed. We establish semantic and syntactic conditions which characterise when the distinction between reasoning on ﬁnite and inﬁnite traces can be completely blurred, providing connections with planning and veriﬁcation. Concerning this last point, several approaches have been con-

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

sidered to preserve satisﬁability of formulas from the ﬁnite to the inﬁnite case, so to reuse algorithms developed for the inﬁnite case [Bauer and Haslum, 2010; De Giacomo et al., 2014b]. Here, we determine conditions that preserve satisﬁability also in the other direction, from inﬁnite to ﬁnite traces. This opens interesting research directions towards the application of efﬁcient ﬁnite traces reasoners [Li et al., 2014] to the inﬁnite case. We provide a uniform framework for these notions, bridging ﬁnite and inﬁnite trace semantics. Full proofs are available in our technical report [Artale et al., 2019].

2 First-order Temporal Logics The ﬁrst-order temporal language, TUQL [Gabbay et al., 2003], is obtained by extending the usual ﬁrst-order language with the temporal operator until (U) interpreted over discrete linear structures, called traces. Syntax The alphabet of TUQL consists of countably inﬁnite 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 quantiﬁer , and the temporal operator U (until). The formulas of TUQL are of the form: ϕ, ψ ::= P( τ) | ϕ | ϕ ψ | xϕ | ϕ U ψ, 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 TUQL2 1 , consists of formulas such that all subformulas of the form ϕ U ψ have at most one free variable. Semantics A ﬁrst-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 ﬁrstorder interpretation with domain M (or simply ): we have P In ar(P ), for each P NP, and a Ii = a Ij for all a NI and i, j N, i.e., constants are rigid designators (with ﬁxed interpretation, denoted simply by a I). 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(τ) = a I, 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 deﬁned as:

M, n |=a P( τ) iff a( τ) P In, M, n |=a ϕ iff not M, n |=a ϕ, M, n |=a ϕ ψ iff M, n |=a ϕ and M, n |=a ψ, M, n |=a xϕ iff M, n |=a ϕ for some assignment a that can differ from a only on x, M, n |=a ϕ U ψ iff m T, m > n: M, m |=a ψ and i (n, m): M, i |=a ϕ.

We say that ϕ is satisﬁed in M (and M is a model of ϕ), writing M |= ϕ, if M, 0 |=a ϕ, for some a. Moreover, ϕ is said to be satisﬁable if it is satisﬁed in some M. A formula ϕ logically implies a formula ψ if every M that satisﬁes ϕ satisﬁes also ψ, and we write ϕ |= ψ. We say that ϕ and ψ are equivalent, writing ϕ ψ, if ϕ |= ψ and ψ |= ϕ. In the following, we call ﬁnite trace a ﬁrst-order temporal interpretation with T = [0, l], often denoted by F = ( F, (Fn)n [0,l]), while inﬁnite traces, based on T = [0, ), will be denoted by I = ( I, (In)n [0, )). We say that a TUQL formula ϕ is satisﬁable on inﬁnite, ﬁnite, or k-bounded traces, if it is satisﬁed in a trace in the class of inﬁnite, ﬁnite, or ﬁnite 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 ﬁnite and an inﬁnite trace s.t. F = I (writing ) and a F = a I, for all a NI. We denote by F I = ( F I, (F In)n [0, )) the extension of F with I, deﬁned as the inﬁnite trace with F I = , a F I = a F, for all a NI, and for P NP, n N:

P F In = P Fn, if n [0, l] P In (l+1), if n [l + 1, ).

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 ﬁnite traces, last is satisﬁable in the last time point.

3 Satisﬁability over Finite Traces

In the following we show how to reduce the formula satisﬁability problem over ﬁnite traces to the same problem over inﬁnite traces. Similar to the encoding proposed in [De Giacomo and Vardi, 2013] for propositional LTL, to capture the ﬁniteness 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:

ψf1 = x E(x) (Point (i)), ψf2 = ( x E(x)) U ( x E(x)) (Points (ii), (iii)), ψf3 = 2 x(E(x) E(x)) (Point (iv)).

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 ﬁnite and an inﬁnite trace with the same domain and such that a F = a I, for all a NI. We denote by F E I the end extension of F with I, deﬁned as the extension F I, for all P NP \ {E}, such that:

EF EIn = , if n [0, l] , if n [l + 1, )

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

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

Lemma 1. For every inﬁnite trace I, I |= ψf iff I = F E I , for some ﬁnite trace F and some inﬁnite trace I . We now introduce a translation for TUQL formulas, used together with the end of time formula, ψf, to capture satisﬁability on ﬁnite traces. More formally, a TUQL formula ϕ is satisﬁable on ﬁnite traces if and only if its translation ϕ is satisﬁed in an inﬁnite trace that also satisﬁes the formula ψf. The translation is deﬁned as:

(P( τ)) 7 P( τ), ( ϕ) 7 ϕ ,

(ϕ ψ) 7 ϕ ψ , ( xϕ) 7 xϕ ,

(ϕ U ψ) 7 ϕ U (ψ ψf1).

Lemma 2 states the correctness of . Lemma 2. Let F E I be an end extension of a ﬁnite 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 satisﬁability problem to the same problem for TUQL. Theorem 3. Let ϕ be a TUQL formula. Then ϕ is satisﬁable on ﬁnite traces iff ϕ ψf is satisﬁable on inﬁnite traces. We use the translation to transfer the EXPSPACE upper bound for TUQL2 2 1 over inﬁnite traces to ﬁnite traces [Hodkinson et al., 2003]. The lower bound can be proved using similar ideas as those used to prove hardness of TUQL2 2 1 .

Theorem 4. TUQL2 2 1 satisﬁability on ﬁnite traces is EXPSPACE-complete. We now study TUQL2 2 1 satisﬁability 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 satisﬁability problem decreases from EXPSPACE to NEXPTIME. Hardness follows from the fact that: (1) one can translate ALC-LTL with rigid concepts to TUQL2 2 1 ; and (2) satisﬁability in ALC-LTL with rigid concepts on k-bounded traces is NEXPTIME-hard, as for inﬁnite 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 certiﬁcate for the existence of a quasimodel (and therefore a model) for the input formula.

Theorem 5. TUQL2 2 1 satisﬁability on k-bounded traces is NEXPTIME-complete. We end this section by establishing that TUQL2 2 1 on ﬁnite traces enjoys the bounded trace property and the bounded domain property. If there is a ﬁnite trace which satisﬁes a TUQL2 2 1 formula ϕ then there is a ﬁnite 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 ﬁnite non-repeting sequence of states is correlated with the number

of time points in a ﬁnite trace. The number of distinct states of a TUQL2 2 1 formula on ﬁnite traces is the same as in the inﬁnite case, where it is known to be double exponential [Gabbay et al., 2003]. This directly implies that TUQL2 2 1 enjoys the bounded trace property. Theorem 6. TUQL2 2 1 satisﬁability of ϕ on ﬁnite traces implies TUQL2 2 1 satisﬁability of ϕ on k-bounded traces, with k double exponential in |ϕ|.

We now establish that a TUQL2 2 1 formula has the bounded domain property: if it is satisﬁable, 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. TUQL2 2 1 satisﬁability of ϕ on k-bounded traces implies the existence of a model with domain size exponential in k and ϕ. Since TUQL2 2 1 satisﬁability on ﬁnite traces implies satisﬁability on k-bounded traces, for some k > 0, the formula

2+ x(P(x) 2+( P(x) y R(x, y) P(y))), (*)

which only admits models with an inﬁnite domain [Lutz et al., 2008], is unsatisﬁable over ﬁnite traces.

4 Finite vs. Inﬁnite Traces While certain formulas, such as 2 , are satisﬁable both on ﬁnite and inﬁnite traces, others, e.g., 3last and 2+ , are only satisﬁable on ﬁnite traces and on inﬁnite traces, respectively. One then wonders, when does satisﬁability on ﬁnite and inﬁnite traces coincide, so that solvers can simply stop trying to build the lasso of an inﬁnite trace when a ﬁnite 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 ﬁnite traces but not on inﬁnite traces [Bauer and Haslum, 2010]. Moreover, 2+3+ϕ and 3+2+ϕ are not equivalent on inﬁnite traces, whereas on ﬁnite traces they are both equivalent to 3+(last ϕ) [De Giacomo and Vardi, 2013]. Conversely, and last are only equivalent on inﬁnite traces. In this section we address these questions and investigate the distinction between reasoning on ﬁnite and on inﬁnite traces. More speciﬁcally, we propose semantic properties which guarantee that formula satisﬁability and equivalences between formulas are preserved, and thus, the distinction can be blurred. Given a ﬁnite trace F, we deﬁne the set of extensions of F as the set Ext(F) = {I | I = F I , for some I }. Instead, given an inﬁnite trace I, the set of preﬁxes of I is the set Pre(I) = {F | I = F I , for some I }. For a TUQL formula ϕ and a quantiﬁer Q { , }, we say that ϕ is FQ if, for all ﬁnite traces F and all assignments a, it satisﬁes the ﬁnite trace property:

F |=a ϕ QI Ext(F).I |=a ϕ,

and, similarly, ϕ is IQ if, for all inﬁnite traces I and all assignments a, it satisﬁes the inﬁnite trace property:

I |=a ϕ QF Pre(I).F |=a ϕ.

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

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

Property Formulas

F 3+last 3P(x); 3+last 3P(x) (*).

F 3+P(x); 3+P(x) (*).

I 2 last; 2 last.

I 2+P(x) 3+(P(x) last); 2+P(x) 3+(P(x) last).

Table 1: Formulas satisfying exactly one of the ﬁnite/inﬁnite 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 quantiﬁers 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 ﬁnite traces can be translated into equisatisﬁable formulas on inﬁnite traces. Such translation is not always needed, since for some classes of formulas satisﬁability is already preserved. Indeed, for a TUQL formula ϕ: if ϕ is F , then it is satisﬁable on ﬁnite traces only if it is satisﬁable on inﬁnite traces; moreover, if ϕ is I , then it is satisﬁable on inﬁnite traces only if it is satisﬁable on ﬁnite 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 inﬁnite traces, and ϕ F ψ if they are equivalent on ﬁnite traces. The following theorem provides sufﬁcient conditions to preserve formula equivalence from the inﬁnite to the ﬁnite 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 inﬁnite traces. Also, 2+P(x) 3+(P(x) last) and 2+P(x) 3+(P(x) last) are I , and equivalent on inﬁnite but not on ﬁnite traces. This example also shows that the condition I alone is not sufﬁcient for Theorem 9. Moreover, F alone is also not sufﬁcient. To see this, consider, e.g., 2+3 (P(x) 3last) and 2+3 (3last) , which are F but are equivalent only over inﬁnite traces. We now present sufﬁcient conditions to preserve equivalences from the ﬁnite to the inﬁnite 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 sufﬁcient to ensure that formula equivalence on ﬁnite traces implies formula equivalence on inﬁnite 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 ﬁnite 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 ﬁnite traces. This example also shows that the condition F alone is not sufﬁcient for Theorem 10. We now argue that I alone is also not sufﬁcient. To see this, consider, e.g., (P(x) 2+3 ) 3last and 2+3 3last, which are I but are equivalent only on ﬁnite 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 ﬁnite and inﬁnite 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 ﬁnite/inﬁnite trace properties F , F , I , and I . 3+-formulas ϕ, ψ are built according to (with P NP):

3+ϕ | ϕ ψ | ϕ ψ | xϕ | P( τ) | P( τ)

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 inﬁnite (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 ﬁnite preﬁx where x3+P(x) holds.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

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

2+ϕ | ϕ ψ | ϕ ψ | xϕ | P( τ) | P( τ)

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 inﬁnite (and countable) domain, where each element is in P at a speciﬁc time point n N. The formula x2+ P(x) holds in every ﬁnite preﬁx but it does not hold in this inﬁnite trace. It follows from our results that there is no distinction between reasoning on ﬁnite and inﬁnite 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 ﬁnite traces, and so, the distinction between reasoning on ﬁnite and inﬁnite 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 ﬁnite and inﬁnite traces can be safely blurred, is of interest for several applications. Here we show how it can be related to planning and veriﬁcation. Moreover, for knowledge representation scenarios, we introduce temporal DLs on ﬁnite traces, providing complexity results for the satisﬁability problem.

Planning. In automated planning, the sequence of states generated by actions is usually ﬁnite [Cerrito and Mayer, 1998; Bauer and Haslum, 2010; De Giacomo and Vardi, 2013; De Giacomo et al., 2014b]. To reuse temporal logics based on inﬁnite traces for specifying plan constraints, one approach, developed by De Giacomo et al. 2014b for LTL, is based on the notion of insensitivity to inﬁniteness. This property is meant to capture those formulas that can be equivalently interpreted on inﬁnite 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 ﬁrst-order temporal setting, and to provide a characterisation analogous to the propositional one, we introduce the following deﬁnitions. Let F = ( F, (Fn)n [0,l]) be a ﬁnite trace, and let E = ( E, (En)n [0, )) be the inﬁnite trace such that E = F

(we write just ), a E = a F 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 inﬁniteness (or simply insensitive) if, for every

ﬁnite 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 ﬁnite 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 deﬁnition of ψf, we deﬁne χf = ψf χf1, with

χf1 = 2 x y(E(x)

P Σ\{E} P(x, y)).

The next characterisation result extends Theorem 4 in [De Giacomo et al., 2014b] to TUQL. Theorem 14. A TUQL formula ϕ is insensitive to inﬁniteness iff χf |= ϕ ϕ holds on inﬁnite traces. Insensitive formulas allow us to blur the distinction between ﬁnite and inﬁnite traces as soon as inﬁnite traces satisfy χf. Thus, we can check satisﬁability of insensitive TUQL2 2 1 (or other decidable languages) formulas on ﬁnite traces by using satisﬁability algorithms for the inﬁnite 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 sufﬁcient to ensure that if formulas are equivalent on inﬁnite traces then they are equivalent on ﬁnite 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 ﬁnite 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 ﬁnite and inﬁnite traces coincides.

Veriﬁcation. In this section we show how our comparison between ﬁnite and inﬁnite traces can be related to the literature on temporal logics for veriﬁcation. We point out some connections between the ﬁnite/inﬁnite trace properties and: (i) the deﬁnition of safety in LTL on inﬁnite traces; (ii) some notions related to the construction of monitoring functions in runtime veriﬁcation. (i) Safety. Recall that a safety property intuitively asserts that bad things never happen during the execution of a program. In veriﬁcation, LTL is often used as a speciﬁcation

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

language for such properties, and the notion of safety is deﬁned accordingly on inﬁnite 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 inﬁnite run of a program, then it must be violated already after a ﬁnite execution. That is, the inﬁnite trace contains a ﬁnite preﬁx 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 inﬁnite trace I and an assignment a:

( F Pre(I).F |=a ϕ) I |=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 veriﬁcation. We recall that in runtime veriﬁcation the task is to evaluate a property with respect to the current history (which is ﬁnite at each given instant) of a dynamic system, and to check whether this property is satisﬁed 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 veriﬁcation introduced by Bauer et al. 2010, which relate ﬁnite trace semantics to the inﬁnite case. The authors suggest that every semantics to be used in runtime veriﬁcation should satisfy the following requirements. Impartiality: never evaluate to true or false a formula on a ﬁnite trace, if one of its inﬁnite extensions can possibly change its value. Anticipation: if a formula has the same truth value on every inﬁnite extension of a ﬁnite trace, then it is equally evaluated also on that ﬁnite preﬁx. 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 deﬁne 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:

C, D ::= A | C | C D | R.C | C U D,

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:

ϕ, ψ ::= α | C D | ϕ | ϕ ψ | ϕ U ψ.

Since a TUALC formula can be mapped into an equisatisﬁable TUQL2 2 1 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 ﬁnite traces has both the bounded trace and domain properties. We now consider the TUALC satisﬁability problem on k-bounded traces restricted to global CIs, deﬁned 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 ﬁnite 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 satisﬁability in ALC is already EXPTIME-hard [Gabbay et al., 2003]. Theorem 17. TUALC satisﬁability is EXPSPACE-complete on ﬁnite traces, and NEXPTIME-complete on k-bounded traces. Moreover, TUALC satisﬁability on k-bounded traces restricted to global CIs is EXPTIME-complete.

6 Conclusion We investigated ﬁrst-order temporal logic over ﬁnite traces, studying satisﬁability of its two-variable monodic fragment, TUQL2 2 1 . While being EXPSPACE-complete over arbitrary ﬁnite traces, it lowers down to NEXPTIME in case of TUQL2 2 1 , 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 ﬁnite vs. inﬁnite reasoning we introduced various semantic conditions that allow to formally specify when it is possible to blur the distinction between ﬁnite and inﬁnite 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 ﬁnite and inﬁnite traces coincide. Some notions used in planning (particularly, insensitivity to inﬁniteness [De Giacomo et al., 2014b]) and veriﬁcation have been lifted to the ﬁrst-order setting, and related to our semantic conditions for blurring the distinction between reasoning over ﬁnite and inﬁnite traces. As future work, we plan to apply the semantic conditions to study the speciﬁc case where inﬁnite extensions of ﬁnite traces are obtained by repeating the last instant forever [Bauer and Haslum, 2010], as well as to the analysis of monitoring functions for runtime veriﬁcation [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 satisﬁability problem for TUALC with just global CIs.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)

References [van der Aalst and Pesic, 2006] Wil van der Aalst and Maja Pesic. Decserﬂow: Towards a truly declarative service ﬂow language. In WS-FM, pages 1 23, 2006. [van der Aalst et al., 2017] Wil van der Aalst, Alessandro Artale, Marco Montali, and Simone Tritini. Object-centric behavioral constraints: Integrating data and declarative process modelling. In DL, volume 1879, 2017. [Artale and Franconi, 2005] Alessandro Artale and Enrico Franconi. Temporal description logics. In Handbook of Temporal Reasoning in Artiﬁcial Intelligence, pages 375 388. Elsevier, 2005. [Artale et al., 2014] Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, and Michael Zakharyaschev. A cookbook for temporal conceptual data modelling with description logics. ACM Trans. Comput. Log., 15(3):25:1 25:50, 2014. [Artale et al., 2019] Alessandro Artale, Andrea Mazzullo, and Ana Ozaki. Do you need inﬁnite time? Technical Report 01, Free University of Bozen-Bolzano, 2019. Available at https://www.inf.unibz.it/krdb/KRDB%20ﬁles/ tech-reports/KRDB19-01.pdf. [Baader and Lippmann, 2014] Franz Baader and Marcel Lippmann. Runtime veriﬁcation using the temporal description logic ALC-LTL revisited. J. Applied Logic, 12(4):584 613, 2014. [Baader et al., 2012] Franz Baader, Silvio Ghilardi, and Carsten Lutz. LTL over description logic axioms. ACM Trans. Comput. Log., 13(3), 2012. [Bacchus and Kabanza, 2000] Fahiem Bacchus and Froduald Kabanza. Using temporal logics to express search control knowledge for planning. Artif. Intell., 116(1-2):123 191, 2000. [Baier and Mc Ilraith, 2006] Jorge A. Baier and Sheila A. Mc Ilraith. Planning with ﬁrst-order temporally extended goals using heuristic search. In AAAI, pages 788 795, 2006. [Bauer and Haslum, 2010] Andreas Bauer and Patrik Haslum. LTL goal speciﬁcations revisited. In ECAI, pages 881 886, 2010. [Bauer et al., 2010] Andreas Bauer, Martin Leucker, and Christian Schallhart. Comparing LTL semantics for runtime veriﬁcation. J. Log. Comput., 20(3):651 674, 2010. [Camacho et al., 2017] Alberto Camacho, Eleni Triantaﬁllou, Christian J. Muise, Jorge A. Baier, and Sheila A. Mc Ilraith. Non-deterministic planning with temporally extended goals: LTL over ﬁnite and inﬁnite traces. In AAAI, pages 3716 3724, 2017. [Cerrito and Mayer, 1998] Serenella Cerrito and Marta Cialdea Mayer. Bounded model search in linear temporal logic and its application to planning. In TABLEAUX, pages 124 140, 1998. [Cerrito et al., 1999] Serenella Cerrito, Marta Cialdea Mayer, and Sébastien Praud. First order linear temporal logic over ﬁnite time structures. In LPAR, pages 62 76, 1999.

[De Giacomo and Vardi, 2013] Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on ﬁnite traces. In IJCAI, pages 854 860, 2013. [De Giacomo et al., 2014a] Giuseppe De Giacomo, Riccardo De Masellis, Marco Grasso, Fabrizio Maria Maggi, and Marco Montali. Monitoring business metaconstraints based on LTL and LDL for ﬁnite traces. In BPM, pages 1 17, 2014. [De Giacomo et al., 2014b] Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. Reasoning on LTL on ﬁnite traces: Insensitivity to inﬁniteness. In AAAI, pages 1027 1033, 2014. [Fionda and Greco, 2016] Valeria Fionda and Gianluigi Greco. The complexity of LTL on ﬁnite traces: Hard and easy fragments. In AAAI, pages 971 977, 2016. [Gabbay et al., 2003] Dov M. Gabbay, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Many-dimensional Modal Logics: Theory and Applications, volume 148. Elsevier, 2003. [Giannakopoulou and Havelund, 2001] Dimitra Giannakopoulou and Klaus Havelund. Automata-based veriﬁcation of temporal properties on running programs. In ASE, pages 412 416, 2001. [Gutiérrez-Basulto et al., 2016] Víctor Gutiérrez-Basulto, Jean Christoph Jung, and Ana Ozaki. On metric temporal description logics. In ECAI, pages 837 845, 2016. [Hodkinson et al., 2000] Ian M. Hodkinson, Frank Wolter, and Michael Zakharyaschev. Decidable fragment of ﬁrstorder temporal logics. Annals of Pure and Applied Logic, 106(1-3):85 134, 2000. [Hodkinson et al., 2003] Ian M. Hodkinson, Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. On the computational complexity of decidable fragments of ﬁrst-order linear temporal logics. In TIME-ICTL, pages 91 98, 2003. [Li et al., 2014] Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. LTLf Satisﬁability Checking. In ECAI, pages 513 518, 2014. [Lutz et al., 2008] Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Temporal description logics: A survey. In TIME, pages 3 14, 2008. [Maggi et al., 2011] Fabrizio Maria Maggi, Marco Montali, Michael Westergaard, and Wil M. P. van der Aalst. Monitoring business constraints with linear temporal logic: An approach based on colored automata. In BPM, pages 132 147, 2011. [Manna and Pnueli, 1995] Zohar Manna and Amir Pnueli. Temporal veriﬁcation of reactive systems - Safety. Springer, 1995. [Sistla, 1994] A. Prasad Sistla. Safety, liveness and fairness in temporal logic. Formal Asp. Comput., 6(5):495 512, 1994. [Wolter and Zakharyaschev, 1998] Frank Wolter and Michael Zakharyaschev. Temporalizing description logics. In Fro Co S, pages 104 109, 1998.

Proceedings of the Twenty-Eighth International Joint Conference on Artiﬁcial Intelligence (IJCAI-19)