Abstract
We present an approach and associated computer tool support for conducting distributed state space exploration for Coloured Petri Nets (CPNs). The distributed state space exploration is based on the introduction of a coordinating process and a number of worker processes. The worker processes are responsible for the storage of states and the computation of successor states. The coordinator process is responsible for the distribution of states and termination detection. A main virtue of our approach is that it can be directly implemented in the existing single-threaded framework of Design/CPN and CPN Tools. This makes the distributed state space exploration and analysis largely transparent to the analyst. We illustrate the use of the developed tool on an example.
This work was started when both authors were at LSV, CNRS UMR 8643, ENS de Cachan, France.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barnat, J., Brim, L., Stříbrná, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 200. Springer, Heidelberg (2001)
Behrmann, G.: A Performance Study of Distributed Timed Automata Reachability Analysis. In: Brim, L., Grumberg, O. (eds.) Electronic Notes in Theoretical Computer Science, vol. 68. Elsevier, Amsterdam (2002)
Behrmann, G., Hune, T., Vaandrager, F.: Distributed Timed Model Checking - How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. In: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)
Brim, L., Grumberg, O. (eds.): Proc. of 1st Workshop on Parallel and Distributed Model Checking, October 2002. Electronic Notes in Theoretical Computer Science, vol. 68 (2002)
Brim, L., Grumberg, O. (eds.): Proc. of 2nd Workshop on Parallel and Distributed Model Checking, September 2003. Electronic Notes in Theoretical Computer Science, vol. 89 (2003)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
The CPN Tools Homepage, http://www.daimi.au.dk/CPNtools
The Design/CPN Homepage, http://www.daimi.au.dk/designCPN
Dijkstra, E.W.: Derivation of a Termination Detection Algorithm for Distributed Computations. Information Processing Letters 16, 217–219 (1983)
Farret, G., Carré, G.: Distributed Methods for Computation and Analysis of a Coloured Petri Net State Space. Master’s thesis, Department of Computer Science, University of Aarhus (August 2002)
Gallasch, G., Kristensen, L.M.: Comms/CPN: A Communication Infrastructure for External Communication with Design/CPN. In: Proc. of the 3rd Workshop on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2001), Department of Computer Science, pp. 79–93. University of Aarhus, Aarhus (2001); DAIMI PB-554, ISSN 0105-8517
Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 217–234. Springer, Heidelberg (2001)
Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. Basic Concepts, vol. 1. Springer, Heidelberg (1992)
Lerda, F., Sisto, R.: Distributed-Memory Model-Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)
Stern, U., Dill, D.L.: Parallelizing the Murφ Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kristensen, L.M., Petrucci, L. (2004). An Approach to Distributed State Space Exploration for Coloured Petri Nets. In: Cortadella, J., Reisig, W. (eds) Applications and Theory of Petri Nets 2004. ICATPN 2004. Lecture Notes in Computer Science, vol 3099. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27793-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-27793-4_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22236-1
Online ISBN: 978-3-540-27793-4
eBook Packages: Springer Book Archive