Decidable and undecidable fragments of first-order branching temporal logics

Abstract In this paper we analyze the decision problem for fragments of first-order extensions ofbranching time temporal logics such as computational tree logics CTL and CTL \Lambda or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragmentsof logics like first-order C T L \Lambda--such as the product of propositional C T L\Lambda with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with soletemporal 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 \Lambda, 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 devis-ing expressive and effective time-dependent knowledge representation formalisms, e.g., tempora