R. Mateescu, D. Bergamini, N. Descoubes, C. Joubert, R. Kim et al., BISIMULATOR : A Modular Tool for On-the-Fly Equivalence Checking, Proc. of the 11 th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005, pp.156-161, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00685325

C. [. Brookes, A. W. Hoare, . [. Roscoe, J. J. Bos, . Kleijnfronczak et al., A Theory of Communicating Sequential Processes Formal Specification and Analysis of Industrial Systems Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking : Analysis of the Nutritional Stress Response in Escherichia Coli Analyzing a ? Model of a Turntable System using Spin, CADP and UPPAAL, Proc. of the 4 th Int. School on Formal Methods for the Design of Computer, Communication, and Software Systems SFM-RT'04 Thèse de DoctoratBRdJ + 05] Systèmes temps reél 1 ? techniques de description et de vérification, pp.200-236560, 1984.

M. B. Dwyer, G. S. Avrunin, J. C. Corbettfl79-]-m, R. E. Fischer, and . Ladner, Patterns in Property Specifications for Finite-State Verification, Proc. of the 21 st Int. Conference on Software Engineering ICSE'99EM85] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1 ? Equations and Initial Semantics Propositional Dynamic Logic of Regular Programs . Journal of Computer and System Sciences, pp.411-420194, 1979.

H. Garavel, Compilation of LOTOS Abstract Data Types

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

H. Garavel and H. Hermanns, On Combining Functional Verification and Performance Evaluation Using CADP
DOI : 10.1007/3-540-45614-7_23
URL : https://hal.archives-ouvertes.fr/inria-00072096

H. Garavel and F. Lang, SVL: A Scripting Language for Compositional Verification, Proc. of the 21 st IFIP WG 6.1 Int. Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

H. Garavel, F. Lang, and R. Mateescu, An Overview of CADP European Association for Software Science and Technology (EASST) Newsletter, pp.13-24, 2001.

H. Garavel, R. Mateescu, D. Bergamini, A. Curic, N. Descoubes et al., DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation, Proc. of the 12 th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006, pp.445-449, 2006.
DOI : 10.1007/3-540-44612-5_34

H. Garavel, R. Mateescu, and I. Smarandache, Parallel state space construction for model-checking, Proc. of the 8 th Int. SPIN Workshop on Model Checking of Software SPIN, pp.217-234, 2001.
DOI : 10.1007/3-540-45139-0_14
URL : https://hal.archives-ouvertes.fr/inria-00072247

J. Friso-groote, The Syntax and Semantics of Timed muCRL, 1997.

H. Garavel and J. Sifakis, Compilation and Verification of LOTOS Specifications, Proc. of the 10 th Int. Symposium on Protocol Specification, Testing and Verification 30 R. Mateescu for the Construction and Analysis of Systems TACAS'2003, pp.379-394, 1990.

G. Holzmann, The SPIN Model Checker ? Primer and Reference Manual, 2003.

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

C. Joubert and R. Mateescu, Distributed On-the-Fly Equivalence Checking, Proc. of the 3 rd Int. Workshop on Parallel and Distributed Methods in Verification PDMC, 2004.
DOI : 10.1016/j.entcs.2004.10.018

C. Joubert and R. Mateescu, Distributed Local Resolution of Boolean Equation Systems, 13th Euromicro Conference on Parallel, Distributed and Network-Based Processing, pp.264-271, 2005.
DOI : 10.1109/EMPDP.2005.19
URL : https://hal.archives-ouvertes.fr/hal-00683892

C. Joubert and R. Mateescu, Distributed On-the-Fly Model Checking and Test Case Generation, Proceedings of the 13th International SPIN Workshop on Model Checking of Software SPIN'2006 Lecture Notes in Computer Science, 2006.
DOI : 10.1007/BFb0054166
URL : https://hal.archives-ouvertes.fr/inria-00071388

]. D. Koz83 and . Kozen, Results on the Propositional µ-calculus, Theoretical Computer Science, vol.27, pp.333-354, 1983.

[. Lang and . Exp, Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods, Proc. of the 5 th Int. Conference on Integrated Formal Methods IFM'2005, pp.70-88, 2005.
DOI : 10.1007/11589976_6
URL : https://hal.archives-ouvertes.fr/inria-00070339

R. Mateescu, Efficient Diagnostic Generation for Boolean Equation Systems
DOI : 10.1007/3-540-46419-0_18
URL : https://hal.archives-ouvertes.fr/inria-00072795

R. Mateescu, A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems, Proc. of the 9 th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003, pp.81-96, 2003.
DOI : 10.1007/3-540-36577-X_7
URL : https://hal.archives-ouvertes.fr/inria-00071875

R. Mateescu, On-the-fly state space reductions for weak equivalences, Proceedings of the 10th international workshop on Formal methods for industrial critical systems , FMICS '05, pp.80-89, 2005.
DOI : 10.1145/1081180.1081191

R. Mateescu, . Caesar, and . Solve, CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems, International Journal on Software Tools for Technology Transfer, vol.8, issue.1, pp.37-56, 2006.
DOI : 10.1007/s10009-005-0194-9
URL : https://hal.archives-ouvertes.fr/inria-00084628

[. Milner, Communication and Concurrency, 1989.

[. Mateescu and M. Sighireanu, Efficient on-the-fly model-checking for regular alternation-free mu-calculus, Science of Computer Programming, vol.46, issue.3, pp.255-281, 2003.
DOI : 10.1016/S0167-6423(02)00094-1
URL : https://hal.archives-ouvertes.fr/inria-00072755

R. De, N. , and F. W. Vaandrager, Action versus State Based Logics for Transition Systems, Semantics of Systems of Concurrent Processes, pp.407-419, 1990.

[. Pace, F. Lang, and R. Mateescu, Calculating ??-Confluence Compositionally, Proc. of the 15 th Int. Conference on Computer Aided Verification CAV'2003, pp.446-459, 2003.
DOI : 10.1007/978-3-540-45069-6_41
URL : https://hal.archives-ouvertes.fr/inria-00071661

G. Salaün and W. Serwe, Translating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS, Proc. of the 5 th Int. Conference on Integrated Formal Methods IFM'2005, pp.287-306, 2005.
DOI : 10.1007/11589976_17

R. R. Schiffelers, D. A. Van-beek, K. L. Man, M. A. Reniers, and J. E. Rooda, Formal Semantics of Hybrid Chi, Proc. of the 1 st Int. Workshop on Formal Modeling and Analysis of Timed Systems FORMATS'03 volume 2791 of Lecture Notes in Computer Science, pp.151-165, 2003.
DOI : 10.1007/978-3-540-40903-8_12

I. Unité-de-recherche and . Rhône, Alpes 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4

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