On non-local propositional and local one-variable quantified CTL*

We prove decidability of ´non local´ propositional CTL*, where truth values of atoms may depend on the branch of evaluation. This result is then used to show decidability of the ´weak´ one-variable fragment of first-order (local) CTL*, in which all temporal operators and path quantifiers except ´tomorrow´ are applicable only to sentences. Various spatio-temporal logics based on combinations of CTL* and RCC-8 can be embedded into this fragment, and so are decidable.