Fixpoints in Temporal Description Logics

1 Introduction

Monodic temporal extensions of various (decidable) fragments of first-order logic have been studied employing the quasi-model approach of Wolter and Zakharyashev [Hodkinson et al., 2000; 2001]. Their technique has been successfully applied to a variety of decidable fragments, e.g., to the ALC and DLR description logics, to the guarded fragment GF, or to the two variables fragment. In addition, the complexity of the decision procedures for these fragments has been studied [Hodkinson et al., 2003]. All these papers have focused on the standard first-order temporal logic that uses the U (until) and S (since) connectives [Artale and Franconi, 2005; Lutz et al., 2008], save [Gabbay et al., 2003] that studies an extension of a multi-modal (but still first-order) logic.

However, first-order temporal logics have been shown to lack certain expressiveness related, e.g., to expressing periodic events. This shortcoming has been identified by Wolper [Wolper, 1983] and various extensions have been proposed, e.g., the extended temporal logic (ETL) [Wolper, 1983] and the temporal fixpoint calculus [Vardi, 1988].

Simple temporal fixed point extensions of description logics have been considered in [Franconi and Toman, 2003] that enhances the temporal part of the language instead of varying the first-order fragment. That paper shows that the original quasimodel technique is amenable to using a much more expressive language over the temporal structure, while retaining decidability for many of the fragments studied in the US case. However, the temporal description logic proposed in that paper disallows all of the interactions between the temporal fix-

David Toman

D.R.Chariton School of Computer Science University of Waterloo, Canada

david@cs.uwaterloo.ca

points and the role constructors in the underlying description logic.

This paper addresses that shortcoming by allowing fixpoint operators to interact with role constructors of the underlying description logic: this way resolves one of the open problems proposed by [Franconi and Toman, 2003].

In order to focus on the actual temporal dimension of the problem, the results of our paper are formulated with respect to a basic description logic ALC. However, the results can be extended to other dialects of description logics and likely to many other decidable fragments of first-order logic, provided they satisfy the monodicity restriction of [Hodkinson et al., 2000]. The results are as follows:

• We introduce a decision procedure for ALCμTL, a temporal description logic with future time temporal operators that is strictly more expressive than ALCU. The extension is based on the temporal fixpoint calculus [Streett and Emerson, 1984; Vardi, 1988];
• We provide tight complexity bounds on the decision procedure that mirror those for ALCU . Thus, from the complexity standpoint, the extension is for free;
• We show that a similar technique works also for ALCμTL extended with past connectives that properly extends the logic ALCUS; and
• We briefly discuss how the proposed extension can be applicable to other more expressive dialects of description logics, e.g., ALCO, ALCQ, and others.

The paper is organised as follows: Sections 2 and 3 provide the necessary definitions and discuss the properties of the proposed logic. Section 4 presents decidability of the temporal fixpoint extension of a simple description logic ALC. It also presents complexity bounds for the associated reasoning problems. However, due to a heavy reliance on a rather complex quasimodel machinery [Hodkinson et al., 2000], we will only give a outline of the main steps needed to prove the main claim of the paper. Section 6 discusses the applicability of the results to a wider range of description logics and other decidable fragments of first-order logic. Section 7 concludes with directions for future research.

2 Definitions

We start with defining ALCμTL, the temporal fixpoint extension of the standard description logic ALC:

Definition 1 (ALCμTL syntax) Concepts in the language ALCμTL are defined by the following abstract syntax:

where Circle is the usual next-time temporal operator. For the fixpoint concept μA.C-where A is an atomic concept-we require that free occurrences of A in the concept expression C are all positive, i.e., they appear within even numbers of negations and in addition in the scope of at least one next time (Circle) operator.

Formulas of ALCμTL are defined by the abstract syntax

Similar to concepts descriptions, the propositional variable x in μx.ϕ can only appear in ϕ under an even number of negations and must be in the scope of at least one Circle operator.

Informally, the concept μA.C denotes the least fixpoint solution to the equation A = C(A), where C is seen as a set to set function of the concept variable A. Similarly, μx.ψ denotes the least solution to the x ≡ ψ equation.

The restriction on formation of the fixpoint constructs ensures that the fixpoint is well defined and truly temporal; indeed we will see that this restriction makes the description logic part of ALCμTL essentially a fragment of firstorder logic. The greatest fixpoint operator can be defined, as expected, as νA.C = ¬μA.¬C[¬A/A] for concepts and νx.ϕ = ¬μx.¬ϕ[¬x/x] for formulas of ALCμTL.

Definition 2 (ALCμTL semantics) An ALCμTL interpretation structure is a triple I = (T ,Δ, (·)I(t) ) where T is a flow of time based on natural numbers, Δ is a non-empty domain of objects, and (·)I(t) is an interpretation function that for every t ∈ T provides an interpretation for concepts and roles at time t, i.e., C I(t) ⊆ Δ and RI(t) ⊆ Δ × Δ. The interpretation must satisfy the following conditions:

where C k [⊥/A] stands for the concept description obtained by unfolding a fixpoint concept k times 1 . Note that we make the constant domain assumption, i.e., Δ does not change over time.

Given a formula ϕ, an interpretation I, and a time point t ∈ T , the truth-relation I, t |= ϕ (ϕ holds in I at time instant t) is defined inductively as follows:

where false is a shorthand for p ∧ ¬p. A formula ϕ is satisfiable if there is a temporal interpretation I such that I, 0 |= ϕ; I is then called a model for ϕ.

A concept C is satisfiable if there is an interpretation I such that CI(t) ̸= ∅ for t = 0. We say that ϕ is globally satisfiable if there is an interpretation I such that I, t |= ϕ for every t (I |= ϕ, in symbols). We say that ϕ (globally) implies ψ and write ϕ |= ψ if we have I |= ψ whenever I |= ϕ.

Note that a concept C is satisfiable iff ¬(C ⊑ ⊥) is satisfiable, a formula ϕ is globally satisfiable iff ✷ϕ is satisfiable, and ϕ |= ψ iff ✷ϕ∧¬ψ is not satisfiable 2 . Thus, all reasoning tasks connected with the notions introduced above reduce to satisfiability of formulas.

In the rest of the paper we also assume that all concepts and formulas are in negation normal form (NNF), i.e., negations are only applied to primitive concepts and primitive formulas. It is easy to see that every concept (formula) in ALCμTL has an equivalent concept (formula) in NNF.

3 Properties of ALCμTL

The language we have introduced so far has clear advantages over the description logic ALCU, for example, the addition of fixpoints allows us to express the notion of evenness and periodicity, properties not expressible in ALCU . On the other hand, the U (until) operator and the other standard temporal connectives of ALCU can be encoded in the logic with fixpoints ALCμTL as follows:

Moreover, based on results on the expressive power of propositional linear time temporal logics [Wolper, 1983] we can prove the following:

1 Due to the restrictions on the occurrence of A in C, this definition is equivalent to the more common intersection of models definition [Calvanese et al., 1999; Vardi, 1988].

2 The ✷ operator (read always in the future) will be defined in Section 3.

Proposition 3 ALCμTL is more expressive than ALCU .

A typical example of the additional expressive power of ALCμTL would be a property which should hold true every k time points, starting from the current one. For example, a catholic priest celebrates the Mass every seven days:

Celebrating-Catholic-Priest .= ν A.(∃celebrate.Catholic-Mass ⊓ CircleCircleCircleCircleCircleCircleCircleA)

Observe that, in the fragment introduced in the previous section, the descriptions within a single state are purely firstorder; the fixpoint operator only affects the temporal part of the language and it does not change the first order nature of the description logic.

Note also that in this fragment it is impossible to express temporalised roles (temporal operators cannot be applied on roles). It is well known that allowing these would lead to an undecidable satisfiability problem even in ALCU [Hodkinson et al., 2000].

4 Decidability and Complexity of Reasoning

Now we study the computational properties of ALCμTL. We consider only the natural numbers-like flows of time T = (N, <).

We first introduce the necessary background definitions related to the quasimodel-based technique used to show decidability of various monodic temporal extensions of decidable fragments of first-order logic [Hodkinson et al., 2000; Wolter and Zakharyaschev, 1999]. We modify these to suit ALCμTL over the flow of time (N,<).

Consider a formula ϕ ∈ ALCμTL. We define sets of formulas and concepts, subϕ and conϕ to be the closures under negations of all subformulas and subconcepts of ϕ, ψ[μx.ψ/x], and D[μA.D/A] for each fixpoint subformula μx.ψ and fixpoint concept μA.D in ϕ; a natural extension of the idea of the Fischer-Ladner closure of ϕ with respect to its subformulas and subconcepts [Fisher, 1979]. We also assume that all concepts (formulas) the form CircleC (Circleψ) have been replaced by unique auxiliary primitive concepts ACircleC (propositions pCircleψ), respectively, that do not appear in ϕ.

Definition 4 (Quasiworlds for ϕ) Given an ALC interpretation I (that interprets primitive symbols in ϕ and the above auxiliary symbols), we define a quasiworld wI for ϕ to be the tuple

Were constants (ABox or nominals) allowed, the quasiworlds would need an additional component accounting for the behaviour of these constants. The important observations at this point are that, for a fixed formula ϕ, (1) there are only finitely many (distinct) quasiworlds, and (2) for decidable description logics, they can be effectively constructed.

The interpretations I for the individual quasiworlds will eventually serve as templates for models of single states in an overall model for ϕ. In turn sequences of quasiworlds will serve as abstractions of models of ϕ.

However, these abstractions must be coherent along the temporal dimension. This, in particular, requires that the auxiliary concepts and formulas standing for temporal subconcepts and subformulas behave according to the underlying temporal semantics, in particular

1. for least fixpoints there must not be infinite regenerating sequences, and
2. the auxiliary concepts and formulasmust behave according to the definitions of temporal connectives.

First we need to guarantee that the abstraction prevents infinite sequences of unfolding of a least fixpoint that appears in ϕ as a subconcept or a subformula. To achieve this goal we need to detect such sequences in a potential quasimodel by considering repetitive unfolding of fixpoints along time, called regeneration. For this we need an auxiliary definition of derivation that tells us how later instances of fixpoint subformulas have been derived from earlier ones. We employ an extension of choice function introduced by Street and Emerson [Streett and Emerson, 1984] for μTL:

Definition 5 (Choice Relations and Adornment) Let W = 〈wi : i ∈ N〉 be a sequence of quasiworlds of the form 〈Ti,Ψi〉, indexed by natural numbers. We say that a relation

is a concept adornment of W if, for each time instant i ∈ N, each type t ∈ Ti and every concept D ∈ t of the form C1⊔C2, ∃R.C, or ACircleC, it satisfies

where E is either C1 or C2, t′ ∈ Ti such that C ∈ t′ and whenever ∀R.E ∈ t then E ∈ t′ , and t′′ ∈ Ti+1 such that C ∈ t′′ . Moreover, for each triple i, t, and D there is at least one tuple in the relation ADRNC. We say that a relation

is a formula adornment of W if, for each time instant i and every formula ψ ∈ Ψi of the form ψ1 ∨ ψ2 it satisfies

where δ is either ψ1 or ψ2 and such that for each tuple i and ψ there is at least one tuple in the relation ADRNF.

Intuitively, the adornment relation ADRNC tells us how disjunctions and existential restrictions are to be satisfied in the abstraction: we use relations to represent the adornments to capture the fact that, e.g., the concept ∃R.D can be realized in several ways in a particular model and thus in its abstraction 3 . Similarly, ADRNF handles disjunctions in ALCμTL formulas.

3 [Streett and Emerson, 1984] use a partial function instead.

It is easy to see that, whenever a sequence of quasiworlds faithfully represents an actual model of an ALCμTL formula, the adornment relations, as defined above, exist and represent at least a partial functions, i.e., each disjunction and existential restriction (in each type of every quasiworld) must have a realization-represented as a tuple in these relations. Conversely, given a sequence of quasiworlds with an adornment, we can construct a model for each wi ∈ W that corresponds to the adornment (by appropriately realizing disjunctions and existential restrictions.

Hence, given a sequence W = 〈wi : i ∈ N〉 of quasiworlds of the form 〈Ti,Ψi〉 and with the help of the adornments ADRNC and ADRNF we can define a derivation of concepts, denoted by ⊢, for concepts in the type t ∈ Ti, as follows:

1. if C1 ⊔ C2 ∈ t then (i, t,C1 ⊔ C2) ⊢ (i, t,E) when ADRNC(i, t, C1 ⊔ C2, t, E));
2. if ∃R.C ∈ t then (i, t, ∃R.C) ⊢ (i, t′ ,C) when ADRNC(i, t, ∃R.C, t′ , C);
3. if ∀R.C ∈ t then (i, t, ∀R.C) ⊢ (i, t′ ,C) whenever ∃R.E ∈ t and ADRNC(i, t, ∃R.E, t′ , E);
4. if C1 ⊓ C2 ∈ t then (i, t,C1 ⊓ C2) ⊢ (i, t,C1) and (i, t, C1 ⊓ C2) ⊢ (i, t, C2);
5. if ACircleC ∈ t then (i, t,CircleC) ⊢ (i + 1, t′ , C) whenever ADRNC(i, t, ACircleC, t′ , C);
6. if μA.C ∈ t then (i, t, μA.C) ⊢ (i, t,C[μA.C/A]); and
7. if νA.C ∈ t then (i, t, νA.C) ⊢ (i, t,C[νA.C/A]).

Note that the choice of t′ in (5) corresponds to the fact that runs potentially connect all compatible pairs of types and thus we must consider derivations through any of the compatible types t′ in the next quasiworld. Similarly, we define a derivations of formulae in Ψi as follows:

1. if ψ1 ∨ ψ2 ∈ Ψi then (i, ψ1 ∨ ψ2) ⊢ (i, ψ) when ADRNF(i, ψ1 ∨ ψ2, ψ);
2. if ψ1 ∧ψ2 ∈ Ψi then (i, ψ1 ∧ψ2) ⊢ (i, ψ1) and (i, ψ1 ∧ ψ2) ⊢ (i, ψ1);
3. if PCircleψ ∈ Ψi then (i,Circleψ) ⊢ (i +1, ψ);
4. if μx.ψ ∈ Ψi then (i, μx.ψ) ⊢ (i, ψ[μx.ψ/x]); and
5. if νx.ψ ∈ Ψi then (i, νx.ψ) ⊢ (i, ψ[νx.ψ/x]).

Similar to types in quasiworlds, the adornment relations can be represented by unary predicates over W indexed by the remaining parameters (as those are fixed for a given ALCμTL formula ϕ). Derivation relations can then be captured, e.g., as a S1S formula over these relations.

Definition 6 (Regenerating Sequence) Let i0, ik ∈ N. We say that

• the concept μA.C is regenerated from i0 to ik if there is a sequence i1, . . . , ik-1 ∈ N such that (ij, tij ,Cij ) ⊢ (ij+1, tij+1 ,Cij+1 ) such that Ci0 = Cik = μA.C and each Cij contains μA.C as subconcept; and
• the formula μx.ψ is regenerated from i0 to ik if there is a sequence i1, . . . , ik-1 ∈ N such that (ij, ψij ) ⊢ (ij+1, ψij+1 ) such that ψi0 = ψik = μx.ψ and each ψij contains μx.ψ as subformula.

To make auxiliary concepts and formulas respect the semantics of temporal connectives, we define the notion of run:

Definition 7 (Runs) Let W = 〈wi : i ∈ N〉 be a sequence of quasiworlds of the form 〈Ti,Ψi〉, indexed by natural numbers. We say that a sequence r = 〈ti : i ∈ N〉, where ti ⊆ conϕ, is a run if

Runs relate domain elements from the domains of different quasiworlds yielding a coherent model for ϕ (here, the ability to copy domain elements in the individual states sufficiently many times is essential to have sufficiently many runs). We use runs not involved in infinite regenerating sequences to restrict sequences of quasiworlds to those that properly abstract models of an ALCμTL formula ϕ as follows:

Definition 8 (Quasimodel) Let W = 〈wi : i ∈ N〉 be a sequence of quasiworlds of the form 〈Ti, Ψi〉, indexed by natural numbers. We say that W is a quasimodel for ϕ if

1. ϕ ∈ Ψ0;
2. for every t ∈ Ti and i ∈ N there is a run r such that t = r(i);
3. pCircleψ ∈ Ψi iff ψ ∈ Ψi+1;
4. μx.ψ ∈ Ψi iff ψ[μx.ψ/x] ∈ Ψi;
5. νx.ψ ∈ Ψi iff ψ[νx.ψ/x] ∈ Ψi; and
6. W is well-founded, i.e., there is no infinite sequence i0, i1, . . . such that μA.C ∈ conϕ (μx.ψ ∈ subϕ) regenerates from ij to ij+1 for all j ≥ 0.

Theorem 9 An ALCμTL formula ϕ is satisfiable if and only if there is a quasimodel for ϕ.

Proof (sketch) Given a model of ϕ we show that a quasimodel W for ϕ exists (this is analogous to the proof in

[Wolter and Zakharyaschev, 1999]); in addition we need to show that we can construct an adornment ADRNC and ADRNF for W (follows from the fact that every quasiworld in W can be realised); for the other direction having a quasimodel W and an adornment ADRNC and ADRNF we can construct a realisation Ij of each quasiworld in wj ∈ W that corresponds to the adornment; and then using these realisations Ij from and runs we can construct a model for ϕ; this is again analogous to the proof in [Wolter and Zakharyaschev, 1999], save the use of adornments to guarantee well-foundedness of least fixpoints.

Thus, it suffices to check whether ϕ has a quasimodel. This can be done, e.g., by embedding the quasimodel conditions into S1S, similarly to [Hodkinson et al., 2000]. In particular, S1S is more than sufficient to enforce the temporal fixpoint conditions. To achieve tight complexity bounds, we can employ the fact that, for satisfiable ALCμCircle formulas, periodic quasimodels exist. We construct an automaton that accepts exactly the quasimodels for ϕ: this automaton is a product of an automaton that verifies the conditions on runs and a complement of another automaton that detects infinite regenerating sequences for fixpoints; the technique is an adaptation of a technique in [Vardi, 1988].

Theorem 10 The formula satisfiability problem for ALCμTL is EXPSPACE-complete.

The upper bound relies on the construction in [Vardi, 1988] by observing that the input to the construction is exponential in |ϕ|, hardness holds even for ALC✷.

5 ALCμTL with previous-time operator

We now consider extending ALCμTL with past operators, in particular the previous time (CIRCLE) operator. The natural extension of the semantics of ALCμTL are as follows:

and

for an integer-like flow of time (for natural numbers-like flows we need two past operators to account for differences for t = 0). To keep the description logic part first-order we require that each fixpoint variable (i.e., primitive concept name or propositional variable) must occur in the scope of at least one of the previous (CIRCLE) and next time (Circle) operators and, if it occurs in the scope of multiple operators, the number of Circle and CIRCLE must be different (this ensures that fixpoint formulas can regenerate only at different time instants). Note that this logic properly contains ALCUS .

With these definitions we can reuse all of the machinery introduced in Section 3 to obtain a tight EXPSPACE complexity bound for ALCμTL with both past (CIRCLE) and future (Circle) temporal operators. The main technical difference is that for checking for well foundedness of a quasimodel a two-way automaton is needed [Vardi, 1988].

6 Temporal Fixpoints and Other Fragments

The decidability result can be extended to more powerful description logics and other decidable fragments of first-order logic, in particular to the following:

Theorem 11 Satisfiability of the monodic fixpoint temporal extensions of

• ALCO and
• ALCQ

is EXPSPACE-complete.

These results are based on patching the decidability proofs in, e.g., [Wolter and Zakharyaschev, 1999; Hodkinson, 2002; Artale et al., 2002] using our technique. In the first case we add constants in the same fashion as in [Wolter and Zakharyaschev, 1999]: the quasiworlds will now have an additional component of types realized by said constants. In the second case we simply modify the derivation relation (for ∃R.C) in the notion of regeneration (Definition 6) to account for the number restrictions. This modification is confined to single quasiworlds and does not affect the remaining machinery.

Consequently, the extension of ALCμTL with an ABOXallowing assertions of the form a : C and aRb, for a and b names of individual objects in Δ, to be considered atomic formulas alongside C ⊑ D-does not change the computational properties of ALCμTL:

Theorem 12 The formula satisfiability problem for ALCμTL with an ABox is EXPSPACE-complete.

This follows immediately from the result for ALCO.

Our results also show that the temporal fixpoint extension is mostly orthogonal to the consideration of the underlying first-order fragment (as long as integer-like flow of time is used).

7 Conclusion

The paper solves an open problem in [Franconi and Toman, 2003] and shows that a much more involved introduction of temporal fixpoints in description logics still preserves decidability and complexity bounds. The extension enhances the expressive power of the languages: for example, evenness is now definable over the temporal dimension. The technical contribution of the paper lies in a non-trivial extension of the quasiworld technique to logics in which temporal operators (in our case defined by fixpoints) interact with the role constructors of the underlying description logic and thus cannot be captured by considering properties of individual runs in a quasimodel alone (in contrast to the standard first-order connectives U and S or the fixpoint extension proposed in [Franconi and Toman, 2003]). The paper also paves a path to fixpoint extensions of other decidable fragments of first-order logics that have been shown decidable using the quasimodel technique in the first-order temporal logic setting.

7.1 Open Problems

We are currently studying several extensions of the framework proposed in this paper, namely:

• Allowing full ALCμTL; in this case, the concept descriptions are no longer first-order in every temporal world and the quasi-model technique cannot be applied directly;
• Allowing inverses in the underlying description logic: this complicates the construction of adornments (we conjecture such an extension still preserves the EXPSPACE complexity bound but the development is beyond the scope of this paper), and
• Allowing other decidable formalisms, such as the guarded fragment GF in a monodic combination with temporal fixpoints.

Other extensions relate to studying temporal fixpoints for other flows of time, to allowing even more expressive temporal languages (e.g., S1S), and to investigating interaction with queries [Artale et al., 2002].

Orthogonally, we can consider various restrictions on the occurrence of temporal operators, e.g., only in concepts, with an optional global set of DL axioms, or only in DL axioms leaving concepts and roles non-temporal, along the lines in [Lutz et al., 2008]. Yet another direction is to consider temporal fixpoints in connection with lightweight description logics such as DL-Lite and EL and the problem of query answering over knowledge bases based on fixpoint temporal description logics.