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 same arguments show decidability of
`non-local' propositional CTL*, in which truth values of
propositional atoms depend on the history as well as the current
time. 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.
