Temporal Description Logics: A Survey <s> E(EU candidate A¬♦EU member). <s> The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics. <s> BIB001 </s> Temporal Description Logics: A Survey <s> E(EU candidate A¬♦EU member). <s> 1. The handling of time: introduction and survey 2. Semantical presentation of temporal connectives 3. Axiomatic presentation of propositional temporal connectives 4. Predicate temporal logics 5. Temporal logics presented in the predicate calculus: language-metalanguage 6. A general theory of axiomatization for propositional temporal logic 7. Basic many-dimensional systems 8. Propositional quantifiers and fixed point operators 9. Expressive power of one-dimensional temporal connectives: basic concepts 10. Expressive completeness of Since and Until over integer and real time 11. Expressive completeness of Stavi connectives over general linear time 12. Further expressive completeness results 13. H-dimension 14. Adding a temporal dimension to a logic system 15. Decidability in temporal logic Bibliography Notation Index Index of Systems Index <s> BIB002 </s> Temporal Description Logics: A Survey <s> E(EU candidate A¬♦EU member). <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> BIB003 </s> Temporal Description Logics: A Survey <s> E(EU candidate A¬♦EU member). <s> We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties. <s> BIB004
A natural branching model of time consists of infinite trees where the root represents the current moment of time (or genesis) and the branches starting from the root represent possible histories. There are several temporal logics for branching time; see, e.g., BIB002 . Here we only consider computational tree logic CTL * BIB001 and its fragment CTL BIB004 . The language of CTL * is the straightforward extension of the language of LTL with the path (or history) quantifiers E and A. In CTL, the path quantifiers and temporal operators may occur only in the form E(CUD), A (C D), etc. (so A(C D) is not a well-formed CTL formula). A branching time interpretation I = (T I , Δ I , · I ) consists of an ω-tree tree T I = (W, <), a nonempty domain Δ I , and a function · I that maps every A ∈ N C to some A I ⊆ W × Δ I and every r ∈ N R to r I ⊆ W × Δ I × Δ I . The elements on each full branch h of T I are ordered by <, and each such branch j is required to be order-isomorphic to ( , <). Intuitively, branches h represent possible histories, and their elements represent time points in these histories. Thus, the usual temporal operators can be applied to a given history, while E and A quantify over the set of all histories that include the current time point. This means that the interpretation of a complex concept depends not only on the time point w, but also on the history h that this time point belongs to, e.g., • (w, h, d) ∈ A I iff (w, d) ∈ A I , for a concept name A, • (w, h, d) ∈ (♦C) I iff there exists w ∈ h such that w < w and (w , h, d) ∈ C I , • (w, h, d) ∈ (EC) I iff there exists a full branch h in T such that w ∈ h and (w, h , d) ∈ C I . We consider temporal CTL * ALC and CTL ALC TBoxes and KBs. Thus, we allow the application of temporal operators and (in the case of CTL * ) path quantifiers to concepts, concept inclusions, and ABox assertions (in the case of KBs), but not to roles. Both problems are defined by extending the definitions for LTL ALC in a straightforward way. In particular, the truth-relation (I, w, h) |= ϕ for temporal CTL * ALC KBs ϕ is defined by combining the inductive definitions above with those for ALC. The addition of branching to temporal interpretations changes the computational properties of TDLs in a drastic way. We remind the reader that CTL * and CTL are 2EXPTIME-and EXPTIME-complete, respectively. The problem with TDLs based on CTL * and CTL is that, intuitively, they are '2 . This is not a good sign as we know from BIB003 that almost all 3D products of modal-like logics are undecidable.