SpringerLink
Log in

Improved Net Reductions for LTL\(\setminus \)X Model Checking

  • Conference paper
  • First Online:
Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2013)

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

  • 757 Accesses

Abstract

A set of reduction rules for LTL\(\setminus \)X model checking of 1-safe Petri nets are presented in this paper. Compared with the rules available, more original transitions and places could be removed from the synchronization of Büchi automata obtained from LTL\(\setminus \)X formulae and 1-safe Petri nets with the new proposed rules. As a result, a compact synchronization is generated. This is useful in improving efficiency of LTL\(\setminus \)X model checking of 1-safe Petri nets.

This research is supported by the NSFC Grant Nos. 61133001, 61272118, 61272117, 61202038, 91218301, 61322202, 61373043, and National Program on Key Basic Research Project (973 Program) Grant No. 2010CB328102.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Desel, J.: Reduction and design of well-behaved concurrent systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 166–181. Springer, Heidelberg (1990)

    Google Scholar 

  2. Esparza, J.: Reduction and synthesis of live and bounded free choice petri nets. Inf. Comput. 114(1), 50–87 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Esparza, J., Heljanko, K.: A new unfolding approach to LTL model checking. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 475–486. Springer, Heidelberg (2000)

    Google Scholar 

  4. Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37–56. Springer, Heidelberg (2001)

    Google Scholar 

  5. Esparza, J., Kanade, P., Schwoon, S.: A negative result on depth-first net unfoldings. Softw. Tools Technol. Transfer 10(2), 161–166 (2008)

    Article  Google Scholar 

  6. Esparza, J., Römer, S., Vogler, W.: An improvement of Mcmillan’s unfolding algorithm. Formal Methods Syst. Des. 20(3), 285–310 (2002)

    Article  MATH  Google Scholar 

  7. Esparza, J., Schröter, C.: Net reductions for LTL model-checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 310–324. Springer, Heidelberg (2001)

    Google Scholar 

  8. Esparza, J., Schröter, C.: Unfolding based algorithms for the reachability problem. Fundamenta Informaticae 47(3), 231–245 (2001)

    MATH  MathSciNet  Google Scholar 

  9. Gastin, P., Oddoux, D.: Fast LTL to büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)

    Google Scholar 

  10. Haddad, S., Pradat-Peyre, J.F.: New efficient petri nets reductions for parallel programs verification. Parallel Process. Lett. 16(1), 101–116 (2006)

    Article  MathSciNet  Google Scholar 

  11. Heljanko, K.: Deadlock and reachability checking with finite complete prefixes. Research Report A56, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo (1999)

    Google Scholar 

  12. Hyung, L., Favrel, J., Baptiste, P.: Generalized petri net reduction method. IEEE Trans. Syst. Man Cybern. SMC 17(2), 297–303 (1987)

    Article  MATH  Google Scholar 

  13. Katoen, J.P.: Concepts, Algorithms, and Tools for Model Checking. IMMD, Erlangen (1999)

    Google Scholar 

  14. Khomenko, V., Koutny, M.: Verification of bounded petri nets using integer programming. Formal Methods Syst. Des. 30(2), 143–176 (2007)

    Article  MATH  Google Scholar 

  15. McMillan, K.L.: Symbolic Model Checking. Springer, New York (1993)

    Book  MATH  Google Scholar 

  16. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)

    Google Scholar 

  17. Melzer, S., Römer, S.: Deadlock checking using net unfoldings. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 352–363. Springer, Heidelberg (1997)

    Google Scholar 

  18. Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 510–584. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  19. Wallner, F.: Model checking LTL using net unforldings. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 207–218. Springer, Heidelberg (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ICTT and ISN Lab, **dian University, **’an, 710071, China

    Ya Shi, Zhenhua Duan & Cong Tian

  2. Bei**g Institute of Control Engineering, Bei**g, 100000, China

    Hua Yang

Authors
  1. Ya Shi
    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

  3. Cong Tian
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hua Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhenhua Duan .

Editor information

Editors and Affiliations

  1. Hosei University, Koganei-shi, Tokyo, Japan

    Shaoying Liu

  2. Technology, **dian University, **’an, China

    Zhenhua Duan

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Shi, Y., Duan, Z., Tian, C., Yang, H. (2014). Improved Net Reductions for LTL\(\setminus \)X Model Checking. In: Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2013. Lecture Notes in Computer Science(), vol 8332. Springer, Cham. https://doi.org/10.1007/978-3-319-04915-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-04915-1_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-04914-4

  • Online ISBN: 978-3-319-04915-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation