Decidable and undecidable fragments of first-order branching temporal logics
Proceedings - Symposium on Logic in Computer Science - Trang 393-402
Tóm tắt
In this paper we analyze the decision problem for fragments of first-order extensions of branching time temporal logics such as computational tree logics CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragments of logics like first-order CTL*-such as the product of propositional CTL* with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with sole temporal operator 'some time in the future'-are undecidable. On the other hand, it is proved that by restricting applications of first-order quantifiers to state (i.e., path-independent) formulas, and applications of temporal operators and path quantifiers to formulas with at most one free variable, we can obtain decidable fragments. The positive decidability results can serve as a unifying framework for devising expressive and effective time-dependent knowledge representation formalisms, e.g., temporal description or spatio-temporal logics.
Từ khóa
#Logic #Computer science #Educational institutions #Knowledge representation #Application software #Turning #HistoryTài liệu tham khảo
hodkinson, 2001, Monodic fragments of first-order temporal logics: 2000-2001 A.D., LNAI, 2250, 1
10.2178/jsl/1190150040
10.1016/S0168-0072(00)00018-X
10.1016/0022-0000(89)90039-1
hirsch, 2001, Representability is not decidable for finite relation algebras, Trans Amer Math Soc, 353, 1403, 10.1090/S0002-9947-99-02264-3
10.1007/3-540-52513-0_17
10.2307/2274321
gabbay, 2002, Many-Dimensional Modal Logics: Theory and Applications, Studies in Logic, 10.1023/A:1021304426509
gabbay, 2000, Temporal Logic Mathematical Foundations and Computational Aspects, 2
maddux, 1980, The equational theory of C A3 is undecidable, J Symbolic Logic, 45, 311, 10.2307/2273191
10.1016/B978-0-934613-04-0.50016-8
10.1007/3-540-61313-7_89
10.1093/acprof:oso/9780198243113.001.0001
prior, 1968, Nous, 2, 101, 10.2307/2214699
�hrstr�m, 1996, Temporal Logic: From Ancient Ideas to Artificial Intelligence, Studies in Logic and Philosophy, 57
10.2307/1995086
10.1023/A:1004359325754
wooldridge, 1992, A first-order branching time logic of multi-agent systems, Proceedings of the 11th European Conference on Artificial Intelligence, 234
10.2307/2695115
10.1090/memo/0066
10.1109/TIME.2002.1027466
10.1145/4904.4999
10.1023/A:1004275029985
10.1016/S0168-0072(01)00124-5
chagrov, 1997, Modal Logic
10.2307/2273296
10.2307/2275595
10.1111/j.1755-2567.1978.tb00175.x
wolter, 2002, Qualitative spatio-temporal representation and reasoning: A computational perspective, Exploring Artificial Intelligence in the New Millenium
10.1007/978-3-642-59207-2
10.1016/B978-0-444-88074-1.50021-4
clarke, 1981, Synthesis of synchronization skeletons for branching time temporal logic, Proc IBM Workshop Logics of Programs, 52