Temporal Description Logics: A Survey <s> TBoxes is undecidable. <s> In this paper we analyze the decision problem for fragments of first-order extensions of branching time temporal logics such as computational tree logics CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragments of logics like first-order CTL*-such as the product of propositional CTL* with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with sole temporal operator 'some time in the future'-are undecidable. On the other hand, it is proved that by restricting applications of first-order quantifiers to state (i.e., path-independent) formulas, and applications of temporal operators and path quantifiers to formulas with at most one free variable, we can obtain decidable fragments. The positive decidability results can serve as a unifying framework for devising expressive and effective time-dependent knowledge representation formalisms, e.g., temporal description or spatio-temporal logics. <s> BIB001 </s> Temporal Description Logics: A Survey <s> TBoxes is undecidable. <s> In this paper we prove decidability of two kinds of branching time temporal logics. First we show that the non-local version of propositional PCTL*, in which truth values of atoms may depend on the branch of evaluation, is decidable. Then we use this result to establish decidability of various fragments of quantified PCTL*, where the next-time operator can be applied only to formulas with at most one free variable, all other temporal operators and path quantifiers are applicable only to sentences, and the first-order constructs follow the pattern of any of several decidable fragments of first-order logic. <s> BIB002
The original proof in BIB001 was given for one-variable firstorder CTL * with only one temporal operator ♦. It is not hard to see, however, that quantification over a single variable can be simulated by means of concept inclusions of the form C and the Boolean operators on CIs, which are available even in CTL * DL-Lite bool (which is, therefore, also undecidable). Positive decidability results can be obtained by restricting the application of temporal operators and path quantifiers in various ways BIB002 . An example is the replacement of CTL * with CTL as the temporal component. Theorem 14 ([32, 12] 