Skip to main content
SpringerLink
Log in
Book cover

International Computing and Combinatorics Conference

COCOON 2019: Computing and Combinatorics pp 503–515Cite as

An Efficient Decision Procedure for Propositional Projection Temporal Logic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11653))

Abstract

The decision problem for Propositional Projection Temporal Logic (PPTL) has been solved successfully, however time complexity of the procedure is increased exponentially to the length of the formula. To solve the problem, a Labeled Unified Complete Normal Form is introduced as an intermediate form to rewrite a PPTL formula into its equivalent Labeled Normal Form, based on which the Labeled Normal Form Graph is constructed and an efficient decision procedure for PPTL is formalized with the time complexity linear to the length of the formula and the size of the power set of the atomic propositions in the formula.

This research is supported by the Industrial Research Project of Shaanxi Province No. 2017GY-076, and NSFC Grant No. 61572386 and No. 61672403.

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 EPUB and 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

References

  1. Duan, Z.: An extended interval temporal logic and a framing technique for interval temporal logic programming. Ph.D. thesis, University of Newcastle Upon Tyne (1996)

    Google Scholar 

  2. Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19, 333–344 (2004)

    MathSciNet  Google Scholar 

  3. Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)

    Article  MathSciNet  Google Scholar 

  4. Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  5. Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167–186. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88194-0_12

    Chapter  Google Scholar 

  6. Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011)

    Article  MathSciNet  Google Scholar 

  7. Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: CSCWD, pp. 360–365 (2014)

    Google Scholar 

  8. Yu, Y., Duan, Z., Tian, C., Yang, M.: Model checking C programs with MSVL. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 87–103. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39277-1_7

    Chapter  Google Scholar 

  9. Ma, Q., Duan, Z., Zhang, N., Wang, X.: Verification of distributed systems with the axiomatic system of MSVL. Formal Asp. Comput. 27(1), 103–131 (2015)

    Article  MathSciNet  Google Scholar 

  10. Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  11. McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publisher, Dordrecht (1993)

    Book  Google Scholar 

  12. Duan, Z.: Temporal Logic and Temporal Logic Programming Language. Science Press, Beijing (2006)

    Google Scholar 

  13. Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inf. 45(1), 43–78 (2008)

    Article  MathSciNet  Google Scholar 

  14. Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169–190 (2014)

    Article  MathSciNet  Google Scholar 

  15. Shu, X., Duan, Z., Du, H.: A decision procedure and complete axiomatization for projection temporal logic Theor. Comput. Sci. (2017). https://doi.org/10.1016/j.tcs.2017.09.026

  16. Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of finite interval temporal logic with projection. J. Log. Comput. 13(2), 195–239 (2003)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Technology, Xi’an University of Posts and Communications, Xi’an, 710061, China

    Xinfeng Shu

  2. Institute of Computing Theory and Technology, Xidian University, Xi’an, 710071, China

    Nan Zhang

Authors
  1. Xinfeng Shu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nan Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xinfeng Shu .

Editor information

Editors and Affiliations

  1. The University of Texas at Dallas, Richardson, TX, USA

    Ding-Zhu Du

  2. Xidian University, Xi'an, China

    Zhenhua Duan

  3. Xidian University, Xi'an, China

    Cong Tian

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Shu, X., Zhang, N. (2019). An Efficient Decision Procedure for Propositional Projection Temporal Logic. In: Du, DZ., Duan, Z., Tian, C. (eds) Computing and Combinatorics. COCOON 2019. Lecture Notes in Computer Science(), vol 11653. Springer, Cham. https://doi.org/10.1007/978-3-030-26176-4_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-26176-4_42

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-26175-7

  • Online ISBN: 978-3-030-26176-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation