DocumentCode
2147547
Title
On non-local propositional and local one-variable quantified CTL*
Author
Bauer, Sebastian ; Hodkinson, Ian ; Wolter, Frank ; Zakharyaschev, Michael
Author_Institution
Inst. fur Informatik, Leipzig Univ., Germany
fYear
2002
fDate
2002
Firstpage
2
Lastpage
9
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.
Keywords
computability; decidability; process algebra; temporal logic; RCC-8; atom truth values; decidability; evaluation branch; first-order CTL*; local one-variable quantified CTL*; non local propositional CTL*; path quantifiers; sentences; spatio-temporal logics; temporal operators; tomorrow; weak fragment; Calculus; Computer science; Educational institutions; Embedded computing; Instruments; Logic; Spatiotemporal phenomena;
fLanguage
English
Publisher
ieee
Conference_Titel
Temporal Representation and Reasoning, 2002. TIME 2002. Proceedings.Ninth International Symposium on
ISSN
1530-1311
Print_ISBN
0-7695-1474-X
Type
conf
DOI
10.1109/TIME.2002.1027466
Filename
1027466
Link To Document