Skip to main content

Stubborn Sets for Standard Properties

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1639))

Abstract

Stubborn sets aree a tool for state space reduction preserving certain system properties. We present stubborn set approaches for all popular Petri net standard properties. This extends the list of properties that can be analysed successfully (including boundedness, reversibility). For other properties, our approach can lead to larger reductions (reachability) than previous ones. Futhermore, shortest and cheapest witness paths for several properties are now preservered.

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

Buying options

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. A. Finkel. A minimal coverability graph for Petri nets. Proc. of the 11th Int. Conf. Application and Theory of Petri Nets, pages 1–21, 1990.

    Google Scholar 

  2. R.. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking. 3rd Israel Symp. on the Theory of Computing and Systems, IEE 1995, pages 130–140, 1995.

    Google Scholar 

  3. P. Godefroid and P. Wolper. A partial approach to model checking. 6th IEEE Symp. on Logic in Computer Science, Amsterdam, pages 406–415, 1991.

    Google Scholar 

  4. R. M. Karp and R. E. Miller. Parallel program schemata. Journ. Computer and System Sciences 4, pages 147–195, May 1969.

    Google Scholar 

  5. I. Kokkarinen, D. Peled, and A. Valmari. Relaxed visibility enhances partial order reduction. 9th Int. Conf. Computer Aided Verification, LNCS 1254, pages 328–339, 1997.

    Google Scholar 

  6. D. Peled. All from one, one for all: on model-checking using representatives. 5th Int. Conf. Computer Aided Verification, LNCS 697, pages 409–423, 1993.

    Google Scholar 

  7. S. Roch and P. Starcke. INA Integrierter Netz Analysator Version 2.1. Technical Report 12, Humboldt-Uneversität zu Berlin, 1998.

    Google Scholar 

  8. P. Starke. Private communication, 1998.

    Google Scholar 

  9. A. Valmari. Error detection by reduced reachability graph generation. 9th European Workshop on Application and Theory of Petri Nets, pages 95–112, 1988.

    Google Scholar 

  10. A. Valmari. Stubborn sets for reduced state space generation. Advances in Petri Nets 1990, LNCS 483, pages 491–511, 1991.

    Google Scholar 

  11. A. Valmari. A stubborn attack on state explosion. Formal methods in System Design 1, pages 297–322, 1992.

    Google Scholar 

  12. A. Valmari. On-the-fly verification with stubborn sets. 5th Int. Cinf. Computer Aided Verification, LNCS 697, pages 397–408, 1993.

    Google Scholar 

  13. A. Valmari. State of the art report: stubborn sets. Petri Net Newsletter 46, pages 6–14, 1994.

    Google Scholar 

  14. A. Valmari. Stubborn set methods for process algebras. Workshop on Partial order Methods in Verification, Princeton, pages 192–210, 1996.

    Google Scholar 

  15. A. Valmari. The state explosion problem. Lectures on Petri Nets I: Basic Models, LNCS 1491, pages 429–528, 1998.

    Google Scholar 

  16. K. Varpaaniemi. Private communication, 1993.

    Google Scholar 

  17. K. Varpaaniemi. On the stubborn set method in reduced state space generation. PhD thesis, Helsinki Uneversity of Technology, 1998.

    Google Scholar 

  18. K. Varpaaniemi. Private Communication, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmidt, K. (1999). Stubborn Sets for Standard Properties. In: Donatelli, S., Kleijn, J. (eds) Application and Theory of Petri Nets 1999. ICATPN 1999. Lecture Notes in Computer Science, vol 1639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48745-X_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-48745-X_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66132-0

  • Online ISBN: 978-3-540-48745-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics