A Description Logic of Change

1 Introduction

An important application of Temporal Description Logics (TDLs) is the representation of and reasoning about temporal conceptual models [Artale, 2004; Artale et al., 2003; 2002]. Knowledge captured by such models is translated into a TDL TBox and reasoning algorithms for TDL are then used to detect inconsistencies and implicit IS-A relations in the temporal model [Artale and Franconi, 1999; Artale et al., 2002; Calvanese et al., 1998]. A serious obstacle for putting this general idea to work is posed by the fact that for many natural temporal conceptual formalisms and their associated TDLs, reasoning turns out to be undecidable.

The most prominent witnesses of this problem are the various temporal entity-relationship (TER) models used to design temporal databases [Chomicki and Toman, 2005]. TERs are classical ER data models extended with two additional classes of constraints that model the temporal evolution of data in an application domain [Spaccapietra et al., 1998]. First, timestamping constraints are used to distinguish temporal and atemporal components of a TER model. Timestamping is usually implemented by marking entities (i.e., classes), relationships and attributes as snapshot, temporary, or unrestricted. The idea behind such a classification is to express that object membership in entities, relationships, and attribute values cannot or must change in time; this is achieved by snapshot and temporary marks in the diagram, respectively. Second, evolution constraints govern object migration between entities and can state, for example, that every instance of the entity Child will eventually become an instance of the entity Adult.

∗The research was supported by EU IST-2005-7603 FET Project TONES and by NSERC.

TER models with both timestamping and evolution constraints can be translated into the TDL DLRUS [Artale et al., 2002]. Unfortunately, reasoning in this logic is undecidable. Moreover, the computational problems are not due to the translation to TDLs: even direct reasoning in the generally less powerful TER models is undecidable [Artale, 2004]. There are two principal ways around this problem. The first approach restricts the application of timestamping: it allows arbitrary timestamping of entities, but gives up timestamping of relationships and attributes (i.e., all relationships and attributes are unrestricted). This re-establishes decidability of TER models with restricted timestamping and evolution constraints [Artale et al., 2002]. The second approach to regaining decidability allows for full use of timestamping, but prohibits the use of evolution constraints.

This second alternative is pursued in the current paper. We devise a multi-dimensional description logic S5ALCQI that is obtained by combining the modal logic S5 with the standard DL ALCQI. The S5 modality can be applied to both concepts and roles; axioms in the TBox are, however, interpreted globally. This logic can be viewed as a description logic of change: it can express that concept and role memberships change in time, but does not permit discriminating between changes in the past or future. We show that TER models with full timestamping (i.e., timestamping on entities, relationships, and attributes) but without evolution constraints can be captured by S5ALCQI TBoxes.

The main contribution of this paper is to show that reasoning in S5ALCQI is decidable. We also pinpoint the exact computational complexity by showing 2-EXPTIME completeness. Thus, adding the S5 change modality pushes the complexity of ALCQI, which is EXPTIME-complete, by one exponential. Our upper bound can be viewed as an extension of the decidability result for a simpler multi-dimensional DL, S5ALC, [Gabbay et al., 2003] which is not capable of capturing TER models. However, we had to develop completely new proof techniques as the decidability proof for S5ALC relies on the ability to duplicate points in a model, which is impossible in the presence of S5ALCQI's number restrictions. Our lower bound applies also to S5ALC, hence we show that this logic is also 2-EXPTIME-complete.

The paper is organized as follows. Section 2 introduces the logic S5ALCQI. Section 3 shows that reasoning in S5ALCQI is decidable in 2-EXPTIME by first providing a tree abstraction of S5ALCQI interpretations and then presenting a 2EXPTIME procedure that checks for the existence of such a tree abstraction. Section 4 illustrates how S5ALCQI is able to capture conceptual models with timestamping constraints. Full proofs and the 2-EXPTIME lower bound can be found in the full version of this paper [Artale et al., 2006].

2 The Logic S5ALCQI

The logic S5ALCQI combines the modal logic S5 and the description logic ALCQI in a spirit similar to the multidimensional DLs [Gabbay et al., 2003; Wolter and Zakharyaschev, 1999]. The syntax of S5ALCQI is defined as follows. Let N C and N R be disjoint and countably infinite sets of concept names and role names. We assume that N R is partitioned into two countably infinite sets N glo and N loc of global role names and local role names. The set ROL of roles is defined as {r, r-, ✸r, ✸r-, ✷r, ✷r- | r ∈ N R}. The set of concepts CON is defined inductively as follows: N C ⊆ CON; if C, D ∈ CON, r ∈ ROL, and n ∈ N, then the following are also in CON: ¬C, C ⊓ D, (⩾ n r C), and ✸C. A TBox is a finite set of general concept inclusions (GCIs) C ⊑ D with C, D ∈ CON.

An S5ALCQI-interpretation I is a pair (W, I) with W a non-empty set of worlds and I a function assigning an ALCQI-interpretation I(w) = (Δ, ·I,w ) to each w ∈ W, with Δ a fixed non-empty set called the domain and ·I,w a function mapping each A ∈ N C to a subset AI,w ⊆ Δ and each r ∈ N R to a relation rI,w ⊆ Δ×Δ; for r ∈ N glo we additionally require rI,w = rI,v for all w, v ∈ W. We extend the mapping ·I,w to complex roles and concepts as follows:

An S5ALCQI -interpretation I = (W, I) is a model of a TBox T iff it satisfies CI,w ⊆ DI,w for all C ⊑ D ∈ T and w ∈ W. It is a model of a concept C if CI,w ̸= ∅ for some w ∈ W. A concept C is satisfiable w.r.t. a TBox T if there exists a common model of C and T . Note that when S5ALCQI is considered a temporal description logic, the elements of W correspond to time points. We do not distinguish between global and local concept names because a concept name A can easily be enforced to be global using the GCI A ⊑ ✷A.

The concept constructors C ⊔ D, ∃r.C, ∀r.C, (⩽ n r C), (= n r C), ✷C, ⊤, and ⊥ are defined as abbreviations in the usual way. For roles, we allow only single applications of S5 modalities and inverse. It is easily seen that roles obtained by nesting modal operators and inverse in an arbitrary way can be converted into an equivalent role in our simple form: multiple temporal operators are absorbed and inverses commute with temporal operators.

The fragment S5ALC of S5ALCQI is obtained by allowing only roles of the form r, ✸r, and ✷r, and replacing the concept constructor (⩾ n r C) by ∃r.C. We note that neither S5ALC nor S5ALCQI enjoys the finite model property: there are concepts and TBoxes that are only satisfiable in models with both an infinite set of worlds W and an infinite domain Δ. An example of this phenomenon is the concept ¬C and the TBox {¬C ⊑ ✸C, C ⊑ ∃r.¬C, ¬C ⊑ ∀r.¬C}, with r ∈ N glo.

3 Reasoning in S5ALCQI

We show that in S5ALCQI, satisfiability w.r.t. TBoxes is decidable in 2-EXPTIME. For simplicity, throughout this section we assume that only local role names are used. This can be done w.l.o.g. as global role names can be simulated by ✷r, for r a fresh local role name. Let C0 and T be a concept and a TBox whose satisfiability is to be decided. We introduce the following notation. For roles r, we use Inv(r) to denote r- if r ∈ N R, s if r = s-, ✸Inv(s) if r = ✸s, and ✷Inv(s) if r = ✷s. We use rol(C0, T ) to denote the smallest set that contains all sub-roles used in C0 and T and is closed under Inv. We use cl(C0, T ) to denote the smallest set containing all sub-concepts appearing in C0 and T that is closed under negation: if C ∈ cl(C0, T ) and "¬" is not the top level operator in C, then ¬C ∈ cl(C0, T ).

In the rest of this section we devise tree abstractions of models of C0 and T which we call (C0, T )-trees. In the subsequent section, we then show how to construct looping tree automata that accept the (C0, T )-trees and thus reduce satisfiability in S5ALCQI to the emptiness problemof looping tree automata, yielding decidability of S5ALCQI .

3.1 Tree Abstractions of S5ALCQI models

Intuitively, for a (C0, T )-tree τ that abstracts a model I of C0 and T , the root node of τ corresponds to an object x in I that realizes C0. Successors of the root in τ correspond to objects in I that can be reached from x by traversing a role in some S5 world. Similarly, further nodes in τ correspond to objects of I reachable from x by traversing multiple roles. To describe the concept and role interpretations of I in its abstraction τ, we decorate the nodes of τ with extended quasistates as introduced in Definition 3 below. Extended quasistates are defined in terms of types and quasistates, which we introduce first. Intuitively, a type describes the concept memberships of a domain element x ∈ Δ in a single S5 world.

Definition 1 (Type). A type t for C0, T is a subset of cl(C0, T ) such that

We use tp(C0, T ) to denote the set of all types for C0 and T . To describe the concept memberships of a domain element in all S5 worlds, we use quasistates:

Definition 2 (Quasistate). Let W be a set and f : W → tp(C0, T ) a function such that for all w ∈ W we have:

We call the pair (W, f) a quasistate witness and the set {f(v) | v ∈ W} a quasistate.

To check whether a set of types {t1, . . . , tn} forms a valid quasistate, we can simply check whether the pair (W, f ), with W = {t1, . . . , tn} and f the identity function, is a quasistate witness. Note, however, that each quasistate has many witnesses.

Quasistates only abstract concept membership of a particular object in all worlds. To capture the role structure relating objects adjacent in some S5 world in a given S5ALCQI model, we develop the notion of a extended quasistate. Ultimately, in the desired tree abstraction these two objects turn into a parent and a child nodes; the child is then labeled by the extended quasistate in question. Note the similarity to handling inverse roles using the double blocking technique used in tableau algorithms for ALCQI [Horrocks et al., 1999].

Definition 3 (Extended Quasistate). Let W be a set, (W, f) and (W, g) quasistate witnesses, and h : W → rol(C0, T ) ∪ {✷ε} for ε ̸∈ rol(C0, T ) such that, for every r ∈ N R ∪ {s- | s ∈ N R}:

1. if h(w) = ✸r, for some w ∈ W, then h(v) = r, for some v ∈ W;
2. if h(w) = r, for some w ∈ W, then either h(v) = ✸r or h(v) = r, for all v ∈ W;
3. it is not the case that h(w) = r for all w ∈ W;
4. if h(w) = ✷r, for some w ∈ W, then h(v) = ✷r, for all v ∈ W.

We call (W, f, g, h) an extended quasistate witness and the set of triples Q(W, f, g, h) = {(f(v), g(v), h(v)) | v ∈ W} an extended quasistate. Elements of Q(W, f, g, h) are called extended types and etp(C0, T ) denotes the set of all extended types for C0 and T . We say that Q(W, f, g, h) realizes a concept C if C ∈ f(w) for some w ∈ W; we say that Q(W, f, g, h) is root if h(w) = ✷ε for all w ∈ W.

Intuitively, given a node labeled with the extended quasistate witness (W, f, g, h), the quasistate witness (W, f) describes the node which is labeled with the extended quasistate, (W, g) describes the predecessor of this node, and h describes the role connections between the two nodes. Conditions 1 to 4 ensure that the mapping h assigns roles in a way that respects the semantics of modal operators. To fully understand these conditions, note that we assume an ordering ✸r ≤ r ≤ ✷r between roles which allows us to use a single role in the extended quasistate to capture all the implied roles. The dummy role ε is intended only for use with the root object, which does not have a predecessor.

We now introduce the concept of a matching successor. The main difficulty is to properly capture the effects of qualified number restrictions (⩾ n r C) which constrain the possible combinations of extended quasistates in (C0, T )-trees:

the extended quasistates assigned to children nodes must satisfy the qualified number restrictions of the parent node.

Definition 4 (Matching Successor). Let W and Γ be sets, x /∈ Γ, and let e be a function mapping each y ∈ Γ∪{x} to an extended quasistate witness (W, fy, gy, hy) such that gy = fx for all y ∈ Γ. We call (W, Γ, x, e) a matching successor witness if for all w ∈ W:

1. if (⩾ n r C) ∈ fx(w) and C ̸∈ gx(w) or Inv(r) ̸≤ hx(w) then |{y ∈ Γ | r ≤ hy(w), C ∈ fy(w)}| ≥ n,
2. if (⩾ n r C) ∈ fx(w), then |{y ∈ Γ | r ≤ hy(w),C ∈ fy(w)}| ≥ n - 1,
3. if (⩾ n r C) ∈ cl(T ,C0), C ∈ gx(w), and Inv(r) ≤ hx(w), and |{y ∈ Γ | r ≤ hy(w), C ∈ fy(w)}| ≥ n - 1 then (⩾ n r C) ∈ fx(w),
4. if (⩾ n r C) ∈ cl(T ,C0) and |{y ∈ Γ | r ≤ hy(w), C ∈ fy(w)}| ≥ n then (⩾ n r C) ∈ fx(w).

The pair (Q(W, fx, gx, hx), {Q(W, fy, gy, hy) | y ∈ Γ}) is called a matching successor,.

We say that two matching successor witnesses are equivalent if they define the same matching successor.

The intuition behind this definition is as follows: the object x stands for a parent node (described by fx) and the set of objects Γ for all its children (described by fy). The extended quasistates are chosen in a consistent way w.r.t. the information that is represented twice: the parent part of the extended quasistates labeling the children matches the quasistate attached to the parent itself (i.e., gy = fx for all y ∈ Γ). A matching successor witness is then a witness such that the extended quasistates attached to x and to all elements of Γ can be used to build a part of a model of C0 and T without violating any qualifying number restrictions. Also, the domain of such a model is eventually built from the objects {x} ∪ Γ. As already mentioned, matching successors are the most crucial ingredient to the definition of (C0, T )-trees.

Definition 5 ((C0, T )-tree). Let τ = (N,E,G, n0) be a tuple such that (N,E) is a tree with root n0 ∈ N and G a mapping of τ's nodes to extended quasistates. Then τ is a (C0, T )-tree if:

1. G(n0) realizes C0;
2. G(n0) is root;
3. for all n ∈ N, the pair (G(n), {G(m) | (n,m) ∈ E}) is a matching successor.

Note that the matching successor witnesses induced by the matching successors consisting of the extended quasistates associated with a node and its children in the (C0, T )-tree do not necessarily share the same set W. This poses a difficulty when showing that (C0, T )-trees are proper abstractions of models of C0 and T : when we want to convert such a tree into an interpretation, we need to decide on a common set of worlds W. This difficulty can be overcome using the following lemma, which shows that we can assume that all extended quasistate witnesses are based on sets of world W of identical cardinality.

Lemma 6 (CompatibleMatching Successor). There exists an infinite cardinal α such that the following holds: for every matching successor witness (W, Γ, x, e), there is a matching successor witness (W ′ , Γ, x, e′ ) such that

• (W, Γ, x, e) and (W ′ , Γ, x, e′ ) define the same matching successor and;
• for all y ∈ Γ ∪ {x} and all extended types ν ∈ Q(W ′ , f ′y, g′y, h′y), we have:

Intuitively, the Lemma is proved by replicating elements of W a sufficient number of times. When all extended quasistate witnesses for a (C0, T )-tree are based on a set of worlds of identical cardinality, we can connect these extended quasistate witnesses to a model by simply permuting the set W in an appropriate way. In this way, we can prove the difficult right-to-left direction of the following theorem.

Theorem7. C0 is satisfiable w.r.t. T iff a (C0, T )-tree exists.

3.2 Decidability and Complexity of S5ALCQI

We now develop an effective procedure to check whether there exists a (C0, T )-tree for a given concept C0 and TBox T . We also show that the procedure runs in 2-EXPTIME. Since it is easy to see that the number of all possible matching successors (q,Q) is 3-exponential, we cannot simply generate all of them and check whether they give rise to a (C0, T )-tree. Instead, we start by showing that if a (C0, T )- tree exists, then there is one with slim matching successors witnesses only, i.e., all matching successors in this tree are witnessed by matching successor witnesses whose size is at most exponential. In the rest of the paper, let maxC0,T = ∑(⩾m r C)∈cl(C0,T ) m, and n = |cl(C0, T )|.

Lemma 8. Let (W, Γ, x, e) be a matching successor witness for a matching successor (q, Q). Then there is a Q′ ⊆ Q and a matching successor witness (W ′ , Γ′ , x, e′ ) for (q,Q′ ) such that: |Γ′ | ≤ n · 22n · (maxC0,T +1), and |W ′ | ≤ (1 + |Γ′ |) · n · 22n.

We call a matching successor witness slim if it satisfies the cardinality bounds given in the above Lemma. We call a matching successor slim if it has a slim matching successor witness.

To prove Lemma 8, we need to construct the required slim matching successor witness (W ′ , Γ′ , x, e′ ) from (W, Γ, x, e). To this end, we choose a set Γ′ ⊆ Γ and a function μ that associates an extended type μ(y) with every y ∈ Γ′ such that

• μ(y) ∈ Q(W, fy, gy, hy) and
• if ν ∈ Q(W, fz, gz, hz) for some z ∈ Γ \ Γ′ then we have |{y ∈ Γ′ | μ(y) = ν}| =maxC0,T +1.

The function μ tells us which objects in Γ′ can, in every particular world w, be used to fulfill number restrictions that have been originally fulfilled by (extended types of) objects in Γ \ Γ′ .

The set Γ′ , in turn, is the basis to constructing a slim witness as it can always be chosen in a way such that |Γ′ | ≤ |etp(C0, T )|·(maxC0,T +1) ≤ n ·2n ·(maxC0,T +1). Finally, for a witness in which |Γ| is bounded as above, we can simply eliminate superfluous worlds of W to obtain a slim witness. This can be done by keeping at most |etp(C0, T )| ≤ n · 22n worlds for each element of {x} ∪ Γ′ ; those worlds can be chosen fromW independently.

The crucial step of the actual construction is illustrated in Figure 1: consider a particular world w. In the original witness the number restrictions in the parent object are fulfilled, e.g., by the objects yl+1, . . . , yn with ym, . . . , yn falling outside of the set Γ′ . Assume first, for simplicity, that the objects ym, . . . , yn have been assigned a common extended type ν. We then pick objects y1, . . . , yl ∈ Γ such that μ(y1) = · · · = μ(yl) = ν. Since n - m + 1 ≤ maxC0,T we can always find l ≤ maxC0,T + 1 of such objects in Γ′ such that l = n - m+ 2; follows from the definition of Γ′ . Thus we can transform the old witness to a new one as depicted in Figure 1. Whenever more than one extended type is associated with ym, . . . , yn in the original witness, we simply pick objects in Γ′ with an appropriate matching μ value and proceed similarly to the above example. To construct a slim matching successor witness we fix the set Γ′ and apply this transformation to all w ∈ W independently. Note that the transformation preserves quasistates associated with all objects in Γ′ (hence all S5 modalities are preserved) and that all number restrictions are met.

Lemma 9. There is a procedure that runs in 2-EXPTIME to We simply use a brute-force approach to enumerate all candidates for slim matching successor witnesses up to exponentially sized Γ and W and test for satisfaction of the conditions in Definition 4.

As the next step, we show that whenever a (C0, T )-tree exists, then there is a (C0, T )-tree constructed solely from slim matching successors, i.e., (G(n), {G(m) | (n,m) ∈ E}) is a slim matching successor for all n ∈ N. We call such a (C0, T )-tree slim.

Lemma 10. For any C0 and T , a slim (C0, T )-tree exists whenever a (C0, T )-tree exists.

Since the children in a slim matching successor are a subset of the children in the original matching successor, it is easy to convert an arbitrary (C0, T )-tree into a slim one.

Finally, to check whether a slim (C0, T )-tree exists we define a looping tree automaton AC0,T that accepts exactly the slim (C0, T )-trees. To check satisfiability of C0 w.r.t. T , it then suffices to check whether this looping automaton accepts at least one such tree. This observation yields a 2-EXPTIME decision procedure for satisfiability in S5ALCQI as the emptiness problem for looping tree automata is decidable in time linear in the size of the automaton [Vardi andWolper, 1986].

We use extended quasistates as states of the automaton AC0,T and slim matching successors to define the transition relation. Since C0, T -trees do not have a constant branching degree, we use amorphous looping automata which are similar to the automata model introduced in [Kupferman and Vardi, 2001] except that in our case the branching degree is bounded and thus the transition relation can be represented finitely in a trivial way.

Definition 11 (Looping Tree Automaton). A looping tree automaton A = (Q,M, I, δ) for an M-labeled tree is defined by a set Q of states, an alphabet M, a set I ⊆ Q of initial states, and a transition relation δ ⊆ Q × M × 2Q.

Let T = (N,E, ℓ, r) be a tree with root r ∈ N and labeling function ℓ : N → M. A run of A on T is a mapping γ : N → Q such that γ(r) ∈ I and (γ(α), ℓ(α), {γ(β) | (α, β) ∈ E}) ∈ δ for all α ∈ N. A looping automaton A accepts those labeled trees T for which there exists a run of A on T.

We construct an automaton for C0 and T as follows.

Definition 12. Let C0 be a concept and T an S5ALCQI TBox. The looping automaton AC0,T = (Q,M, I, δ) is defined by setting M = Q = etp(C0, T ), I := {q ∈ Q | q realizes C0 and q is root}, and δ to the set of those tuples (q, q,Q) such that Q ∈ 2Q and (q,Q) is a slim matching successor for C0 and T .

The following Lemma states that the obtained looping automata behaves as expected.

Lemma 13. τ is a slim (C0, T )-tree iff τ is accepted by AC0,T .

It is easily seen that there are at most 2-EXP many extended quasistates and thus AC0,T has at most 2-EXP many states. To construct the transition function of the automaton, we need to construct all slim matching successors which can be done in 2-EXPTIME by Lemma 9. Since emptiness of looping automata can be checked in polynomial time, the overall decision procedure for satisfiability in S5ALCQI runs in 2EXPTIME. This holds regardless of whether numbers inside number restrictions are coded in unary or in binary.

Theorem 14. Satisfiability in S5ALCQI w.r.t TBoxes is decidable and 2-EXPTIME-complete.

The lower bound in Theorem 14 is obtained by reducing the word problem of exponentially space-bounded, alternating Turing machines. Since the reduction does not use inverse role and qualifying number restrictions, we also obtain a 2EXPTIME lower bound for satisfiability on S5ALC.

Corollary 15. Satisfiability in S5ALC w.r.t TBoxes is decidable and 2-EXPTIME-complete.

4 Capturing Conceptual Schemata

It is known that the TDL ALCQIUS is able to capture the temporal conceptual model ERV T , a TER model that supports timestamping and evolution constraints, IS-A links, disjointness, covering, and participation constraints [Artale et al., 2003]. In ERV T , timestamping is implemented using a marking approach as sketched in the introduction. The translation of atemporal constructs is similar to the one using ALCQIUS; see [Artale et al., 2003] for full details and examples. In the following we briefly recall the translation of atemporal constructs and then show that S5ALCQI is sufficient to capture the fragment of ERV T that has timestamping as the only temporal construct.

When translating ERV T to TDLs, entities E-denoting sets of abstract objects-are mapped into concept names AE and attributes P-denoting functions associating mandatory concrete properties of entities-are mapped into roles names rP interpreted as total functions, which is enforced by the GCI ⊤ ⊑ (= 1 rP ⊤). In S5ALCQI, unrestricted entities and attributes need no special treatment. Properties of snapshot or temporary entities and attributes are captured as follows:

AE ⊑ ✷AE

snapshot entity

AE ⊑ ✸¬AE

temporary entity

AE ⊑ ∃✷rP .⊤ snapshot attribute

AE ⊑ ∀✷rP .⊥ temporary attribute

Relationships-n-ary relations between abstract objects-are translated using reification: each n-ary relationship R is translated into a concept name AR with n global role names r1, . . . , rn. Intuitively, for each instance x ∈ AI,w R , the tuple (y1, . . . , yn) with (x, yi) ∈ rI,w i is a tuple in the relationship R at a time point w. To ensure that every instance of AR gives rise to a unique tuple in R, we use GCIs ⊤ ⊑ (= 1 ri ⊤), for 1 ≤ i ≤ n. To capture snapshot relationships, we assert AR ⊑ ✷AR, while for temporary relationships, we assert AR ⊑ ✸¬AR in the TBox.

Note that the latter GCIs do not fully capture temporary relationships. As an example, consider the interpretation I = ({w1,w2}, I), with Δ = {a, a′ , b, c}, AI,w1 R = {a}, AI,w2 R = {a′}, rI,w1 1 = {(a, b)}, rI,w1 2 = {(a, c)}, rI,w2 1 = {(a′ , b)}, and rI,w2 2 = {(a′ , c)}. Although the GCI

AR ⊑ ✸¬AR (expressing temporary relationships) is satisfied, (b, c) is constantly in the temporary relationship R. This is due to a mismatch between the models of an ERV T schema and the models of its translation into S5ALCQI. In particular, in models of ERV T , tuples belonging to relationships are unique while in models of the reified translation there may be two distinct objects connected through the global roles ri to the same objects, thus representing the same tuple (e.g. the objects a, a′ in the above interpretation). Then, S5ALCQI models in which the above situation occurs do not directly correspond to any ERV T model. Similarly to [Calvanese et al., 1999], however, it is possible to show that: (i) there are so called safe models of S5ALCQI that are in one-to-one correspondence with ERV T models, and (ii) every satisfiable S5ALCQI concept is also satisfied in a safe model. When reasoning about ERV T schemas, we can thus safely ignore non-safe models. An S5ALCQI interpretation I = (W, I) is safe for an ERV T schema if, for every n-ary relationship R reified with the global functional roles ri, and every w ∈ W, we have the following:

It is not hard to see that: (1) the model in the example above is not safe, and (2) given a safe model, the above GCIs correctly capture the temporal behavior of relationships.

5 Conclusions

This work introduces the modal description logic S5ALCQI as a logic for representing and reasoning in temporal conceptual models with timestamping constraints. A novel technique is used to show decidability and 2-EXPTIMEcompleteness for S5ALCQI. This is also the first decidability result that allows reasoning in temporal conceptual models with timestamping for entities, relationships, and attributes. Furthermore, reasoning on the less expressive logic S5ALC is also shown to be 2-EXPTIME-complete.

This paper leaves several interesting open problems for further investigation. The fine line separating the decidable TDLs from the undecidable ones is not fully explored: we plan to investigate further extensions of S5ALCQI that still enjoy decidability. Two natural candidates are S5ALCQI that allows, in addition to S5 modalities, an irreflexive ✷ (thus enabling statements about everywhere else) and S5ALCQI with temporalized axioms (enabling TBox statements to appear in scope of S5 operators). Another open issue concerns decidability and complexity of S5ALCQI in finite models.

On the knowledge representation side, we believe that a converse translation-from TER with full timestamping to S5ALCQI-is also possible; this result would allow to fully characterize the complexity of reasoning in TER with timestamping. The limits of the expressive power of S5ALCQI w.r.t. various constraints that have appeared in literature on temporal models other than timestamping also remain to be determined.