Combining DL-Lite_{bool}^N with Branching Time: A gentle Marriage

1 Introduction

Over the last 25 years, plenty of extensions of classical description logics (DLs) with an explicit temporal component have been investigated. The study of temporal DLs (TDLs) is motivated by the fact that, arguably, in almost every domain where ontologies are used many terms are described and classified based on certain temporal patterns. For instance, in the biomedical domain, where DL-ontologies are commonly used, diseases or findings are defined according to the evolution of specific symptoms or the repetition of certain patterns over time [Shankar et al., 2008; O'Connor et al., 2009; Crowe and Tao, 2015]. Another prominent application of TDLs is the representation of and reasoning about temporal conceptual data models (TCMs) [Artale et al., 2007b; 2011; 2014] introduced in the context of temporal databases as extensions of classical conceptual models such as ER and UML.

The most popular approach to TDLs is to combine DLs with traditional temporal logics such as LTL or CTL∗ and provide a two-dimensional semantics, one dimension for time and the other for DL quantification, in the style of manydimensional modal logics [Gabbay et al., 2003]. In the construction of this kind of TDLs there are a number of design choices, depending on the desired level of interaction between the component logics. For example, we can choose whether temporal operators are applied to concepts, roles or TBox and ABox axioms. Unfortunately, many TDLs become undecidable if they allow to reason about the temporal evolution of both roles and concepts [Artale et al., 2007a;

∗Guti´errez-Basulto was funded by the EU's Horizon 2020 programme under the Marie Skłodowska-Curie grant No 663830.

Jean Christoph Jung

Universit¨at Bremen, Germany jeanjung@informatik.uni-bremen.de

Lutz et al., 2008; Guti´errez-Basulto et al., 2014]. In fact, these undecidability results hold already if roles are declared rigid (not changing their interpretation over time), the temporal operators available are heavily restricted and the lightweight sub-Boolean DL EL is used. On the other hand, in their seminal work, Artale et al. [2007a] showed that TDLs based on LTL and members of the family of lightweight DLs DL-Lite [Artale et al., 2009] can support rigid roles and temporal concepts without compromising decidability. Furthermore, it was recently shown [Artale et al., 2014] that this type of TDLs, besides being complexity-wise well-behaved, are well-suited to encode many important aspects of TCMs.

The purpose of this paper is to make further progress in the study of temporal extensions of DL-Lite. We are particularly interested in setting the basis for the development of a finegrained analysis of TDLs based on DL-Lite and the branching temporal logics CTL∗ and CTL. To this aim, we investigate combinations of the expressive member DL-LiteNbool of DL-Lite with CTL∗ and CTL, and provide algorithms for the satisfiability problem and (mostly tight) complexity bounds. We believe the obtained results are important because the understanding of this kind of TDLs was very limited; indeed, only initial results were available [Guti´errez-Basulto et al., 2014]. Moreover, in the light of the results by Artale et al. [2014] above, these TDLs might be well-suited to encode TCMs incorporating branching time to capture various versions of the different components of conceptual schemas over time [Golendziner and dos Santos, 1995; Moro et al., 2001; de Matos Galante et al., 2005], or version document models, also requiring branching time [Noronha et al., 1998; Weitl et al., 2009].

We look at two types of combinations: (i) CTL∗-Lite Nbool and CTL-Lite Nbool with rigid roles in the case where temporal operators are applied to concepts and temporal ABox assertions of certain shape are allowed, too. (ii) we look again at the TDLs in (i), but additionally temporal operators can be applied to Boolean combinations of concept inclusions and ABox assertions. For both types of combinations, we develop a uniform algorithm (working for both CTL and CTL∗ -based TDLs) for satisfiability based on a combination of type-based abstractions and tree automata. This approach to satisfiability was originally introduced in [Guti´errez-Basulto et al., 2012] for combinations of CTL and CTL∗ with ALC; here, we extend and adapt it to deal with ABoxes, unqualified number restrictions and rigid roles. Note that, as discussed, if rigid roles are allowed in qualified existential restrictions, already combinations of sub-fragments of CTL with the sub-logic EL of ALC are undecidable [Guti´errez-Basulto et al., 2014].

Our results are as follows: For combinations of type (i), we develop a uniform algorithm for knowledge base satisfiability based on a combination of type-elimination with automatatheoretic approaches to temporal reasoning in CTL and CTL∗ , yielding tight 2EXPTIME and EXPTIME upper bounds for CTL∗-Lite Nbool and CTL-Lite Nbool , respectively. For combinations of type (ii), we devise a uniform approach to formula satisfiability that combines type-based abstractions, nondeterministic automata for CTL and CTL∗, and two-way alternating tree automata. We obtain 3EXPTIME and 2EXPTIME upper bounds for CTL∗-Lite Nbool - and CTL-Lite Nbool formulas, respectively. For CTL-Lite Nbool , we get a matching lower bound.

We note in passing that previously developed techniques for combinations of LTL with DL-LiteNbool cannot be straightforwardly adapted to the branching case. For combinations of type (i), upper bounds cannot be obtained by adapting the two-step technique developed by Artale et al. [2014] because the second step of such technique relies on the past being unbounded, which is not the standard semantics for CTL and CTL∗ . For combinations of type (ii), elementary upper bounds cannot be derived by providing a satisfiability preserving translation into (a decidable sub-fragment of) the one-variable fragment of first-order branching temporal logic [Hodkinson et al., 2002] because (to our knowledge) no elementary complexity bounds are known. In contrast, for LTL-LiteNbool formulas tight upper bounds are obtained via a satisfiability preserving translation into the one-variable fragment of first-order temporal logic [Artale et al., 2007a].

An extended version with an appendix can be found in http://tinyurl.com/ktkgwqg.

2 Preliminaries

Syntax. We introduce the TDLs CTL∗-Lite Nbool and CTL-Lite Nbool based on the DL DL-Lite Nbool . We consider a vocabulary of countably infinite disjoint sets of concept names NC, role names NR and individual names NI, and assume that NR is partitioned into two countably infinite sets of rigid role names Nrig and local role names Nloc. CTL∗-Lite Nbool -state concepts C,D and CTL∗-Lite Nbool -path concepts C, D are defined by the following grammar:

with A ∈ NR, r ∈ {s, s- | s ∈ NR} a role, C,D state concepts, C, D path concepts and n a positive integer given in binary. CTL-LiteNbool is the fragment of CTL∗-Lite Nbool in which temporal operators ©,□, U must be immediately preceded by the path quantifier E. From now on, the term concept refers to a state concept.

Roles and concepts of the form r- and ≥ n r are called inverse roles and number restrictions, respectively. We identify r- with s ∈ NR if r = s-, use standard abbreviations ⊤, ⊥, C ⊔ D, C → D, ∃r and ≤ n r, and temporal abbreviations AC = ¬E¬C and ♦C = ¬□¬C. In CTL-Lite Nbool the abbreviations A©C, ACUD, E♦C and A♦C are defined as in CTL [Clarke and Emerson, 1981] - cf. appendix.

A CTL∗-Lite Nbool TBox T is a finite set of concept inclusions (CIs) C ⊑ D with C,D CTL∗-Lite Nbool concepts 1 - CTL-Lite Nbool TBoxes are defined analogously. An ABox A is a finite set of concept assertions and role assertions of the form

where P ∈ {A,E}, A ∈ NC, s ∈ NR, {a, b} ⊆ NI and (P©)i denotes P© i times, with i given in unary. To avoid clunky notation, from here on, we write P©i instead of (P©)i . Moreover, we assume wlog. that E©i s(a, b) ̸∈ A if A©i s(a, b) ∈ A. A knowledge base (KB) K is a pair (T , A).

We use ind(A), CN(K), Rol(K) to denote, respectively, the set of all (i) individual names occurring in A, (ii) concept names occurring in K, (iii) role names occurring in K and their inverses; and Rolrig/loc(K), ♯rT and ♯A to denote, respectively, (iv) the subset of rigid/local roles of Rol(K), (v) the set containing 1 and all numbers n such that ≥ n r occurs in T and (vi) all numbers 0 ≤ n ≤ i such that ©iα occurs in A.

Semantics. An interpretation I based on an infinite tree T = (W,E) is a structure (∆I , (Iw)w∈W), where each Iw is a classical DL interpretation with domain ∆I , that is, for each w ∈ W we have aIw ∈ ∆I , AIw ⊆ ∆I , and rIw ⊆ ∆I×∆I . We additionally require that the interpretations of a rigid role name is the same at all w ∈ W. Moreover, we make the two common assumptions constant domain assumption (CDA), that is, all w ∈ W share the same domain ∆I , and standard name assumption, that is, we assume aIw = a for all a ∈ ind(A), w ∈ W. From here on, we usually write AI,w instead of AIw , and refer to nodes in T as time points or worlds.

For a path π = w0w1w2 · · · in T, we write π[i] for wi, π[i..] for the path wiwi+1 · · · and use Paths(w) to denote the set of all paths starting at node w. The mapping ·I,w is then extended from concept names and role names as follows:

where C I,π refers to the extension of CTL∗-Lite Nbool -path concepts on a given path π, defined as:

1 Inclusions between path concepts are not admitted since they lead to undecidability [Hodkinson et al., 2002; Lutz et al., 2008].

The satisfaction relation |= is defined as follows, where ε is the root world and ∗ stands for all if P = A and for some if P = E.

An interpretation I is a model of a TBox T , written I |= T , if I |= α for all α ∈ T , and it is a model of an ABox A, written I |= A, if I |= α for all α ∈ A. Thus, a TBox T is interpreted globally and ABox assertions are interpreted with respect to the root world ε. Finally, I is a model of a KB K = (T , A), denoted by I |= K, if I |= T and I |= A.

Fragments. We consider the sub-language CTL-Litehorn of CTL-Lite Nbool that disallows the constructor ¬ (and thus abbreviations C ⊔ D, etc) and numbers n ≥ 2 in number restrictions ≥ n r. In this context, we see the operator A© as a primitive instead of as an abbreviation.

Reasoning Problem. We are interested in the knowledge base satisfiability problem: given a KB K, determine whether there exists an interpretation I such that I |= K.

3 KB Satisfiability in CTL- &CTL∗-Lite Nbool

We next devise an algorithm for the KB satisfiability problem in CTL- & CTL∗-Lite Nbool , yielding tight EXPTIME and 2EXPTIME upper bounds, respectively. The lower bounds are inherited from CTL and CTL∗ [Fischer and Ladner, 1979; Vardi and Stockmeyer, 1985]. We present for both TDLs a uniform approach to satisfiability that amalgamates Prattstyle type elimination [Pratt, 1979] with automata-based techniques for temporal logics [Kupferman and Vardi, 2005; Vardi, 2006]. We particularly use the fact that for deciding whether a (propositional) CTL or CTL∗ formula ϕ is satisfiable, one can construct a nondeterministic B¨uchi tree automaton (NBTA) Aϕ that accepts all (tree) models of ϕ, and then check whether any tree is accepted by Aϕ, see appendix for details. The overall approach is sanctioned by the rather limited interaction between the temporal and DL dimensions, which allows us to 'independently' reason about the temporal evolution of each domain element, and then use all such one-dimensional temporal models to construct a single twodimensional one.

In the rest of the paper, we use standard terminology for trees [Vardi, 1998]. We will say that a tree T is k-ary, k ≥ 1, if every node of T has exactly k successors. Let Σ be a finite alphabet. A Σ-labelled tree is a pair (T, τ) with T a tree and τ : W → Σ assigns a letter from Σ to each node.

Let K = (T , A) be the KB whose satisfiability is to be decided, with T formulated in CTL-Lite Nbool or CTL∗-Lite Nbool . We assume wlog. that T is of the form {⊤ ⊑ CT } and that if P©i s(a, b) ∈ A then P©i s-(b, a) ∈ A, and use ccl(K) to denote the concept closure under subconcepts and single negation of {CT } ∪ {C | C(a) ∈ A} ∪ {∃r | r ∈

Rol(K)} ∪ {P©i ≥ n r | P©i r(a, b) ∈ Arol ∧ n ∈ ♯rT } where Arol = {P©j R(a, b) | P©i R(a, b) ∈ A, j ≤ i} with R of the form r or ¬r.

A concept type for K is a set t ⊆ ccl(K) such that (i) CT ∈ t and (ii) if ≥ n r ∈ t, then ≥ m r ∈ t, for all m ∈ ♯rT with m < n; and tp(K) denotes the set of all concept types for K. An ABox type for K is a pair (t, a) with t ⊆ ccl(K) ∪ Arol and a ∈ ind(A) such that t satisfies (i)-(ii) above and (iii) if P©iR(b, c) ∈ t, then b = a or c = a; and atp(K) denotes the set of all ABox types for K. From here on, we write ta instead of (t, a) and use α ∈ ta to denote that α ∈ t. We say type for K to refer to either a concept or ABox type for K, and freely use ≥ 1 r or ∃r. If no confusion arises, we omit the name a in ta and write t.

We now introduce the temporal component in our typebased abstraction. A temporal type for K is a pair (t, i) where t ∈ tp(K) ∪ atp(K) is a type for K and i ≥ 0 denotes the distance of a world w from the root time point. For any n0 ≥ 0, ttpn0 (K) denotes the set of all temporal types (t, i) for K with i ≤ n0.

As the next step, in order to use the automata machinery for temporal reasoning, we surrogate the 'DL-component' from our logics. We start by introducing a surrogation on types that will allow us to use them as an alphabet of models of the (propositional) temporal formulas defined below. For a type t, let ¯ t denote the result of replacing (i) every C ∈ t, C ̸∈ CN(K), with a fresh propositional variable XC, and (ii) every β = P©iR(a, b) ∈ t with a fresh propositional variable Xβ. Let cn be the set of resulting propositional variables, including CN(K). As the final step, we surrogate concepts and role assertions so as to obtain temporal formulas. For C ∈ ccl(K), ¯ C denotes the result of replacing in C every subconcept ≥ n r with Xn r and ⊓ with ∧; for β = P©iR(a, b) ∈ Arol, ¯ β denotes the result of replacing in β R(a, b) with XR(a,b).

We are now ready to describe the overall decision procedure, we will establish later on an appropriate n0 bound. Our algorithm performs type-elimination, similar to what has been done for combinations (without rigid roles and ABoxes) of ALC with CTL and CTL∗ [Guti´errez-Basulto et al., 2012]. The algorithm starts with the set S0 = ttpn0 (K) and obtains the set Sj+1 from Sj by removing temporal types that, intuitively, cannot appear in any model of K: A temporal type (ta, i) is eliminated from Sj if it is not realisable in Sj . Abusing notation, in the next definition ta denotes a concept or ABox type; in the former case, the subindex a is vacuous.

Definition 1. A temporal type (ta, i) is realisable in Sj if it satisfies the following conditions.

1. (ta, i) is DL-realisable in Sj, that is, if ≥ n r ∈ ta, then there is a (t′ , i) ∈ Sj with t′ ∈ tp(K) and (∃r-) ∈ t′ ;
2. (ta, i) is temporally realisable in Sj, that is, there is a 2cn -labelled ♯E(K)-ary tree (T, τ) that satisfies the following
3. (a) for some w ∈ T at distance i from the root (|w| = i), we have that τ(w) = ¯ ta;
4. (b) for each w ∈ T, there is a (t′a , ϱ(|w|)) ∈ Sj with τ (w) = ¯ t′a ;

where ϱ(i) = min(i, n0), ♯E(K) denotes the number of concepts and assertions of the form EC and E©iα in K, and nr,i a and ˆnr,i a are defined as follows: Let Ari be the set defined as:

• {r(a, b) | P©j r(a, b) ∈ A}, if r ∈ Rolrig(K),

Then, nr,i a is max({0} ∪ {m ∈ ♯rT | r(a, b1) . . . r(a, bm) ∈ Ari , for distinct b1, . . . , bm}) and ˆnr,i a is nr,i a +1 if nr,i a +1 ∈ ♯rT , and nr,i a , otherwise.

Intuitively, Condition 1 takes care of the 'DL-dimension' in the sense that it ensures that each time point will have associated an appropriate DL-interpretation. Condition 2 generally takes care of the temporal evolution of a single domain element a, captured by the tree (T, τ), and of verifying Boolean consistency of types; indeed, that is why types are not required to 'respect' Booleans. More interestingly, Condition 2(c) takes care of the temporal dimension by checking that (i) the fresh concept names faithfully represent the surrogated concepts and role assertions they are substituting (ϕ1), (ii) no inconsistencies are introduced by role assertions (ϕ2), (iii) rsuccessors induced by the ABox are properly witnessed (ϕ3 and ϕ4), and (iv) the semantics of rigid roles is respected, that is, if a fresh concept name standing for a number restriction involving rigid roles is satisfied at some world, then it must be satisfied at all worlds (ϕ5). The numbers nr,i a and ˆnr,i a , used in (iii), intuitively, take into account the number of r-successors of a induced by A at worlds at distance i from the root.

The algorithm terminates when Sj = Sj+1 (no further temporal types are eliminated) and returns "satisfiable" if for every a ∈ ind(A), there is a type (ta, 0) ∈ Sj such that (i) if P©iC(a) ∈ A (C of the form A or ¬A), then P©iC ∈ ta and (ii) if a occurs in a role assertion α ∈ A, then α ∈ ta; and "unsatisfiable" otherwise.

Bound n0. It now remains to determine the value of n0 for which the algorithm is correct. Intuitively, we are looking for an n0 ensuring that all necessary information to build an (infinite) model is captured in the final result S of the algorithm. In other words, it must be ensured that all the temporal types of the infinite expansion

are realisable in the sense that they satisfy Conditions 1 and 2 of Definition 1 when ϱ(i) is replaced with i.

We start by observing that while for CTL-Lite Nbool types capture the required information about models, making the number of types an appropriate n0 bound, they fail to do so for CTL∗-Lite Nbool . Intuitively, this is because CTL∗-Lite Nbool allows to nest an arbitrary number of temporal operators, as for example in E©©©C, but this is not reflected in the definition of (state) subconcepts and therefore in that of types. To solve this problem, we follow an approach suggested by Guti´errez-Basulto et al. [2012] in which the aforementioned connection between NBTAs and CTL and CTL∗ is used to show that the states Q of the NBTA Aϕ, accepting precisely the 2cn -labelled ♯E(K)-ary trees satisfying ϕ in Condition 2(c), ensure that all elements of the infinite expansion of S are realisable; indeed, states do 'memorise' consecutive temporal operators. We thus obtain the following bound n0 := |Q|·|tp(K)|·|atp(K)|, where |Q| ∈ 22poly(|ϕ|) if ϕ is a CTL∗ formula, and |Q| ∈ 2poly(|ϕ|) if ϕ is a CTL formula [Kupferman and Vardi, 2005; Vardi, 2006]. See the appendix for more details on the bound. Having n0 at hand:

Theorem 1. The algorithm returns "satisfiable" iff there is a model of K.

For proving "⇒", we inductively construct a twodimensional model of K using the infinite trees (T, τ) witnessing that all temporal types in Sω satisfy the modified Condition 2. We roughly proceed as follows. We start with fixing the temporal evolutions of all ABox individuals by choosing, for every a ∈ ind(A), some (ta, 0) ∈ Sω, and the corresponding infinite tree witnessing Condition 2. For the inductive step, assume that an element d has in its type t at time point w with |w| = i a number restriction 'demand' ≥ n r. In such a case, we add n elements d1, . . . , dn to the domain (if there already some r-successors, we add less). Then, we choose some type (t′ , i) from Sω witnessing Condition 1 of Definition 1 for (t, i), and complete the temporal evolution of each dj according to infinite tree (T, τ) witnessing (the modified) Condition 2 for (t′ , i).

Overall Complexity. We finally argue that the algorithm runs in double and single exponential time for CTL∗-Lite Nbool and CTL-Lite Nbool , respectively. Clearly, the bound n0 is in 22poly(|K|) for CTL∗-Lite Nbool and in 2poly(|K|) for CTL-Lite Nbool , and the number of steps of the algorithm is in n0 · 2poly(|K|) . The number of states of Aϕ, used to check Condition 2(c), is n0, and NBTAs to check Conditions 2(a) and 2(b) can be constructed using at most n0 states. Thus, the desired result is obtained from the above arguments and the two following facts: (i) a constant number of NBTAs can be intersected with only a polynomial blowup, and (ii) non-emptiness of NBTAs can be checked in quadratic time in the number of states [Vardi, 1998].

Theorem 2. KB satisfiability is EXPTIME-complete for CTL-LiteNbool and 2EXPTIME-complete for CTL∗-LiteNbool .

Note that CTL-Lite Nbool is rather robust in the sense that by just lightening its components better complexity is not immediately obtained. Indeed, the following can be shown using ideas of the EXPTIME-hardness proof for subsumption in the DL ELI [Baader et al., 2008].

Theorem 3. KB satisfiability is EXPTIME-hard for CTL-

Litehorn with only the temporal operators E© and A©.

4 CTL- &CTL∗-Lite Nbool Formulas

In this section, we study extensions of CTL-Lite Nbool and CTL∗-Lite Nbool in which temporal operators are not only applied to concepts, but also to Boolean combinations of concept inclusions and ABox assertions. CTL∗-LiteNbool -state formulas ϕ, ϑ and CTL∗-LiteNbool -path formulas ψ, χ are defined by the following grammar:

where C,D are CTL∗-Lite Nbool -concepts, {a, b} ⊆ NI and r ∈ NR. Given an interpretation I, a world w in I and a path π, the truth relations I, w |= ϕ and I, π |= ψ are defined as expected (cf. appendix); for instance, I,w |= C ⊑ D iff C I,w ⊆ DI,w . We say CTL∗-LiteNbool -formula to refer to a CTL∗-Lite Nbool -state formula (CTL-Lite Nbool -formulas are defined analogously), and say that I is a model of a CTL∗-Lite Nbool -formula ϕ, written I |= ϕ, iff I, ε |= ϕ.

4.1 Satisfiability of Temporal Formulas

We next devise an algorithm for the satisfiability problem of CTL∗-Lite Nbool and CTL-Lite Nbool formulas combining again type-based abstractions with automata-based approaches to temporal reasoning. We obtain 3EXPTIME and 2EXPTIME upper bounds for CTL∗-Lite Nbool - and CTL-Lite Nbool formulas, respectively. In contrast to the TDLs in Section 3, for temporal formulas the independence of elements at each Iw is lost, and therefore one cannot 'separately' reason about the temporal evolution of each domain element. Indeed, the introduction of temporal TBox formulas, e.g. A♦□(A ⊑ E♦∃r), forces to see each Iw as one inseparable entity. As a consequence, in our decision procedure, tree automata run over trees labelled with sets of types (rather than a single type), representing interpretations.

Let ϕ be a CTL∗-Lite Nbool or a CTL-Lite Nbool -formula whose satisfiability is to be decided, and ind(ϕ), Rol(ϕ), CN(ϕ), Rolrig/loc(ϕ), ♯rϕ denote the expected sets, see Section 2. We use cl(ϕ) and sub(ϕ) to respectively denote the set of all (i) state concepts occurring in ϕ together with {∃r | r ∈ Rol(ϕ)}, closed under subconcepts and single negation, and (ii) state subformulas of ϕ, closed under single negation. We assume wlog. that if r(a, b) ∈ sub(ϕ), then r-(b, a) ∈ sub(ϕ). A concept type for ϕ is a set t ⊆ cl(ϕ) such that ≥ n r ∈ t implies ≥ m r ∈ t, for all ≥ n r ∈ cl(ϕ) and m ∈ ♯rϕ with m < n; and tp(ϕ) denotes the set of all concept types for ϕ. A pointed type for ϕ is a pair (t, a) with t ∈ tp(ϕ) and a ∈ ind(ϕ), and ptp(ϕ) denotes the set of all pointed types for ϕ - ta is used as in the previous section.

Definition 2. A quasistate for ϕ is a tuple (S1, S2, S3) with S1 ⊆ tp(ϕ), S2 ⊆ ptp(ϕ) and S3 ⊆ sub(ϕ) is a formula type for ϕ such that

1. For each t ∈ S1, if ≥ n r ∈ t, then there is a t′ ∈ S1 with ∃r- ∈ t′ ;
2. For each a ∈ ind(ϕ), S2 contains exactly one pointed type ta;
3. If (t, a) ∈ S2, then t ∈ S1;
4. For all C(a) ∈ sub(ϕ) and ta ∈ S2, C(a) ∈ S3 iff C ∈ ta;
5. For all a ∈ ind(ϕ), r ∈ Rol(ϕ), ≥ nra r ∈ ta;
6. For all t ∈ S1, C ⊑ D ∈ S3 iff C ∈ t implies D ∈ t, for all C ⊑ D ∈ sub(ϕ),

where nra = max({0} ∪ {m ∈ ♯rϕ | r(a, b1), . . . , r(a, bm) ∈ S3 for distinct b1, . . . bm}). A quasimodel Q for ϕ is a qs(ϕ)- labelled tree (of any outdegree) with qs(ϕ) denoting the set of all quasistates for ϕ.

Similar to Section 3, we again surrogate the 'DL component' to use the automata machinery for temporal reasoning. For t ∈ tp(ϕ), ¯ t is the result of replacing each C ∈ t \ CN(ϕ) with a fresh concept name XC, and ccn denotes the set of all resulting names, including CN(ϕ). For all C ∈ cl(ϕ), ¯ C denotes the result of replacing in C every subconcept ≥ n r with Xn r ; and ⊓ with ∧. We also surrogate the 'DL-component' at the formula level: For every ϑ ∈ sub(ϕ), ¯ ϑ denotes the result of replacing every subformula α of ϑ of the form C ⊑ D, C(a), r(a, b) or ¬r(a, b) with a fresh concept name Yα, and fcn denotes the set of all concept names introduced in this way. We will 'independently' reason about the temporal evolution of concepts and formulas. For S ⊆ sub(ϕ), ¯ S refers to {¯ ϑ | ϑ ∈ S}. For a quasimodel Q, we then use Q3 to denote the 2fcn -labelled tree obtained by associating each w ∈ Q with the label ¯ S3(w).

We next give conditions on quasimodels for ϕ ensuring they appropriately describe models of ϕ.

Definition 3. A quasimodel Q = (T, τ) for ϕ is proper if:

1. For all w ∈ T, τ(w) = (S1, S2, S3) and all t ∈ S1, there is a 2ccn -labelled tree (T, τ ′ ) such that
2. (a) τ ′ (w) = ¯ t;
3. (b) For all w′ ∈ T with τ(w′ ) = (S′1 , S′2 , S′3 ), there is a t′ ∈ S′1 such that τ ′ (w′ ) = ¯ t′ ;
4. (c) ε satisfies ϑ =A□(ϑ1 ∧ ϑ2) where

1. For all a ∈ ind(ϕ), τ(ε) = (S1, S2, S3) with (t, a) ∈ S2, there is a 2cnn -labelled tree (T, τ ′ ) with Condition (c) as in Point 2 above and

Intuitively, Condition 1 takes care of Q satisfying the temporal formula ϕ; in particular, it ensures consistency of role assertions and that if a role assertion involving a rigid role is satisfied at some point, then it is satisfied at all time points. Conditions 2 and 3 ensure that each (pointed) type has an appropriate temporal evolution through the quasimodel; the meaning of Conditions 2(c) and 3(c) is similar to that of the analogous Conditions in Section 3, cf. Definition 1.

We first show that satisfiability of temporal formulas is characterised by the existence of a proper quasimodel:

Lemma 1. ϕ is satisfiable iff there is a proper quasimodel for ϕ.

As the next step, we will construct a tree automaton A that accepts precisely the proper quasimodels for ϕ. To achieve this, most importantly, A will simulate the runs of the NBTAs Aϑ associated with Condition 2(c) in Definition 3. The use of A is sanctioned by the fact that the outdegree of proper quasimodels can be bounded, see [Guti´errez-Basulto, 2013, Lemma 3.22]. Let Aϑ = (Q1,Σ,Q01 , δ1, F1) be the NBTA accepting precisely the 2ccn -labelled ♯E-ary trees satisfying ϑ, where ♯E is the number of state concepts of the form EC in ϕ. We have the following:

Lemma 2. There is a proper quasimodel for ϕ iff there is a proper quasimodel of arity k = |qs(ϕ)|·|tp(ϕ)|·|ind(ϕ)|·Q1.

The tree automaton A we construct in the appendix is a two-way alternating tree automaton (2ATA) [Vardi, 1998]. Intuitively, a 2ATA is needed because of two reasons: (i) A must be two-way, and therefore allow a predecessor state, because while simulating Aϑ in A the simulation needs to start at an arbitrary world w, however, the original run of Aϑ starts at the root world ε. Note that this would not be necessary if we assume expanding domains, instead of a constant one. (ii) A must be alternating, and therefore being able to send several state successors along a branch, because A needs to simulate a run of Aϑ for each type in a given world. Finally, note that the simulated Aϑ needs to be a NBTA (rather than an ATA) because we must ensure that one state is assigned to each successor - cf. Conditions 2(b) and 3(b) in Definition 3. Since the definition of A is essentially the same as the one previously introduced by Guti´errez-Basulto et al. [2012] for temporal formulas based on ALC and CTL and CTL∗, we differ it to the appendix.

Overall Complexity. (i) Non-emptiness of 2ATAs can be checked in EXPTIME in the number of states [Vardi, 1998]. (ii) The number of states of Aϑ, the most dominating in the definition of the states in A, is in 22poly(|ϕ|) if ϑ is a CTL∗ formula and in 2poly(|ϕ|) if ϑ is a CTL formula. We thus obtain:

Theorem 4. Satisfiability is in 3EXPTIME for CTL∗-LiteNbool - and in 2EXPTIME for CTL-LiteNbool -formulas.

4.2 CTL-Litehorn Formulas

Finally, we look at CTL-Litehorn-formulas, the sub-fragment of CTL-Lite Nbool in which C,D are CTL-Litehorn-concepts, and show that this fragment is already 2EXPTIME-hard. In particular, we show the following:

Theorem 5. Satisfiability of CTL-Litehorn-formulas with only local roles and, A© and E© is 2EXPTIME-hard.

The proof of Theorem 5 is by reduction of the word problem of an exponentially space bounded alternating Turing machine. We next outline the main ideas of the reduction. (i) The computation tree of an ATM is represented by the temporal evolution of a single individual name a, such that each time point corresponds to a tape cell and a configuration is then represented by exponentially consecutive time points. (ii) To synchronise i-cells in consecutive configurations, the 'content of a' at position i is stored in a fresh local ra-successor and then recovered back to a using temporal TBoxes of the form⊤ ⊑ A∨⊤ ⊑ ¯ A, with A and ¯ A disjoint, ensuring that all domain elements in a given time point share the truth value of A. (iii) Information is transported between neighbouring configurations using binary counters.

From Theorems 4 and 5, the following is obtained:

Theorem6. Satisfiability of CTL-Litehorn- and CTL-LiteNbool formulas is 2EXPTIME-complete.

5 Conclusions and FutureWork

This paper has advanced the understanding of TDLs based on DL-LiteNbool and, CTL∗ and CTL. In particular, we developed uniform algorithms for both CTL∗ and CTL-based extensions, providing (mostly tight) elementary upper bounds.

As immediate future work, we will look for tractable fragments. To this aim, we plan to follow in the footsteps of Artale et al. [2013; 2014] and analyse clausal fragments of CTL and CTL∗. For example, tractable fragments allowing E♦ (arbitrarily used in both sides of concept inclusions) might be identified since, in contrast to ♦, it does not lead to nonconvexity [Guti´errez-Basulto et al., 2014].

We will also study branching temporal extensions of DLLite in the OBDA scenario. We are particularly interested in studying the query answering problem over branching temporal DL-Lite ontologies. Indeed, it has been argued that in some settings allowing for different versions of data over time might be desirable [Rondogiannis et al., 1998; Chomicki and Toman, 2005].

Beyond TDLs, we will investigate whether our approaches can be extended so as to derive elementary upper bounds for decidable fragments of first-order branching temporal logic.

Acknowledgments

We thank anonymous reviewers for many useful comments and suggestions for improving the paper.