Nothing Special   »   [go: up one dir, main page]

Skip to main content
Log in

Condensed state spaces for symmetrical Coloured Petri Nets

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

This paper deals with state spaces. A state space is a directed graph with a node for each reachable state and an arc for each possible state change. We describe how symmetries of the modelled system can be exploited to obtain much more succinct state space analysis. The symmetries induce equivalence classes of states and equivalence classes of state changes. It is then possible to construct a condensed state space where each node represents an equivalence class of states while each arc represents an equivalence class of state changes. Such a condensed state space is often much smaller than the full state space and it is also much faster to construct. Nevertheless, it is possible to use the condensed state space to verify the same kind of behavioural properties as the full state space. hence, we do not lose analytic power.

We define state spaces and condensed state spaces for a language called Coloured Petri Nets (CP-nets). This language is in widespread use for the modelling and analysis of concurrent systems. However, our techniques are general and they can be used for many other kinds of labelled transition systems. The paper does not assume that the reader is familiar with CP-nets (or Petri nets in general)—although such knowledge will, of course, be a help. The first four sections of the paper introduce the basic concepts of CP-nets. The next three sections deal with state spaces, condensed state spaces and computer tools for state space analysis. Finally, there is a short conclusion.

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

Access this article

Subscribe and save

Springer+ Basic
$34.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

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. G. Chiola, C. Dutheillet, G. Franceschinis, and S. haddad,On Well-Formed Coloured Nets and Their Symbolic Reachability Graph. In [14], pp. 373–396.

  2. G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad,A Symbolic Reachability Graph for Coloured Petri Nets. To appear in Theoretical Computer Science, 1997.

  3. E.M. Clarke, T. Filkorn, and S. Jha, “Exploiting symmetry in temporal logic model checking,” inComputer Aided Verification. Proceedings of the 5th International Conference on Computer Aided Verification, C. Courcoubetis (Ed.), Elounda, Greece, 1993, Lecture Notes in Computer Science, Vol. 697, pp. 450–462, Springer-Verlag 1993.

  4. Design/CPN. Reference Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.aau.dk/designCPN/.

  5. Design/CPN Occurrence Graph Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.aau.dk/designCPN/.

  6. E.A. Emerson and A.P. Sistla, “Symmetry and model checking,” inComputer Aided Verification. Proceedings of the 5th International Conference on Computer Aided Verification, C. Courcoubetis (Ed.), Elounda, Greece, 1993, Lecture Notes in Computer Science, Vol. 697, pp. 463–477, Springer-Verlag, 1993.

  7. A. Finkel, “A minimal coverability graph for Petri nets,”Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, 1990, pp. 1–21.

  8. H.J. Genrich and K. Lautenbach, “System modelling with highlevel petri nets,”Theoretical Computer Science, Vol. 13, pp. 109–136, North Holland, 1981.

    Google Scholar 

  9. P. Huber, A.M. Jensen, L.O. Jepsen, and K. Jensen, “Reachability trees for high-level Petri nets,”Theoretical Computer Science, Vol. 45, pp. 261–292. Also in [14], pp. 319–350, North-Holland, 1986.

  10. K. Jensen, “Coloured Petri Nets and the invariant method,”Theoretical Computer Science, Vol. 14, pp. 317–336, North-Holland, 1981.

    Google Scholar 

  11. K. Jensen, “Coloured Petri Nets: A highlevel language for system design and analysis,” inAdvances in Petri Nets 1990, G. Rozenberg (Ed.), Lecture Notes in Computer Science Vol. 483, pp. 342–416, Springer-Verlag 1991, also in [14], 44–122.

  12. K. Jensen,Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, Vol. 1, Basic Concepts. Monographs in Theoretical Computer Science, Springer-Verlag, 1992.

  13. K. Jensen,Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical use, Vol. 2. Analysis Methods, Monographs in Theoretical Computer Science, Springer-Verlag, 1994.

  14. K. Jensen and G. Rozenberg (Eds.)High-level Petri Nets. Theory and Application. Springer-Verlag, 1991.

  15. R.M. Karp and R.E. Miller, “Parallel program schemata,”Journal of Computer and System Sciences, Vol. 3, pp. 147–195, 1969.

    Google Scholar 

  16. M. Lindqvist,Parameterized Reachability Trees for Predicate/Transition Nets. In G. Rozenberg (Ed.),Advances in Petri Nets 1993, Lecture Notes in Computer Science, Vol. 674, pp. 301–324, Springer-Verlag, 1993, also in [14], pp. 351–372.

  17. R. Milner, R. Harper, and M. Tofte,The Definition of Standard ML, MIT Press, 1990.

  18. R. Milner and M. Tofte,Commentary on Standard ML. MIT Press, 1991.

  19. L. Paulson,ML for the Working Programmer. Cambridge University Press, 1991.

  20. L.Petrucci,Combining Finkels and Jensens Reduction Techniques to Build Covering Trees for Coloured Nets. Petri Net Newsletter No. 36 (August 1990), Special Interest Group on Petri Nets and Related System Models, Gesellschaft für Informatik (GI), Germany, 1990, 32–36.

    Google Scholar 

  21. A. Valmari, “Stubborn sets for reduced state space generation,” in Advances in Petri Nets G. Rozenberg (Ed.) 1990, Lecture Notes in Computer Science Vol. 483, Springer-Verlag, 1991, 491–515.

  22. A. Valmari, “Stubborn sets of coloured Petri nets,”Proceedings of the 12th International Conference on Application and Theory of Petri Nets, Aarhus, 1991, 102–121.

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jensen, K. Condensed state spaces for symmetrical Coloured Petri Nets. Form Method Syst Des 9, 7–40 (1996). https://doi.org/10.1007/BF00625967

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00625967

Keywords

Navigation