Temporal logic with forgettable past
Proceedings - Symposium on Logic in Computer Science - Trang 383-392
Tóm tắt
We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL+Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.
Từ khóa
#Automatic logic units #Computer science #PolynomialsTài liệu tham khảo
10.1016/0304-3975(84)90049-5
lichtenstein, 1985, The glory of the past, Lecture Notes in Computer Science, 193, 196, 10.1007/3-540-15648-8_16
10.1007/978-1-4612-0931-7
10.1016/0304-3975(95)00035-U
10.1006/inco.1999.2817
kupferman, 2001, Extended temporal logic revisited, Lecture Notes in Computer Science, 2154, 519, 10.1007/3-540-44685-0_35
kupferman, 1995, Once and for all, Proc 10th IEEE Symp Logic in Computer Science (LICS'95) San Diego CA USA June 1995, 25
kamp, 1968, Tense logic and the theory of linear order
kesten, 1993, A decision algorithm for full propositional temporal logic, Lecture Notes in Computer Science, 697, 97, 10.1007/3-540-56922-7_9
10.1145/3828.3837
rosner, 1986, A choppy logic, Proc 1st IEEE Symp Logic in Computer Science (LICS'86), 306
10.1016/0304-3975(87)90008-9
vardi, 1986, An automata-theoretic approach to automatic program verification, Proc 1st IEEE Symp Logic in Computer Science (LICS'86), 332
10.1145/73560.73582
vardi, 1995, Alternating automata and program verification, Lecture Notes in Computer Science, 1000, 471, 10.1007/BFb0015261
vardi, 1998, Reasoning about the past with two-way automata, Lecture Notes in Computer Science, 1443, 628, 10.1007/BFb0055090
wilke, 1999, Classifying discrete temporal properties, Lecture Notes in Computer Science, 1563, 32, 10.1007/3-540-49116-3_3
10.1006/inco.2001.3094
clarke, 1999, Model checking
10.1016/0304-3975(85)90225-7
10.1007/978-3-662-04558-9
10.1145/567446.567462
gabbay, 1989, The declarative past and imperative future: Executable temporal logic for interactive systems, Lecture Notes in Computer Science, 398, 409, 10.1007/3-540-51803-7_36
10.1109/LICS.1997.614950
10.1016/B978-0-444-88074-1.50021-4
harel, 1992, Algorithmics The Spirit of Computing
hafer, 1987, Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, Lecture Notes in Computer Science, 267, 269, 10.1007/3-540-18088-5_22