STATES Project

Partners:

CPN Group at DAIMI

The goal of the STATES project is to develop theory, techniques and tools for state space analysis of Coloured Petri Net models. Case studies on the practical use of the developed techniques and tools on industrial-size CPN models is also an important part of the project. The STATES project is sponsered by the Danish Natural Science Research Council (SNF).

The basic idea behind a state space is to construct a directed graph, which has a node for each reachable marking and arcs corresponding to occurring binding elements. State spaces are also called occurrence graphs or reachability graphs/trees. The first of these names reflects the fact that a state space contains all the possible occurrence sequences, while the two latter names reflect that the state space contains all reachable markings. From the state space it is possible to analyse and verify an abundance of properties of the system.

A typical state space has thousands of nodes and thousands of arcs. Therefore, state space methods are closely tied to supporting computer tools, and have to be constructed and analysed by means of a computer tool. For this purpose we have developed a state space tool, which is fully integrated in the Design/CPN tool.

One of the main drawbacks of state space methods is the so-called state explosion problem. For many systems, the state space becomes so large that it cannot be fully constructed. In practice, our present state space tool supports state spaces with up to half a million nodes and one million arcs.

One of the ways to be able to handle large state spaces is to use condensed storage of the multi-sets encountered during the state space construction. Our present representation is identical to the representation used in the CPN simulator. This is far from being optimal and we expect to be able to improve it with as much as a factor of one hundred.

Another way to alliviate state explosion is to use reduction techniques. Reduction methods typically avoids representing the entire state space of the system and/or represents the state space in a compact form. The reduction is done in such a way, that properties of the system can still be derived from the reduced state space. Some of these techniques take a modular approach, while others avoid construction of all the sequences in which concurrent binding elements can be interleaved. There are also techniques that exploit the inherent symmetries and equivalence found in many systems.

Project Group

Research manager:

Kurt Jensen, Prof., Dr. Scient., DAIMI
Phone: +45 8942 5612, E-mail: kjensen@daimi.au.dk

Other members of the project group:

Søren Christensen, Assoc. Prof., PhD, DAIMI (schristensen@daimi.au.dk)
Lars M. Kristensen, Assistant Prof., PhD, DAIMI (kris@daimi.au.dk)
Thomas Mailund, PhD student, DAIMI (mailund@daimi.au.dk)
Michael Westergaard, Student Programmer, DAIMI (mw@daimi.au.dk)

Publications from Project

• Christensen, S., Kristensen, L.M.: State Space Analysis of Hierarchical Coloured Petri Nets. In: B. Farwer, D. Moldt and M-O. Stehr (Eds): Petri Nets in System Engineering (PNSE'97) Modelling, Verification, and Validation, Hamburg, Germany, Plublication No. 205, Universität Hamburg, Fachberich Informatik, pp. 32-43, 1997.
• Jørgensen, J.B.: Analysing Coloured Petri Nets by the Occurrence Graph Method. Summary of Ph.D., DAIMI PB-517, 1997.
• Cheng, A., Christensen, S., Mortensen, K.H.: Model Checking Coloured Petri Nets Exploiting Strongly Connected Components. In M.P. Spathopoulos, R. Smedinga, and P. Kozak (Eds). Proceedings of the International Workshop on Discrete Event Systems, WODES96. Institution of Electrical Engineers, computing and control division, August 1996. Edinburgh, Scotland, UK, pp 169-177, 1996.

• Gallasch, G.E., Kristensen, L.M., Mailund, T.: Sweep-Line State Space Exploration for Coloured Petri Nets. In Proceedings of Fourth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2002). DAIMI PB-560 pp. 101-119, Aarhus, Denmark, 2002.
• Christensen, S., Jørgensen, J.B., Kristensen, L.M.: Design/CPN - A Computer Tool for Coloured Petri Nets. In: E. Brinksma (Ed.): Tools and Algorithms for the Construction and Analysis of Systems, TACAS'97, Lecture Notes in Computer Science, vol. 1217, Springer-Verlag, 209-223, 1997.
• Christensen, S., Jensen, K., Kristensen, L.M.: Design/CPN Occurrence Graph Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.au.dk/designCPN/, 1996.
• Jørgensen, J.B., Kristensen, L.M.: Design/CPN OE/OS Graph Manual. Computer Science Department, University of Aarhus, Denmark. On-line version: http://www.daimi.au.dk/ designCPN/, 1996.

• Kristensen, L.M., Mailund, T.: A Compositional Sweep-Line State Space Exploration Method. In Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 2002), LNCS 2529 pp. 327-343, Springer-Verlag.
• Kristensen, L.M., Mailund, T.: A Generalised Sweep-Line Method for Safety Properties. In Proceedings of Formal Methods Europe (FME 2002), pages 549-567, LNCS 2391, Springer-Verlag.
• Mailund, T.: Analysing Infinite-State Systems by Combining Equivalence Reduction and the Sweep-Line Method. Proceedings of International Conference on Application and Theory of Petri Nets (ICATPN 2002), pages 314-333, LNCS 2360, Springer-Verlag.
• Christensen, S., Jensen, K., Mailund, T., Kristensen, L.M.: State Space Methods for Timed Coloured Petri Nets. Proceedings of 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems. Berlin Germany, September 14-15, 2001.
• Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: T. Margaria and W. Yi (Eds.) Proceedings of TACAS 2001, Lecture Notes in Computer Science 2031, Springer-Verlag, pp. 450-464, 2001.
• Christensen, S., Kristensen, L.M., Mailund, T.: Condensed State Spaces for Timed Petri Nets. In J.-M. Colom and M. Koutny (Eds.) Proceedings of Application and Theory of Petri Nets 2001, Lecture Notes in Computer Science 2075, Springer-Verlag, pp. 101-120, 2001.
• Kristensen, L.M., Valmari, A.: Improved Question-Guided Stubborn Set Methods for State Properties. In: M. Nielsen and D. Simpson (Eds.) Proceedings of the 21st International Conference on Application and Theory of Petri Nets, Aarhus, Denmark, Lecture Notes in Computer Science 1825, Springer-Verlag, pp. 382-302, 2000.
• Christensen, S., Petrucci, L.: Modular Analysis of Petri Nets. The Computer Journal, 43(3), pp. 224-242, 2000.
• Kristensen, L.M., Valmari A.: Finding Stubborn Sets of Coloured Petri Nets without Unfolding. In: J. Desel and and M. Silva (Eds): Proceeding of International Conference on Application and Theory of Petri Nets ICAPTPN98. Springer-Verlag. Lecture Notes in Computer Science volume 1420, pp. 104-123, 1998.
• Jørgensen, J.B, Kristensen, L.M.: Verification of Coloured Petri Nets Using State Space with Equivalence Classes In: B. Farwer, D. Moldt and M-O. Stehr (Eds): Petri Nets in System Engineering (PNSE'97) Modelling, Verification, and Validation, Hamburg, Germany, Plublication No. 205, Universität Hamburg, Fachberich Informatik, pp. 20-31, 1997.
• Jørgensen, J.B.: Construction of Occurrence Graphs with Permutation Symmetries Aided by the Backtrack Metod. DAIMI PB-516, 1997.
• Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9, Kluwer Academic Publishers, pp. 7-14, 1996.
• Christensen, S., Petrucci, L.: Modular State Space Analysis of Coloured Petri Nets. In G. de. Michelis and M. Diaz (Eds.): Application and Theory of Petri Nets 1995. Proceedings of the 16th International Conference, Turin, Italy, Lecture Notes in Computer Science 935, Springer-Verlag, pp. 201-217, 1995.
• Christensen, S., Petrucci, L.: Towards a Modular Analysis of Coloured Petri Nets. In K. Jensen (Ed.): Application and Theory of Petri Nets 1992. Proceedings of the 13th International Conference, Sheffield, UK, Lecture Notes in Computer Science 616, Springer-Verlag, pp. 113-133, 1992.

• Lorentsen, L., Kristensen, L.M.: Modelling and Analysis of a DANFOSS Flowmeter System Using Coloured Petri Nets. In: M. Nielsen and D. Simpson (Eds.) Proceedings of the 21st International Conference on Application and Theory of Petri Nets, Aarhus, Denmark, Lecture Notes in Computer Science 1825, Springer-Verlag, pp. 346-366, 2000.
• Christensen, S., Jørgensen, J.B.: Analysis of Bang & Olufsen's BeoLink® Audio/Video System Using Coloured Petri Nets. In: P. Azéma and G. Balbo (Eds.) Application and Theory of Petri Nets 1997. Proceedings of the 18th International Conference, Toulouse, France, Lecture Notes in Computer Science 1248, Springer-Verlag, pp. 387-406, 1997.
• Jørgensen, J.B., Mortensen, K.H.: Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets. In J. Billington and W. Reisig (eds.): Application and Theory of Petri Nets 1996. Proceedings of the 17th International Petri Net Conference, Osaka 1996, Lecture Notes in Computer Science Vol. 1091, Springer-Verlag, pp. 249-268, 1996.
• Jørgensen, J.B., Kristensen, L.M.: Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm Using Coloured Petri Nets and Occurrence Graphs with Symmetries. IEEE Transactions on Parallel and Distributed Systems, Volume 10, Number 7, July 1999.