×

zbMATH — the first resource for mathematics

A practical decision procedure for propositional projection temporal logic with infinite models. (English) Zbl 1358.68188
Summary: This paper presents a practical decision procedure for Propositional Projection Temporal Logic with infinite models. First, a set \(\mathrm{Prop}_l\) of labels \(l_i\), \(0 \leqslant i \leqslant n \in N_0\), is used to mark nodes of an LNFG of a formula, and a node with \(l_i\) is treated as an accepting state as in an automaton. Further, the generalized Büchi accepting condition for automata is employed to identify a path (resulting a word) in an LNFG as a model of the formula. In addition, the implementation details of the decision procedure and relevant algorithms including pre-processing, LNFG, circle finding algorithms are presented; as a matter of fact, all algorithms are implemented by C++ programs.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Duan, Z.; Tian, C.; Zhang, Li, A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78, (2008) · Zbl 1141.68039
[2] Z. Duan, C. Tian, An improved decision procedure for propositional projection temporal logic with infinite models, in: Proceedings of ICFEM 2010, LNCS, vol. 6447, pp. 90-105.
[3] Duan, Z., Temporal logic and temporal logic programming, (2006), Science Press Beijing
[4] Duan, Z.; Koutny, M.; Holt, C., Projection in temporal logic programming, (Pfenning, F., Proceedings of Logic Programming and Automatic Reasoning, Lecture Notes in Artificial Intelligence, vol. 822, (1994), Springer-Verlag), 333-344
[5] Moszkowski, B., Executing temporal logic programs, (1986), Cambridge University Press · Zbl 0658.68014
[6] Vardi, Moshe Y., The Büchi complementation saga, (STACS 2007, LNCS, vol. 4393, (2007)), 12-22 · Zbl 1186.03062
[7] Glynn Winskel, The Formal Semantics of Programming Languages, Foundations of Computing, The MIT Press, Cambridge, MA. · Zbl 0919.68082
[8] Duan, Z., An extended interval temporal logic and a framing technique for temporal logic programming, (1996), University of Newcastle upon Tyne, Ph.D. thesis
[9] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, (1977), IEEE New York), 46-57
[10] Tian, Cong; Duan, Zhenhua, Model checking propositional projection temporal logic based on SPIN, (ICFEM, LNCS, vol. 4789, (Nov 2007), Springer-Verlag), 246-265
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.