On Non-Local Propositional and Local One-Variable Quantified CTL* Sebastian Bauer, Ian M. Hodkinson, Frank Wolter, and Michael Zakharyaschev   View Paper (PDF)   Return to Temporal Logic in Computer Science 1 Abstract 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. DiSC'03 © 2003 Association for Computing Machinery