Temporal Description Logics: A Survey <s> Varying the DL Component <s> Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical. We present an algorithm that decides satisfiability of the DL ALC extended with transitive and inverse roles and functional restrictions with respect to general concept inclusion axioms and role hierarchies; early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC extended with just transitive and inverse roles is still in PSPACE. We investigate the limits of decidability for this family of DLs, showing that relaxing the constraints placed on the kinds of roles used in number restrictions leads to the undecidability of all inference problems. Finally, we describe a number of optimisation techniques that are crucial in obtaining implementations of the decision procedures, which, despite the worst-case complexity of the problem, exhibit good performance with real-life problems. <s> BIB001 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> Abstract In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps. <s> BIB002 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> This paper introduces a new logical formalism, intended for temporal conceptual modelling, as a natural combination of the well-known description logic DLR and point-based linear temporal logic with Since and Until. We define a query language (where queries are non-recursive Datalog programs and atoms are complex DLRUS expressions) and investigate the problem of checking query containment under the constraints defined by DLRUS conceptual schemas--i.e., DLRUS knowledge bases--as well as the problems of schema satisfiability and logical implication. <s> BIB003 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> I Introduction 1 Modal logic basics 1.1 Modal axiomatic systems 1.2 Possible world semantics 1.3 Classical first-order logic and the standard translation 1.4 Multimodal logics 1.5 Algebraic semantics 1.6 Decision, complexity and axiomatizability problems 2 Applied modal logic 2.1 Temporal logic 2.2 Interval temporal logic 2.3 Epistemic logic 2.4 Dynamic logic 2.5 Description logic 2.6 Spatial logic 2.7 Intuitionistic logic 2.8 'Model level' reductions between logics 3 Many-dimensional modal logics 3.1 Fusions 3.2 Spatio-temporal logics 3.3 Products 3.4 Temporal epistemic logics 3.5 Classical first-order logic as a propositional multimodal logic 3.6 First-order modal logics 3.7 First-order temporal logics 3.8 Description logics with modal operators 3.9 HS as a two-dimensional logic 3.10 Modal transition logics 3.11 Intuitionistic modal logics II Fusions and products 4 Fusions of modal logics 4.1 Preserving Kripke completeness and the finite model property 4.2 Algebraic preliminaries 4.3 Preserving decidability of global consequence 4.4 Preserving decidability 4.5 Preserving interpolation 4.6 On the computational complexity of fusions 5 Products of modal logics: introduction 5.1 Axiomatizing products 5.2 Proving decidability with quasimodels 5.3 The finite model property 5.4 Proving undecidability 5.5 Proving complexity with tilings 6 Decidable products 6.1 Warming up: Kn x Km 6.2 CPDL x K_m 6.3 Products of epistemic logics with Km 6.4 Products of temporal logics with Km 6.5 Products with S5 6.6 Products with multimodal S5 7 Undecidable products 7.1 Products of linear orders with infinite ascending chains 7.2 Products of linear orders with infinite descending chains 7.3 Products of Dedekind complete linear orders 7.4 Products of finite linear orders 7.5 More undecidable products 8 Higher-dimensional products 8.1 S5 x S5 x ... x S5 8.2 Products between K4 x K4 x ... x K4 and S5 x S5 x ... x S5 8.3 Products with the fmp 8.4 Between K x K x ... x K and S5 x S5 x ... x S5 8.5 Finitely axiomatizable and decidable products 9 Variations on products 9.1 Relativized products 9.2 Valuation restrictions 10 Intuitionistic modal logics 10.1 Intuitionistic modal logics with Box 10.2 Intuitionistic modal logics with Box and Diamond 10.3 The finite model property III First-order modal logics 11 Fragments of first-order temporal logics 11.1 Undecidable fragments 11.2 Monodic formulas, decidable fragments 11.3 Embedding into monadic second-order theories 11.4 Complexity of decidable fragments of QLogSU(N) 11.5 Satisfiability in models over (N,<) with finite domains 11.6 Satisfiability in models over (R,<) with finite domains 11.7 Axiomatizing monodic fragments 11.8 Monodicity and equality 12 Fragments of first-order dynamic and epistemic logics 12.1 Decision problems 12.2 Axiomatizing monodic fragments IV Applications to knowledge representation 13 Temporal epistemic logics 13.1 Synchronous systems 13.2 Agents who know the time and neither forget nor learn 14 Modal description logics 14.1 Concept satisfiability 14.2 General formula satisfiability 14.3 Restricted formula satisfiability 14.4 Satisfiability in models with finite domains 15 Tableaux for modal description logics 15.1 Tableaux for ALC 15.2 Tableaux for K(ALC) with constant domains 15.3 Adding expressive power to K(ALC) 16 Spatio-temporal logics 16.1 Modal formalisms for spatio-temporal reasoning 16.2 Embedding spatio-temporal logics in first-order temporal logic 16.3 Complexity of spatio-temporal logics 16.4 Models based on Euclidean spaces Epilogue. Bibliography. List of tables. List of languages and logics. Symbol index. Subject index. <s> BIB004 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> We investigate the computational behaviour of 'two-dimensional' propositional temporal logics over (N, <) (with and without the next-time operator O) that are capable of reasoning about states with transitive relations. Such logics are known to be undecidable (even II 1 1- complete) if the domains of states with those relations are assumed to be constant. Motivated by applications in the areas of temporal description logic and specification & verification of hybrid systems, in this paper we analyse the computational impact of allowing the domains of states to expand. We show that over finite expanding domains (with an arbitrary, tree-like, quasi-order, or linear transitive relation) the logics are recursively enumerable, but undecidable. If these finite domains eventually become constant then the resulting 0-free logics are decidable (but not in primitive recursive time); on the other hand, when equipped with O they are not even recursively enumerable. Finally, we show that temporal logics over infinite expanding domains as above are undecidable even for the language with the sole temporal operator 'eventually.' The proofs are based on Kruskal's tree theorem and reductions of reachability problems for lossy channel systems. <s> BIB005 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> Abstract We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding over time. (It is known that none of these logics is decidable when interpreted in structures where the second component does not change over time.) The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable (in non-primitive recursive time) if the number of function iterations is assumed to be finite. <s> BIB006 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of 'weak' description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable. <s> BIB007 </s> Temporal Description Logics: A Survey <s> Varying the DL Component <s> We combine the modal logic S5 with the description logic (DL) ALCQI. The resulting multi-dimensional DL S5ALCQI supports reasoning about change by allowing to express that concepts and roles change over time. It cannot, however, discriminate between changes in the past and in the future. Our main technical result is that satisfiability of S5ALCQI concepts with respect to general TBoxes (including GCIs) is decidable and 2-EXPTIME-complete. In contrast, reasoning in temporal DLs that are able to discriminate between past and future is inherently undecidable. We argue that our logic is sufficient for reasoning about temporal conceptual models with time-stamping constraints. <s> BIB008
Theorem 2 is rather robust under extensions of the DL component ALC. For example, if L is a DL between ALC and SHIQ (for a definition see, e.g., BIB001 ) then LTL L concept satisfiability w.r.t. TBoxes and with expanding domains has the same complexity as satisfiability in L w.r.t. TBoxes, and the same holds for the case without TBoxes. Theorem 3 and the constant domain case is equally robust. In particular, concept satisfiability in LTL SHIQ w.r.t. TBoxes is EXPTIME-complete, both with expanding and constant domains. As a lower bound, Theorem 4 applies to any extension of ALC, and it is more interesting to look at DL components that are weaker than ALC. One such DL is EL, which is obtained from ALC by dropping negation (and thus also and ∀). In LTL EL , every concept is satisfiable w.r.t. every TBox. For this reason, it is more interesting to consider concept subsumption w.r.t. TBoxes: given a TBox T and a concept inclusion C D, decide whether C D follows from T . In pure EL, concept subsumption w.r.t. TBoxes is tractable  . However, it is shown in BIB007 that concept satisfiability in LTL ALC with TBoxes and rigid roles can be reduced to concept subsumption in LTL EL with TBoxes and rigid roles. Thus, Theorem 4 already applies to the case of LTL EL . Theorem 5 is less robust than Theorems 2 and 3. It can be shown by a straightforward extension of the proof in BIB004 that the result still holds for ALCI, the extension of ALC with inverse roles. We conjecture that it also holds for ALCQ, the extension of ALC with qualified number restrictions. However, concept satisfiability with rigid roles and without TBoxes becomes undecidable if only a single transitive rigid role r is added. Intuitively, the reason is that we can then enforce an infinite r-path also without a TBox. Undecidability is proved in BIB004 using a reduction of Post's Correspondence Problem. In particular, it follows that concept satisfiability in LTL SHIQ without TBoxes and with rigid roles is undecidable. The proof in BIB004 even applies to finite (but unbounded) flows of time. However, it then relies on constant domains: a straightforward combination of the arguments from BIB006 BIB005 and BIB004 shows that concept satisfiability in LTL ALC with rigid transitive roles in expanding domain models with finite flows of time is decidable, though not in time bounded by a primitive recursive function. In BIB008 , it has been proved that Theorem 6 holds for ALCQI in place of ALC. The only noteworthy properties of ALC used in the proof of Theorem 7 are that (i) any satisfiable Boolean combination of concept inclusions is satisfiable in a countably infinite model, and (ii) satisfiability of Boolean combinations of concept inclusions in ALC is in EXPSPACE (and indeed even in EXPTIME). Thus, Theorem 7 generalizes to any DL with these properties, such as SHIQ. In general, if ALC is replaced by a decidable fragment F of first-order logic without equality, and temporal operators are applied to closed formulas only (which is the case for the standard translation of temporal ALC TBoxes into first-order temporal logic), then the complexity of the resulting fragment of first-order temporal logic will have exactly the same complexity as F, if it is at least PSPACE-hard. Theorem 8 can also be generalized to standard DLs such as SHIQ. Notably, a temporal extension of the description logic DLR, which provides for n-ary relations, was considered in BIB003 . The generalization to fragments of firstorder temporal logics has been studied systematically, and the resulting fragments are known as monodic fragments BIB002 . In monodic fragments, temporal operators are applied to formulas with at most one free variable. Note that this is the case for the standard translation of temporal LTL ALC TBoxes into first-order temporal logic. The quasimodel technique has been refined to deal with a variety of monodic fragments BIB004 .