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.
Similar content being viewed by others
References
G. Chiola, C. Dutheillet, G. Franceschinis, and S. haddad,On Well-Formed Coloured Nets and Their Symbolic Reachability Graph. In [14], pp. 373–396.
G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad,A Symbolic Reachability Graph for Coloured Petri Nets. To appear in Theoretical Computer Science, 1997.
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.
Design/CPN. Reference Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.aau.dk/designCPN/.
Design/CPN Occurrence Graph Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.aau.dk/designCPN/.
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.
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.
H.J. Genrich and K. Lautenbach, “System modelling with highlevel petri nets,”Theoretical Computer Science, Vol. 13, pp. 109–136, North Holland, 1981.
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.
K. Jensen, “Coloured Petri Nets and the invariant method,”Theoretical Computer Science, Vol. 14, pp. 317–336, North-Holland, 1981.
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.
K. Jensen,Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, Vol. 1, Basic Concepts. Monographs in Theoretical Computer Science, Springer-Verlag, 1992.
K. Jensen,Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical use, Vol. 2. Analysis Methods, Monographs in Theoretical Computer Science, Springer-Verlag, 1994.
K. Jensen and G. Rozenberg (Eds.)High-level Petri Nets. Theory and Application. Springer-Verlag, 1991.
R.M. Karp and R.E. Miller, “Parallel program schemata,”Journal of Computer and System Sciences, Vol. 3, pp. 147–195, 1969.
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.
R. Milner, R. Harper, and M. Tofte,The Definition of Standard ML, MIT Press, 1990.
R. Milner and M. Tofte,Commentary on Standard ML. MIT Press, 1991.
L. Paulson,ML for the Working Programmer. Cambridge University Press, 1991.
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.
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.
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.
Author information
Authors and Affiliations
Rights 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
Issue Date:
DOI: https://doi.org/10.1007/BF00625967