S. [. Allmaier, D. Dalibor, and . Kreische, Parallel Graph Generation Algorithms for Shared and Distributed Memory Machines
DOI : 10.1016/S0927-5452(98)80074-9

M. [. Allmaier, G. Kowarschik, and . Horton, State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor, Proceedings of the Seventh International Workshop on Petri Nets and Performance Models, pp.112-121, 1997.
DOI : 10.1109/PNPM.1997.595542

[. Ansi, Small Computer System Interface-2. Standard X3.131-1994, 1994.

G. [. Caselli, F. Conte, M. Bonardi, and . Fontanesi, Experiences on SIMD massively parallel GSPN analysis, Computer Performance Evaluation: Modelling Techniques and Tools, pp.266-283, 1994.
DOI : 10.1007/3-540-58021-2_15

E. [. Cimatti, F. Clarke, M. Giunchiglia, and . Roveri, NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer (STTT), pp.410-425, 2000.
DOI : 10.1007/s100090050046

G. [. Caselli, P. Conte, and . Marenzoni, Parallel state space exploration for GSPN models, Lecture Notes in Computer Science, vol.935, pp.181-200, 1995.
DOI : 10.1007/3-540-60029-9_40

J. [. Ciardo, D. Gluckman, and . Nicol, Distributed State Space Generation of Discrete-State Stochastic Models, INFORMS Journal on Computing, vol.10, issue.1, pp.82-93, 1998.
DOI : 10.1287/ijoc.10.1.82

E. Chang and R. Roberts, An improved algorithm for decentralized extrema-finding in circular configurations of processes, Communications of the ACM, vol.22, issue.5, pp.281-283, 1979.
DOI : 10.1145/359104.359108

]. D. Dil96 and . Dill, The Mur? Verification System, Proceedings of the 8th International Conference on Computer-Aided Verification CAV'96, pp.390-393, 1996.

I. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier et al., CADP a protocol validation and verification toolbox, Proceedings of the 8th Conference on Computer-Aided Verification, pp.437-440, 1996.
DOI : 10.1007/3-540-61474-5_97

H. Garavel, . Open, and . Caesar, OPEN/C??SAR: An open software architecture for verification, simulation, and testing, Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, pp.68-84, 1998.
DOI : 10.1007/BFb0054165

]. W. Ghll-+-98, S. Gropp, A. Huss-lederman, E. Lumsdaine, B. Lusk et al., MPI: The Complete Reference, The MPI-2 Extensions, 1998.

H. Garavel and L. Mounier, Specification and verification of various distributed leader election algorithms for unidirectional ring networks, Science of Computer Programming, vol.29, issue.1-2, pp.171-197, 1997.
DOI : 10.1016/S0167-6423(96)00034-2

A. [. Haverkort, H. C. Bell, and . Bohnenkamp, On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets, Proceedings 8th International Workshop on Petri Nets and Performance Models (Cat. No.PR00331), pp.12-21, 1999.
DOI : 10.1109/PNPM.1999.796528

T. Heyman, D. Geist, O. Grumberg, and A. Schuster, Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits, Proceedings of the 12th International Conference on Computer-Aided Verification CAV'2000, pp.20-35, 2000.
DOI : 10.1007/10722167_6

]. C. Hoa85 and . Hoare, Communicating Sequential Processes, 1985.

J. Gerard and . Holzmann, Design and Validation of Computer Protocols. Software Series, 1991.

]. G. Hol97 and . Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.

[. Iec, LOTOS ? A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, International Organization for Standardization ? Information Processing Systems ? Open Systems Interconnection, 1988.

J. Jézéquel, W. M. Ho, A. L. Guennec, and F. Pennaneac-'h, UMLAUT: an Extendible UML Transformation Framework, Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE'99, 1999.

P. [. Knottenbelt and . Harrison, Distributed Disk-Based Solution Techniques for Large Markov Models, Proceedings of the 3rd International Meeting on the Numerical Solution of Markov Chains NSMC'99, pp.58-75, 1999.

W. J. Knottenbelt, M. A. Mestern, P. G. Harrison, and P. Kritzinger, Probability, Parallelism and the State Space Exploration Problem, Proceedings of the 10th International Conference on Computer Performance Evaluation -Modelling, Techniques and Tools TOOLS'98 (Palma de Mallorca, Spain), volume 1469 of Lecture Notes in Computer Science, pp.165-179, 1998.
DOI : 10.1007/3-540-68061-6_14

[. Lann, Distributed Systems ? Towards a Formal Approach, Information Processing 77, pp.155-160, 1977.

R. [. Lerda and . Sista, Distributed-Memory Model Checking with SPIN, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking SPIN'99, pp.22-39, 1999.
DOI : 10.1007/3-540-48234-2_3

]. F. Mat87 and . Mattern, Algorithms for Distributed Termination Detection, Distributed Computing, pp.161-175, 1987.

S. [. Marenzoni, G. Caselli, and . Conte, Analysis of large GSPN models: a distributed solution tool, Proceedings of the Seventh International Workshop on Petri Nets and Performance Models, pp.122-131, 1997.
DOI : 10.1109/PNPM.1997.595543

[. Milner, Communication and Concurrency, 1989.

[. Mateescu and M. Sighireanu, Efficient on-the-fly model-checking for regular alternation-free mu-calculus, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 GMD Report 91, pp.65-86, 2000.
DOI : 10.1016/S0167-6423(02)00094-1
URL : https://hal.archives-ouvertes.fr/inria-00072755

G. [. Nicol and . Ciardo, Automated Parallelization of Discrete State-Space Generation, Journal of Parallel and Distributed Computing, vol.47, issue.2, pp.153-167, 1997.
DOI : 10.1006/jpdc.1997.1409

J. Romijn, Model Checking the HAVi Leader Election Protocol, 1999.

S. [. Ramakrishna and . Smolka, Partial-order reduction in the weak modal mu-calculus, Proceedings of the 8th International Conference on Concurrency Theory CONCUR'97, pp.5-24, 1997.
DOI : 10.1007/3-540-63141-0_2

D. [. Stern and . Dill, Parallelizing the Mur?? verifier, Proceedings of the 9th International Conference on Computer-Aided Verification CAV'97, pp.256-267, 1997.
DOI : 10.1007/3-540-63166-6_26

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-l` es-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche, 2004.

I. Editeur and . De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399