Interval-based Temporal Reasoning with General TBoxes

1 Motivation

Description Logics (DLs) are a family of formalisms wellsuited for the representation of and reasoning about conceptual knowledge. Whereas most Description Logics represent only static aspects of the application domain, recent research resulted in the exploration of various Description Logics that allow to, additionally, represent temporal information, see, e.g., [Artale and Franconi,2000] for an overview. One approach for temporal reasoning with DLs is to use so-called concrete domains. Concrete domains have been proposed as an extension of Description Logics that allows reasoning about "concrete qualities" of entities of the application domain such as sizes, weights or temperatures [Baader and Hanschke,1991]. As was first described in [Lutz et al.,1997], if a "temporal" concrete domain is employed, then Description Logics with concrete domains are a very useful tool for temporal reasoning. Ontologically, temporal reasoning with concrete domains is usually interval-based but may also be point-based or even both.

In this paper, we define a temporal Description Logic based on concrete domains which uses points as its basic temporal entity, but which may also be used as a full-fledged intervalbased temporal DL. More precisely, the presented logic CC BW extends the basic Description Logic BTBV with a concrete domain that is based on the rationals and predicates BO and BP. The well-known Allen relations can be defined in terms of their endpoints [Allen,1983] thus allowing for (qualitative) interval-based temporal reasoning. Since it is an important feature of DLs that reasoning should be decidable, we prove decidability of the standard reasoning tasks by using an automata-theoretic approach which also yields a tight EXPTIME complexity bound.

Most DLs allow for some kind of TBox formalism that is used to represent terminological knowledge as well as background knowledge about the application domain. However, there exist various flavours of TBoxes with vast differences in expressivity. To the best of our knowledge, all intervalbased DLs and all DLs with concrete domains defined in the literature admit only a very restricted form of TBox, i.e., sets of acyclic macro definitions. Compared to existing Description Logics that are interval-based or include concrete domains, the distinguishing feature of our logic is that it is equipped with a very general form of TBoxes that allows arbitrary equations over concepts. Thus, the presented work overcomes a major limitation of both families of Description Logics.

Our results can be viewed from the perspective of intervalbased temporal reasoning and from the perspective of concrete domains. For the temporal perspective, we claim that the combination of general TBoxes and interval-based temporal reasoning is important for many application areas. In this paper, we present process engineering as an example. From the concrete domain perspective, our results can be viewed as follows: in [Lutz,2001], it is shown that, even for very simple concrete domains, reasoning with general TBoxes is undecidable. It was an open question whether there exist interesting concrete domains for which reasoning with general TBoxes is decidable. In this paper, we answer this question to the affirmative. This paper is accompanied by a technical report containing full proofs [Lutz,2000].

2 Syntax and Semantics

In this section, we introduce syntax and semantics of the Description Logic CC BW.

Definition 1. Let  BV ,  CA , and  CRBY be mutually disjoint and countably infinite sets of concept names, roles, and concrete features. Furthermore, let  CPBY be a countably infinite subset of  CA . The elements of  CPBY are called abstract features. A path D9 is a composition CU BD A1 A1 A1 CU D2 CV of D2 AL BC abstract features CU BD BN BM BM BM BN CU D2 and one concrete feature CV. The set of CC BW- concepts is the smallest set such that

1. every concept name is a concept
2. if BV and BW are concepts, CA is a role, CV is a concrete feature, D9 BD BN D9 BE are paths, and  BE CUBOBN BPCV, then the following expressions are also concepts: BMBV, BV D9 BW, BV D8 BW, BLCABMBV, BKCABMBV, BLD9 BD BN D9 BE BM , and CVAY.

A TBox axiom is an expression of the form BV DA BW with BV and BW are concepts. A finite set of TBox axioms is a TBox.

Throughout this paper, we will denote atomic concepts by the letter BT, (possibly complex) concepts by the letters BVBNBWBNBX, roles by the letter CA, abstract features by the letter CU , concrete features by the letter CV, paths by the letter D9, and elements of the set CUBOBN BPCV by the letter . We will sometimes call the TBox formalism introduced above general TBoxes to distinguish it from other, weaker formalisms such as the ones in [Nebel,1990]. As most Description Logics, CC BW is equipped with a Tarski-style semantics.

Definition 2. An interpretation
is a pair B4A1
BN A1
B5, where A1
is a set called the domain and A1
is the interpretation function mapping each concept name BV to a subset BV
of A1
, each role name CA to a subset CA
of A1
A2 A1
, each abstract feature CU to a partial function CU
from A1
to A1
, and each concrete feature CV to a partial function CV
from A1
to the rationals . For paths D9 BP CU BD A1 A1 A1 CU D2 CV, we set D9
B4CPB5 BMBP CV
B4CU
D2 B4A1 A1 A1 B4CU
BD B4CPB5B5 A1 A1 A1 B5B5. The interpretation function is extended to arbitrary concepts as follows:

An interpretation
is a model of a TBox CC iff it satisfies C
AI D
for all axioms BV DA BW in CC .
is a model of a concept BV iff BV
BIBP BN.

If CVB4CPB5 BP DC for some CV BE  CRBY , CP BE A1
, and DC BE , then we call DC a concrete successor of CP in
. We write BQ for BTD8BMBT and BR for BMBQ, where BT is a concept name. Moreover, we write D9AY with D9 BP CU BD A1 A1 A1 CU CZ CV for BKCU BD BM A1 A1 A1 BKCU CZ BMCVAY.

Definition 3 (Inference Problems). Let BV and BW be concepts and CC be a TBox. BV subsumes BW w.r.t. CC (written BW DA CC BV) iff BW
AI BV
for all models
of CC . BV is satisfiable w.r.t. CC iff there exists a model of both CC and BV.

It is well-known that (un)satisfiability and subsumption can be mutually reduced to each other: BV DA CC BW iff BV D9 BMBW is unsatisfiable w.r.t. CC and BV is satisfiable w.r.t. CC iff BV BIDA CC BR.

We now discuss the relationship between CC BW and Description Logics with concrete domains.

Definition 4 (Concrete Domain). A concrete domain BW is a pair B4A1 BW BN A8 BW B5, where A1 BW is a set called the domain, and A8 BW

is a set of predicate names. Each predicate name  BE A8 BW is associated with an arity D2 and an D2-ary predicate  BW AI A1 D2 BW .

The concrete domain is usually integrated into the logic by a concept constructor BLD9 BD BN BM BM BM BN D9 D2 BM , with semantics

It is obvious that CC BW can be viewed as being equipped with the concrete domain BW BO BMBP B4 BN CUBOBN BPCVB5, where BO and BP are binary predicates with the usual semantics. For most DLs with concrete domains, it is required that the set of predicates is closed under negation and contains a name BQ BW for A1 BW . This property ensures that every concept can be converted into an equivalent one in the so-called negation normal form (NNF). The NNF of concepts, in turn, is used as a starting point for devising satisfiability algorithms. It is not hard to see that BW BO is not admissible in this sense. However, as we will see in Section 4, the conversion of CC BW-concepts into equivalent ones in NNF is nevertheless possible.

3 Temporal Reasoning with CC BW

Although CC BW does only provide the relations "BP" and "BO" on time points, it is not hard to see that the remaining relations can be defined by writing, e.g., BLD9 BE BN D9 BD BMBO D8 BLD9 BD BN D9 BE BM BP for BLD9 BD BN D9 BE BMAL. However, we claim that CC BW cannot only be used for point-based temporal reasoning but also as a full-fledged interval-based temporal Description Logic. As observed by Allen [1983], there are 13 possible relationships between two intervals such as, for example, the D1CTCTD8D7 relation: two intervals CX BD and CX BE are related by D1CTCTD8D7 iff the right endpoint of CX BD is identical to the left endpoint of CX BE -see [Allen,1983] for an exact definition of the other relations. As we shall see, these 13 Allen relations (as well as the additional relations from the Allen algebra, see [Allen,1983]) can be defined in CC BW. In the following, we present a framework for mixed intervaland point-based reasoning in CC BW and apply this framework in the application area of process engineering

The representation framework consists of several conventions and abbreviations. We assume that each entity of the application domain is either temporal or atemporal. If it is temporal, its temporal extension may be either a time point or an interval. Left endpoints of intervals are represented by the concrete feature CO, right endpoints of intervals are represented by the concrete feature D6, and time-points not related to intervals are represented by the concrete feature D8. All this can be expressed by the following TBox CC A3 :

Here, BV BM BP BW is an abbreviation for CUBV DA BWBN BW DA BVCV. Let us now define the Allen relations as abbreviations. For example, BLB4BYBN BY BC B5BMCRD3D2D8CPCXD2D7 is an abbreviation for BLBYCOBN BY BC COBMBO D9 BLBY BC D6BN BYD6BMBO where BYBN BY BC BE B4 CPBY B5 A3 , i.e., BY and BY BC are words over the alphabet  CPBY . Note that

Similar abbreviations are introduced for the other Allen relations. We use D7CTD0CU to denote the empty word. For example, BLB4BYBN D7CTD0CUB5BMD7D8CPD6D8D7 is an abbreviation for BLBY COBN COBM BP D9 BLBYD6BN D6BMBOBM Intuitively, D7CTD0CU refers to the interval associated with the abstract object at which the BLB4BYBN D7CTD0CUB5BMD7D8CPD6D8D7 concept is "evaluated".

Since we have intervals and points available, we should also be able to talk about the relationship of points and intervals. More precisely, there exist 5 possible relations between a point and an interval [Vilain,1982], one example being D7D8CPD6D8D7D4 that holds between a point D4 and an interval CX if D4 is identical to the left endpoint of CX. Hence, we can define BLB4BY D8BN BY BC B5BMD7D8CPD6D8D7D4 as an abbreviation for BLBY D8BN BY BC COBM BP and similar abbreviations for CQCTCUD3D6CTD4, CSD9D6CXD2CVD4, ACD2CXD7CWCTD7D4, and CPCUD8CTD6D4.

This finishes the definition of the framework. We claim that the combination of interval-based reasoning and general TBoxes is important for many application areas such as reasoning about action and plans [Artale and Franconi,2000]. The examples presented here are from the area of process engineering that was first considered by Sattler in a DL context [Sattler,1998]. However, Sattler's approach does not take into account temporal aspects of the application domain. We show how this can be done using CC BW thus refining Sattler's proposal.

Assume that our goal is to represent information about an automated chemical production process that is carried out by some complex technical device. The device operates each day for some time depending on the number of orders. It needs a complex startup and shutdown process before resp. after operation. Moreover, some weekly maintenance is needed to keep the device functional. Let us first represent the underlying temporal structure that consists of weeks and days.

The axiom states that each week consists of seven days, where the CX'th day is accessible from the corresponding week via the abstract feature CSCPDD CX . The temporal relationship between the days are as expected: Monday starts the week, Sunday finishes it, and each day temporally meets the succeeding one. Note that this implies that days 2 to 6 are during the corresponding week although this is not explicitly stated. Moreover, each week has a successor week that it temporally meets. We now describe the startup, operation, shutdown, and maintenance phases.

BWCPDD BM BP 
D2D8CTD6DACPD0 D9 BLD7D8CPD6D8BMCBD8CPD6D8D9D4 D9 BLD3D4BMD4CTD6CPD8CXD3D2 D9 BLD7CWD9D8BMCBCWD9D8CSD2 D9 BLD7D8CPD6D8 Æ COBN COBMAL D9 BLB4D7D8CPD6D8BN D3D4B5BMD1CTCTD8D7 D9 BLB4D3D4BN D7CWD9D8B5BMD1CTCTD8D7 D9 BLD7CWD9D8 Æ D6BN D6BMAK CFCTCTCZ DA BLD1CPCXD2D8BMCPCXD2D8CTD2CPD2CRCT D9 BLB4D7CTD0CU BN D1CPCXD2D8B5BMCRD3D2D8CPCXD2D7

Here D7D8CPD6D8, D3D4, D7CWD9D8, and D1CPCXD2D8 are abstract features and "Æ" is used for better readability (i.e., paths CU BD A1 A1 A1 CU CZ CV are written as CU BD Æ A1 A1 A1 Æ CU CZ Æ CV). The TBox implies that phases are related to the corresponding day as follows: startup via D7D8CPD6D8D7 or CSD9D6CXD2CV, shutdown via CSD9D6CXD2CV or ACD2CXD7CWCTD7, and operation via CSD9D6CXD2CV. Until now, we did not say anything about the temporal relationship of maintenance and operation. This may be inadequate, if, for example, maintenance and operation are mutually exclusive. We can take this into account by using additional axioms

where CE is replaced by CTD5D9CPD0, D3DACTD6D0CPD4D7, D3DACTD6D0CPD4D4CTCS-CQDD, CSD9D6CXD2CV, CRD3D2D8CPCXD2D7, D7D8CPD6D8D7, D7D8CPD6D8CTCS-CQDD, ACD2CXD7CWCTD7, or ACD2CXD7CWCTCS-CQDD yielding 9 axioms.

Until now, we have modelled the very basic properties of our production process. Let us define some more advanced concepts to illustrate reasoning with CC BW. For example, we could define a busy week as

i.e., each day, the startup process starts at the beginning of the day and the shutdown finishes at the end of the day. Say now that it is risky to do maintenance during startup and shutdown phases and define

expressing that, in a risky week, the maintenance phase is not strictly separated from the startup and shutdown phases. A CC BW reasoner could be used to detect that BUD9D7DDCFCTCTCZ DA CACXD7CZDDCFCTCTCZ, i.e., every busy week is a risky week: in a busy week, the week is partitioned into startup, shutdown, and operation phases. Since maintenance may not OVLP with operation phases (see (A3)), it must OVLP with startup and/or shutdown phases which means that it is a risky week. We can further refine this model by using mixed point-based and interval-based reasoning, see [Lutz,2000] for examples.

4 The Decision Procedure

In this section, we prove satisfiability of CC BW-concepts w.r.t. TBoxes to be decidable and obtain a tight EXPTIME complexity bound. This is done using an automata-theoretic approach: first, we abstract models to so-called Hintikka-trees such that there exists a model for a concept BV and a TBox CC iff there exists a Hintikka-tree for BV and CC . Then, we build, for each CC BW-concept BV and TBox CC , a looping automaton BT B4BVBNCC B5 that accepts exactly the Hintikka-trees for B4BVBN CC B5. In particular, this implies that BT B4BVBNCC B5 accepts the empty language iff BV is unsatisfiable w.r.t. CC .

Definition 5. Let  be a set and CZ AL BD. A CZ-ary -tree is a mapping CC BM CUBDBN BM BM BM BN CZCV A3 AX  that labels each node AB BE CUBDBN BM BM BM BN CZCV A3 with CCB4ABB5 BE . Intuitively, the node ABCX is the CX-th child of AB. We use AF to denote the empty word (corresponding to the root of the tree).

A looping automaton BT BP B4 BNBN
BNA1B5 for CZ-ary -trees is defined by a set of states, an alphabet , a subset
AI of initial states, and a transition relation A1 AI A2  A2 CZ . A run of BT on an -tree CC is a mapping D6 BM CUBDBN BM BM BM BN CZCV A3 AX with D6B4AFB5 BE
and B4D6B4ABB5BN CCB4ABB5BN D6B4ABBDB5BN BM BM BM BN D6B4ABCZB5B5 BE A1 for each AB BE

CUBDBN BM BM BM BN CZCV A3 BM A looping automaton accepts all those -trees for which a run exists, i.e., the language B4BTB5 of -trees accepted by BT is

In [Vardi and Wolper,1986], it is proved that the emptiness problem for looping automata is decidable in polynomial time.

A Hintikka-tree for BV and CC corresponds to a canonical model for BV and CC . Apart from describing the abstract domain A1
of the corresponding canonical model
together with the interpretation of concepts and roles, each Hintikkatree induces a directed graph whose edges are labelled with predicates from CUBOBN BPCV. These constraint graphs describe the "concrete part" of
(i.e., concrete successors of domain objects and their relationships).

Definition 6. Aconstraint graph is a pair BZ BP B4CEBNBXB5, where CE is a countable set of nodes and BX AI CE A2CE A2CUBP BN BOCV a set of edges. We generally assume that constraint graphs are equality closed, i.e., that B4DA BD BN DA BE BN BPB5 BE BX implies B4DA BE BN DA BD BN BPB5 BE BX. A constraint graph BZ BP B4CEBN BXB5 is called satisfiable over , where  is a set equipped with a total ordering BO, iff there exists a total mapping Æ from CE to  such that ÆB4DA BD B5  ÆB4DA BE B5 for all B4DA BD BN DA BE BN B5 BE BX. In this case, Æ is called a solution for BZ.

ABO-cycle in BZ is a finite non-empty sequence of nodes DA BC BN BM BM BM BN DA CZA0BD BE CE such that (1) for all CX with CX BO CZ, we have B4DA CX BN DA CXA8 CZ BD BN B5 BE BX, where  BE CUBOBN BPCV and A8 CZ denotes addition modulo CZ and (2) B4DA CX BN DA CXA8 CZ BD BN BOB5 BE BX for some CX BO CZ.

The following theorem will be crucial for proving that, for every Hintikka-tree, there exists a corresponding canonical model. More precisely, it will be used to ensure that the constraint graph induced by a Hintikka-tree, which describes the concrete part of the correspondingmodel, is satisfiable.

Theorem 7. A constraint graph BZ is satisfiable over  with  BE CU BNCACV iff BZ does not contain a BO-cycle.

Note that Theorem 7 does not hold if satisfiability over  is considered due to the absence of density: if there exist two nodes DA BD and DA BE such that the length of BO-paths (which are defined in the obvious way) between DA BD and DA BE is unbounded, a constraint graph is unsatisfiable over  even if it contains no BO-cycle, see Figure 1.

The decidability procedure works on CC BW-concepts and TBoxes that are in a certain syntactic form.

Definition 8 (Path Normal Form). A CC BW-concept BV is in path normal form (PNF) if, for all subconcepts BLD9 BD BN D9 BE BM of BV, we have either (1) D9 BD BP CV BD and D9 BE BP CV BE , (2) D9 BD BP CUCV BD and D9 BE BP CV BE , or (3) D9 BD BP CV BD and D9 BE BP CUCV BE for some CU BE  CPBY and CV BD BN CV BE BE  CRBY . A CC BW TBox CC is in path normal form iff all concepts appearing in CC are in path normal form.

Lemma 9. Satisfiability of CC BW-concepts w.r.t. CC BW- TBoxes can be reduced to satisfiability of CC BW-concepts in PNF w.r.t. CC BW-TBoxes in PNF.

Proof Let BV be a CC BW concept. For every path D9 BP CU BD A1 A1 A1 CU D2 CV in BV, we assume that CJCVCLBN CJCU D2 CVCLBN BM BM BM BN CJCU BD A1 A1 A1 CU D2 CVCL are concrete features. We inductively define a mapping AL from paths D9 in BV to concepts as follows:

For any CC BW-concept BV, a corresponding concept AQB4BVB5 in PNF is obtained by replacing all subconcepts BLD9 BD BN D9 BE BM of BV with BLCJD9 BD CLBN CJD9 BE CLBM D9 ALB4D9 BD B5 D9 ALB4D9 BE B5 and CVAY with CJCVCLAY. We extend the mapping AQ to TBoxes in the obvious way. It is easy to check that the translation is polynomial and that a concept BV is satisfiable w.r.t. a TBox CC iff AQB4BVB5 is satisfiable w.r.t. AQB4CC B5. ❏

Hence, it suffices to prove that satisfiability of concepts in PNF w.r.t. TBoxes in PNF is decidable. Moreover, we can assume all concepts and TBoxes to be in NNF.

Definition 10 (NNF). A concept BV is in negation normal form (NNF) if negation occurs only in front of concept names. Every concept can be transformed into an equivalent one in NNF by eliminating double negation and using de Morgan's law, the duality between BL and BK, and the following equivalences:

where CT A1 denotes the exchange of predicates, i.e., CT BO is BP and CT BP is BO. With D2D2CUB4BVB5, we denote the equivalent of BV in NNF. A TBox CC is in NNF iff all concepts in CC are in NNF.

Note that transformation to NNF preserves PNF. We often refer to TBoxes CC in their concept form BV CC :

We now define Hintikka-trees for concepts BV and TBoxes CC (in PNF and NNF) and show that there exists Hintikka-tree for BV and CC iff there exists a model for BV and CC .

Let BV be a concept and CC a TBox. With CRD0B4BVBN CC B5, we denote the set of subconcepts of BV and BV CC . We assume that existential concepts BLCABMBW in CRD0B4BVBN CC B5 with CA BE  CA D2  CPBY are linearly ordered, and that BX B4BVBN CC BN CXB5 yields the CX-th existential concept in CRD0B4BVBN CC B5. Furthermore, we assume the abstract features used in CRD0B4BVBN CC B5 to be linearly ordered and use BY B4BVBN CC BN CXB5 to denote the CX-th abstract feature in CRD0B4BVBN CC B5. The set of concrete features used in CRD0B4BVBN CC B5 is denoted with BZ B4BVBN CC B5. Hintikka-pairs are used as labels of the nodes in Hintikka-trees.

Definition 11 (Hintikka-set, Hintikka-pair). Let BV be a concept and CC be a TBox. A set A9 AI CRD0B4BVBN CC B5 is a Hintikkaset for B4BVBN CC B5 iff it satisfies the following conditions:

• (H1) BV CC BE A9,
• (H2) if BV BD D9BV BE BE A9, then CUBV BD BNBV BE CV AI A9,
• (H3) if BV BD D8BV BE BE A9, then CUBV BD BNBV BE CV CKA9 BIBP BN,
• (H4) CUBTBN BMBTCV BIAI A9 for all concept names BT BE CRD0B4BVBN CC B5,
• (H5) if CVAY BE A9, then BLD9 BD BN D9 BE BM BPBE A9 for all concepts BLD9 BD BN D9 BE BM with D9 BD BP CV or D9 BE BP CV.

We say that CU BE  CPBY is enforced by a Hintikkaset A9 iff either BLCUBMBV BE A9 for some concept BV or CUBLCUCV BD BN CV BE BMBN BLCV BD BN CUCV BE BMCV CK A9 BIBP BN for some CV BD BN CV BE BE  CRBY and  BE CUBOBN BPCV. A Hintikka-pair B4A9BN AVB5 for B4BVBN CC B5 consists of a Hintikka-set A9 for B4BVBN CC B5 and a set AV of tuples B4CV BD BN CV BE BN  B5 with CV BD BN CV BE BE BZ B4BVBN CC B5 such that

With A0 B4BVBNCC B5 , we denote the set of all Hintikka-pairs for B4BVBN CC B5. A path D9 (of length 1 or 2) is enforced by B4A9BN AVB5 iff either D9 is a node in AV or CUBLD9BN D9 BC BMBN BLD9 BC BN D9BMCVCKA9 BIBP BN for some path D9 BC and  BE CUBOBN BPCV.

Intuitively, each node AB of a (yet to be defined) Hintikkatree CC corresponds to a domain object CP of the corresponding canonical model
. The first component A9 AB of the Hintikkapair labelling AB is the set of concepts from CRD0B4BVBN CC B5 satisfied by CP. The second component AV AB states restrictions on the relationship between concrete successors of CP. If, for example, B4CV BD BN CV BE BNBOB5 BE AV AB , then we must have CV
BD B4CPB5 BO CV
BE B4CPB5. Note that the restrictions in AV AB are independent from concepts BLCV BD BN CV BE BM BE A9 AB . As will become clear when Hintikkatrees are defined, the restrictions in AV AB are used to ensure that the constraint graph induced by the Hintikka-tree CC, which describes the concrete part of the model
, does not contain a BO-cycle, i.e., that it is satisfiable. This induced constraint graph can be thought of as the union of smaller constraint graphs, each one being described by a Hintikka-pair labelling a node in CC . These pair-graphs are defined next.

Definition 12 (Pair-graph). Let BV be a concept, CC a TBox, and D4 BP B4A9BN AVB5 a Hintikka-pair for B4BVBN CC B5. The pair-graph BZB4D4B5 BP B4CEBN BXB5 of D4 is a constraint graph defined as follows:

1. CE is the set of paths enforced by D4

An edge extension of BZB4D4B5 is a set BX BC AI CE A2CE A2CUBOBN BPCV such that for all CUCV BD BN CUCV BE BE CE , we have either B4CUCV BE BN CUCV BD BN BOB5 BE BX BC or B4CUCV BD BN CUCV BE BN B5 BE BX BC for some  BE CUBOBN BPCV. If BX BC is an edge extension of BZB4D4B5, then the graph B4CEBN BXCJBX BC B5 is a completion of BZB4D4B5.

Note that, due to path normal form and the definitions of Hintikka-pairs and pair-graphs, we have BX BC CKBX BP BN for every edge extension BX BC of a pair-graph B4CEBN BXB5.

We briefly comment on the connection of completions and the AV-component of Hintikka-pairs. Let AB and AC be nodes in a Hintikka-tree CC and let CP and CQ be the corresponding domain objects in the corresponding canonical model
. Edges in Hintikka-trees represent role-relationships, i.e., if AC is successor of AB in CC, then there exists an CA BE  CA such that B4CPBN CQB5 BE CA
. Assume AC is successor of AB and the edge between AB and AC represents relationship via the abstract feature CU , i.e., we have CU
B4CPB5 BP CQ. The second component AV AC of the Hintikka-pair labelling AC fixes the relationships between all concrete successors of CQ that "CP talks about". For example, if B4BLCUCV BD BN CV BE BM BPB5 BE A9 AB and B4BLCUCV BF BN CV BE BM BOB5 BE A9 AB , where A9 AB is the first component of the Hintikka-pair labelling AB, then "CP talks about" the concrete CV BD -successor and the concrete CV BF -successor of CQ. Hence, AV AC either contains B4CV BF BN CV BD BN BOB5 or B4CV BD BN CV BF BN B5 for some  BE CUBOBN BPCV. This is formalized by demanding that the pair-graph BZB4CCB4ABB5B5 of the Hintikka-pair labelling AB together with all the edges from the AV-components of the successors of AB are a completion of BZB4CCB4ABB5B5. Moreover, this completion has to be satisfiable, which is necessary to ensure that the constraint graph induced by CC does not contain a BO-cycle. An appropriate way of thinking about the AVcomponents is as follows: at AB, a completion of BZB4CCB4ABB5B5 is "guessed". The additional edges are then "recorded" in the AV-components of the successor-nodes of AB.

Definition 13 (Hintikka-tree). Let BV be a concept, CC be a TBox, CZ the number of existential subconcepts in CRD0B4BVBN CC B5, and CO be the number of abstract features in CRD0B4BVBN CC B5. A BDB7CZB7 CO-tuple of Hintikka-pairs B4D4 BC BN BM BM BM BN D4 CZB7CO B5 with D4 CX BP B4A9 CX BN AV CX B5 and BZB4D4 BC B5 BP B4CEBN BXB5 is called matching iff

• (H7) if BLCABMBW BE A9 BC and BX B4BVBN CC BN CXB5 BP BLCABMBW, then BW BE A9 CX
• (H8) if CUBLCABMBWBN BKCABMBXCV AI A9 BC and BX B4BVBN CC BN CXB5 BP BLCABMBW, then BX BE A9 CX
• (H9) if BLCUBMBW BE A9 BC and BY B4BVBN CC BN CXB5 BP CU, then BW BE A9 CZB7CX .
• (H10) if CU is enforced by A9 BC , BY B4BVBN CC BN CXB5 BP CU, and BKCUBMBW BE A9 BC , then BW BE A9 CZB7CX .

(H11) the constraint graph B4CEBNBX CJ BX BC B5 is a satisfiable completion of BZB4D4 BC B5, where BX BC is defined as

A CZ B7 CO-ary A0 B4BVBNCC B5 -tree CC is a Hintikka-tree for B4BVBN CC B5 iff CC B4ABB5 is a Hintikka-pair for B4BVBN CC B5 for each node AB in CC , and CC satisfies the following conditions:

For a Hintikka-tree CC and node AB BE CUBDBN BM BM BM BN CZ B7 COCV A3 with CCB4ABB5 BP B4A9BN AVB5, we use CC A1 B4ABB5 to denote A9 and CC A3 B4ABB5 to denote AV. Moreover, if BZB4ABB5 BP B4CEBNBXB5, we use CRD4D0B4CCBN ABB5 to denote the constraint graph B4CEBN BX CJ BX BC B5 as defined in (H11).

Whereas most properties of Hintikka-trees deal with concepts, roles, and abstract features and are hardly surprising, (H11) ensures that constraint graphs induced by Hintikkatrees contain no BO-cycle. By "guessing" a completion as explained above, possible BO-cycles are anticipated and can be detected locally, i.e., it suffices to check that the completions CRD4D0B4CCBN ABB5 are satisfiable as demanded by (H11). Indeed, it is crucial that the cycle detection is done by a local condition since we need to define an automaton which accepts exactly Hintikka-trees and automata work locally. It is worth noting that the localization of cycle detection as expressed by (H11) crucially depends on path normal form.

The following two lemmas show that Hintikka-trees are appropriate abstractions of models.

Lemma 14. A concept BV is satisfiable w.r.t. a TBox CC iff there exists a Hintikka-tree for B4BVBN CC B5.

To prove decidability, it remains to define a looping automaton BT B4BVBNCC B5 for each concept BV and TBox CC such that BT B4BVBNCC B5 accepts exactly the Hintikka-trees for B4BVBN CC B5.

Definition 15. Let BV be a concept, CC be a TBox, CZ the number of existential subconcepts in CRD0B4BVBN CC B5, and CO be the number of abstract features in CRD0B4BVBN CC B5. The looping automaton BT B4BVBNCC B5 BP B4 BN A0 B4BVBNCC B5 BNA1BN
B5 is defined as follows:

• AF BP A0 B4BVBNCC B5 ,
  BP CUB4A9BN AVB5 BE CY BV BE A9CV, and
• AF B4B4A9BN AVB5BN B4A9 BC BN AV BC B5BN B4A9 BD BN AV BD B5BN BM BM BM BN B4A9 CZ BN AV CZB7CO B5B5 BE A1 iff

Note that every state is an accepting state, and, hence, every run is accepting. The following lemma is easily obtained.

Since the size of CRD0B4BVBN CC B5 is linear in the size of BV and CC , it is straightforward to verify that the size of BT B4BVBNCC B5 is exponential in the size of BV and CC . This, together with Lemmas 9, 14, and 16, and the polynomial decidability of the emptiness problem of looping automata [Vardi and Wolper,1986], implies the upper bound given in the following theorem which states the main result of this paper. The lower bound is an immediate consequence of the fact that BTBV with general TBoxes is EXPTIME-hard [Schild,1991].

Theorem 17. Satisfiability and subsumption of CC BW- concepts w.r.t. TBoxes are EXPTIME-complete.

5 Conclusion

There are several perspectives for future work of which we highlight three rather interesting ones: firstly, the presented decision procedure is only valid if a dense strict linear order is assumed as the underlying temporal structure. For example, the concept BQ is satisfiable w.r.t. the TBox

over the temporal structures and CA (with the natural orderings) but not over . To see this, note that CC induces a constraint graph as in Figure 1. Hence, it would be interesting to investigate if and how the presented algorithm can be modified for reasoning with the temporal structure .

Secondly, CC BW does only allow for qualitative temporal reasoning. It would be interesting to extend the logic to mixed qualitative and quantitative reasoning by additionally admitting unary predicates BO D5 and BP D5 for each D5 BE .

Thirdly, we plan to extend CC BW to make it suitable for reasoning about entity relationship (ER) diagrams. As demonstrated in, e.g., [Calvanese et al.,1998; Artale and Franconi,1999], Description Logics are well-suited for this task. By using an appropriate extension of CC BW, one should be able to capture a new kind of temporal reasoning with ER diagrams, namely reasoning over ER diagrams with "temporal" integrity constraints. For example, a temporal integrity constraint could state that employees birthdays should be before their employment date. An appropriate extension of CC BW for this task could be by (unqualified) number restrictions, inverse roles, and a generalized version of the concrete domain constructor BLD9 BD BN D9 BE BM . An extension of the presented automata-theoretic decision procedure to this more complex logic seems possible.

Acknowledgements My thanks go to Franz Baader, Ulrike Sattler, and Stephan Tobies for fruitful discussions. The author was supported by the DFG Project BA1122/3-1 "Combinations of Modal and Description Logics".