Abstract
This paper investigates a model checking algorithm for Propositional Projection Temporal Logic (PPTL) with finite models. To this end, a PPTL formula is transformed to a Normal Form Graph (NFG), and then a Nondeterministic Finite Automaton (NFA). The NFA precisely characterizes the finite models satisfying the corresponding formula and can be equivalently represented as a Deterministic Finite Automaton (DFA). When the system to be verified can be modeled as a DFA A s , and the property of the system can be specified by a PPTL formula P, then ¬P can be transformed to a DFA A p . Thus, whether the system satisfies the property or not can be checked by computing the product automaton of A s and A p , and then checking whether or not the product automaton accepts the empty word. Further, this method can be implemented by means of the verification system Spin.
This research is supported by the NSFC Grant No. 60373103 and 60433010.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Kripke, S.A.: Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math. 9, 67–96 (1963)
Rosner, R., Pnueli, A.: A choppy logic. In: LICS, pp. 306–314. IEEE Computer Society Press, Los Alamitos (1986)
Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)
Moszkowski, B.: An Automata-Theoretic Completeness Proof for Interval Temporal Logic. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 223–234. Springer, Heidelberg (2000)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of duration. Information Processing Letters 40(5), 269–275 (1991)
Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle Upon Tyne (May 1996)
Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, China (2006)
Duan, Z., Zhang, L.: A Decision Procedure for Propositional Projection Temporal Logic. Technical Report No.1, Institute of computing Theory and Technology, Xidian University, Xi’an P.R.China (2005), http://www.paper.edu.cn/process/download.jsp?file=200611-427
Duan, Z., Tian, C.: Decidability of Propositional Projection Temporal Logic with Infinite Models. In: TAMC 2007. LNCS, vol. 4484, pp. 521–532. Springer, Heidelberg (2007)
Duan, Z., Yang, X., Koutny, M.: Semantics of Framed Temporal Logic Programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 256–270. Springer, Heidelberg (2005)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, Heidelberg (1992)
Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages and Computation, 2nd edn. Addison-Wesley, Reading (2001)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332–344. IEEE CS Press, Los Alamitos (1986)
Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proc. 10th LICS, pp. 36–43. IEEE Computer Soc. Press, Los Alamitos (1995)
Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Lowe, G.: Breaking and fixing the Needham-Schroeder public key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Merz, S.: Model Checking: A Tutorial Overview. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 3–38. Springer, Heidelberg (2001)
Wolper, P.L.: Temporal logic can be more expressive. Information and Control 56, 72–99 (1983)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tian, C., Duan, Z. (2007). Model Checking Propositional Projection Temporal Logic Based on SPIN. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds) Formal Methods and Software Engineering. ICFEM 2007. Lecture Notes in Computer Science, vol 4789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76650-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-76650-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76648-3
Online ISBN: 978-3-540-76650-6
eBook Packages: Computer ScienceComputer Science (R0)