Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2007: Formal Methods and Software Engineering pp 246–265Cite as

Model Checking Propositional Projection Temporal Logic Based on SPIN

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4789))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kripke, S.A.: Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math. 9, 67–96 (1963)

    Article  MATH  MathSciNet  Google Scholar 

  2. Rosner, R., Pnueli, A.: A choppy logic. In: LICS, pp. 306–314. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  3. Moszkowski, B.: Reasoning about digital circuits. Ph.D Thesis, Department of Computer Science, Stanford University. TRSTAN-CS-83-970 (1983)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of duration. Information Processing Letters 40(5), 269–275 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  6. Duan, Z.: An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle Upon Tyne (May 1996)

    Google Scholar 

  7. Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, China (2006)

    Google Scholar 

  8. 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

  9. 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)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, Heidelberg (1992)

    Google Scholar 

  12. Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages and Computation, 2nd edn. Addison-Wesley, Reading (2001)

    MATH  Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  16. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  17. 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)

    Google Scholar 

  18. Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  19. 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)

    Google Scholar 

  20. Wolper, P.L.: Temporal logic can be more expressive. Information and Control 56, 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computing Theory and Technology, Xidian University, Xi’an, 710071, P.R. China

    Cong Tian & Zhenhua Duan

Authors
  1. Cong Tian
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenhua Duan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Butler Michael G. Hinchey María M. Larrondo-Petrie

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation