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.

Authors

• Sebastian Bauer 0004
• Ian M. Hodkinson
• Frank Wolter
• Michael Zakharyaschev

Keywords

• Logic
• Educational institutions
• Computer science
• Embedded computing
• Instruments
• Spatiotemporal phenomena
• Calculus
• Temporal Operators
• Set Of Equations
• Tree Model
• Paper Surveys
• Equivalence Relation
• Free Variables
• First-order Structure
• Set Of Branches
• Pair Connections