Temporal Description Logics: A Survey <s> Theorem 8 ([46, 24]). Satisfiability of temporal LTL ALC <s> We show how to combine the standard tableau system for the basic description logic ALC and Wolper's tableau calculus for propositional temporal logic PTL (with the temporal operators 'next-time' and 'until') in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic PTLALC of [20] interpreted in models with constant domains. We use the method of quasimodels [18,16] to represent models with infinite domains, and the technique of minimal types [11] to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics. <s> BIB001 </s> Temporal Description Logics: A Survey <s> Theorem 8 ([46, 24]). Satisfiability of temporal LTL ALC <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> BIB002
TBoxes is EXPSPACE-complete. We confine ourselves to a sketch of the upper bound. The crucial observation in most proofs of the PSPACE upper bound for satisfiability in LTL is that every satisfiable LTLformula is satisfied in a model of the form where the M(i) are propositional valuations and m is at most exponential in the length of ϕ. When considering temporal interpretations I satisfying a temporal LTL ALC TBox ϕ, such regular models need not exist. For example, the TBox is not satisfied in any regular model simply because all interpretations I(n) have to be distinct. The fundamental idea for proving an EXPSPACE upper bound is that, by abstracting from the domains of interpretations I(n) using so-called quasimodels, one can regain a semantics in which regular models always exist. Quasimodels are abstractions of temporal interpretations I = I(0), I(1), . . . in which the non-temporal interpretations I(i) are replaced by sets Ξ i of types, called quasistates. Types are defined in the same way as in Section 3.3, but based on the subconcepts of all concepts that occur in the temporal TBox ϕ for which satisfiability is to be checked. Using the observation that there exist 'only' double-exponentially many quasistates, we can apply regularity arguments as used in the LTL case to quasimodels. To satisfy a TBox ϕ, it suffices to considers regular quasimodels of the form where m is bounded double-exponentially in the length of ϕ. This explains the increase in complexity from PSPACE to EXPSPACE. Of course, a number of conditions have to be imposed on sequences Ξ 0 , Ξ 1 , . . . of quasistates so that they can serve as a quasimodel. We will not describe the conditions in detail here, but refer the reader to BIB002 . The conditions guarantee that one can re-construct a temporal interpretation from a quasimodel. For example, for each Ξ i , there has to exist an interpretation I i satisfying exactly the types in Ξ i (where concepts starting with a temporal operator are regarded as concept names). This condition ensures that the description logic part of a quasistate is satisfiable. For the temporal part, it is required that for each type t ∈ Ξ n , there exists a run r : → i≥0 Ξ i such that • CUD ∈ r(n) iff there exists m ≥ n with D ∈ r(m) and C ∈ r(k) for all n ≤ k < m. When constructing a temporal interpretation I from a quasimodel, the domain Δ I of I consists of all such runs. The condition that is the domain of a run reflects the fact that we are interested in satisfiability in models with constant domain. The proof can easily be adapted to expanding domains. In particular, the domains of runs are then upward-closed subsets of . This yields an EXPSPACE upper bound also for the case of expanding domains. Alternatively, this bound can be shown using the reduction to constant domains mentioned at the end of Section 3.3. Tableau-based algorithms for checking satisfiability of temporal LTL ALC TBoxes that combine a Wolper-style tableau algorithm for LTL  with a tableau algorithm for ALC have been developed in  (for expanding domains) and BIB001 (for constant domains). Both algorithms are based on quasimodels. An implementation for expanding domains is presented in  .