Skip to main content
SpringerLink
Log in

On the Step Explosion Problem

  • Conference paper
Petri Nets and Other Models of Concurrency - ICATPN 2006 (ICATPN 2006)

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

Included in the following conference series:

Abstract

In many well-known extensions of place-transition nets, including read arcs, inhibitory arcs, reset arcs, priorities and signal arcs, it is sometimes possible to reach a marking through firing a step of transitions which cannot be reached through firing a sequence of single transitions. For state space analysis, it is thus recommendable to consider, in each state, all steps of transitions for firing. Since the number of activated steps may be exponential in the number of transitions, we have, in addition to the well-known state explosion problem, another explosion which we call step explosion. In this paper, we present an approach for alleviating step explosion. We furthermore discuss the joint application of our method with partial order reduction and in the context of CTL model checking.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Clarke, E.M., Emerson, E.A.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computing 2, 241–266 (1982)

    MATH  Google Scholar 

  2. Godefroid, P.: Partial–Order Methods for the Verification of Concurrent Systems: An Approach to the State–Explosion Problem. PhD thesis, University of Liege, Computer Science Department (1994)

    Google Scholar 

  3. Huber, P., Jensen, A., Jepsen, L., Jensen, K.: Towards reachability trees for high–level Petri nets. In: Rozenberg, G. (ed.) APN 1984. LNCS, vol. 188, pp. 215–233. Springer, Heidelberg (1985)

    Google Scholar 

  4. Janicki, R., Koutny, M.: Invariant Semantics of Nets with Inhibitor Arcs. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 317–331. Springer, Heidelberg (1991)

    Google Scholar 

  5. Janicki, R., Koutny, M.: Invariants and Paradigms of Concurrency Theory. In: Aarts, E.H.L., van Leeuwen, J., Rem, M. (eds.) PARLE 1991. LNCS, vol. 506, pp. 59–74. Springer, Heidelberg (1991)

    Google Scholar 

  6. Janicki, R., Koutny, M.: Structure of Concurrency. Theoretical Computer Science 112, 5–52 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  7. Janicki, R., Koutny, M.: Semantics of Inhibitor Nets. Information and Computation 123, 1–16 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  8. Mailund, T.: Sweeping the State Space - a sweep-line state space exploration method. PhD thesis, University of Aarhus (2003)

    Google Scholar 

  9. Montanari, U., Rossi, F.: Contextual Nets. Acta Informatica 32(6), 545–596 (1995)

    MATH  MathSciNet  Google Scholar 

  10. Peled, D.: All from one, one for all: on model–checking using representitives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)

    Google Scholar 

  11. Rausch, M.: Modulare Modellbildung, Syntese und Codegenerierung ereignisdiskreter Steuerungssysteme. PhD thesis, Otto-von-Guerike Universität Magdeburg, Lehrstuhl Steuerungstechnik (1996)

    Google Scholar 

  12. Roch, S., Starke, P.H.: INA - Integrated Net Analyzer - Version 2.2 - Manual. Technical report, Informatik-Berichte, Humboldt-Universität zu Berlin (1998)

    Google Scholar 

  13. Roch, S., Starke, P.: The sesa home page (2002), http://www.informatik.hu-berlin.de/lehrstuehle/automaten/sesa/

  14. Schmidt, K.: How to calculate symmetries of Petri nets. Acta Informatica 36(7), 545–590 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  15. Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 192–204. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Starke, P.H., Roch, S.: Analysing Signal-Net Systems. Informatik-Berichte 162, Humboldt-Universität zu Berlin (2002)

    Google Scholar 

  17. Starke, P.: Reachability analysis of Petri nets using symmetries. J. Syst. Anal. Model. Simul. 8, 294–303 (1991)

    MathSciNet  Google Scholar 

  18. Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  19. Valmari, A.: Error detection by reduced reachability graph generation. In: Proceedings of the Ninth European Workshop on Application and Theory of Petri Nets, Venice, Italy, pp. 95–112 (1988)

    Google Scholar 

  20. Valmari, A.: Stubborn Sets for Reduced State Space Generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)

    Google Scholar 

  21. van Glabbeek, R.: Personal communication (2005)

    Google Scholar 

  22. Vogler, W.: Partial Order Semantics and Read Arcs. Technical Report 1997-1, Universität Augsburg (1997)

    Google Scholar 

  23. Vogler, W., Semenov, A., Yakovlev, A.: Unfolding and Finite Prefix for Nets with Read Arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, D-10099, Berlin, Germany

    Stephan Roch & Karsten Schmidt

Authors
  1. Stephan Roch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karsten Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, 10149, Torino, Italy

    Susanna Donatelli

  2. School of Computing, National University of Singapore,  

    P. S. Thiagarajan

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roch, S., Schmidt, K. (2006). On the Step Explosion Problem. In: Donatelli, S., Thiagarajan, P.S. (eds) Petri Nets and Other Models of Concurrency - ICATPN 2006. ICATPN 2006. Lecture Notes in Computer Science, vol 4024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11767589_19

Download citation

  • DOI: https://doi.org/10.1007/11767589_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-34699-9

  • Online ISBN: 978-3-540-34700-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation