On non-local propositional and local one-variable quantified CTL*
Tóm tắt
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.
Từ khóa
#Logic #Educational institutions #Computer science #Embedded computing #Instruments #Spatiotemporal phenomena #CalculusTài liệu tham khảo
10.1016/S0168-0072(00)00018-X
10.1145/4904.4999
10.1007/BF00649485
10.1109/LICS.2002.1029847
10.1007/3-540-45653-8_1
10.2307/1995086
10.1007/3-540-57785-8_130
10.1145/800076.802493
wolter, 2002, Qualitative spatio-temporal representation and reasoning: a computational perspective, Exploring Artificial Intelligence in the New Millenium
10.2307/2273296