Advertisement

Stubborn Sets for Standard Properties

  • Karsteb Schmidt
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

(Theory) Analysis of nets Computer tools for nets 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 8.
    P. Starke. Private communication, 1998.Google Scholar
  9. 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. 10.
    A. Valmari. Stubborn sets for reduced state space generation. Advances in Petri Nets 1990, LNCS 483, pages 491–511, 1991.Google Scholar
  11. 11.
    A. Valmari. A stubborn attack on state explosion. Formal methods in System Design 1, pages 297–322, 1992.Google Scholar
  12. 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. 13.
    A. Valmari. State of the art report: stubborn sets. Petri Net Newsletter 46, pages 6–14, 1994.Google Scholar
  14. 14.
    A. Valmari. Stubborn set methods for process algebras. Workshop on Partial order Methods in Verification, Princeton, pages 192–210, 1996.Google Scholar
  15. 15.
    A. Valmari. The state explosion problem. Lectures on Petri Nets I: Basic Models, LNCS 1491, pages 429–528, 1998.Google Scholar
  16. 16.
    K. Varpaaniemi. Private communication, 1993.Google Scholar
  17. 17.
    K. Varpaaniemi. On the stubborn set method in reduced state space generation. PhD thesis, Helsinki Uneversity of Technology, 1998.Google Scholar
  18. 18.
    K. Varpaaniemi. Private Communication, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Karsteb Schmidt
    • 1
  1. 1.Institut für InformatikHumboldt-Universität zu BerlinBerlinGermany

Personalised recommendations