H. R. Andersen, Model checking and boolean graphs, Theoretical Computer Science, vol.126, issue.1, pp.3-30, 1994.
DOI : 10.1016/0304-3975(94)90266-6

URL : http://dx.doi.org/10.1016/0304-3975(94)90266-6

R. Henrik, B. Andersen, and . Vergauwen, Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion, Proceedings of the 7th International Conference on Computer Aided Verification CAV'95, pp.142-154, 1995.

J. Barnat, L. Brim, and J. Stribrna, Distributed LTL model-checking in SPIN, Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001, pp.200-216, 2001.
DOI : 10.1007/3-540-45139-0_13

I. Bergamini, N. Descoubes, C. Joubert, and R. Mateescu, BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005, pp.581-585, 2005.
DOI : 10.1007/978-3-540-31980-1_42

URL : https://hal.archives-ouvertes.fr/hal-00685325

[. Bollig, M. Leucker, and M. Weber, Local Parallel Model Checking for the Alternation-Free ??-Calculus, Proceedings of the 9th International SPIN Workshop on Model Checking of Software SPIN'2002, pp.128-147, 2002.
DOI : 10.1007/3-540-46017-9_11

E. [. Clarke, A. P. Emerson, and . Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

X. Du, S. A. Smolka, and R. Cleaveland, Local model checking and protocol analysis, International Journal on Software Tools for Technology Transfer (STTT), pp.219-241, 1999.
DOI : 10.1007/s100090050031

C. [. Emerson and . Lei, Efficient Model Checking in Fragments of the Propositional Mu-Calculus, Proceedings of the 1st LICS, pp.267-278, 1986.

R. [. Fischer and . Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

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

H. Garavel, F. Lang, and R. Mateescu, Compiler Construction Using LOTOS NT, Proceedings of the 11th International Conference on Compiler Construction CC 2002, pp.9-13, 2002.
DOI : 10.1007/3-540-45937-5_3

[. Hermanns and C. Joubert, A Set of Performance and Dependability Analysis Components for CADP, Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003, pp.425-430, 2003.
DOI : 10.1007/3-540-36577-X_30

H. , S. T. Huang, and P. W. Kao, Detecting Termination of Distributed Computations by External Agents, Journal of Information Science and Engineering, vol.7, issue.2, pp.5880187-201, 1991.

[. Holmen, M. Leucker, and M. Lindstrom, UppDMC: A Distributed Model Checker for Fragments of the ??-Calculus, Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification PDMC, pp.91-105, 2004.
DOI : 10.1016/j.entcs.2004.10.021

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

C. Jard and T. Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer (STTT), pp.297-315, 2005.
DOI : 10.1007/s10009-004-0153-x

C. Joubert and R. Mateescu, Distributed On-the-Fly Equivalence Checking, Proceedings of the 3rd International 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

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

]. K. Lar88 and . Larsen, Proof Systems for Hennessy-Milner logic with Recursion, Proceedings of the 13th Colloquium on Trees in Algebra and Programming CAAP '88, pp.215-230, 1988.

S. [. Liu and . Smolka, Simple linear-time algorithms for minimal fixed points, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming ICALP'98, pp.53-66, 1998.
DOI : 10.1007/BFb0055040

R. [. Lerda and . Sisto, Distributed-Memory Model Checking with SPIN, Proceedings of the 5th and INRIA 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

M. Leucker, R. Somla, and M. Weber, Parallel Model Checking for LTL, CTL???, and L2??, Proceedings of the 2nd International Workshop on Parallel and Distributed Methods in Verification PDMC'2003, pp.4-16, 2003.
DOI : 10.1016/S1571-0661(05)80093-3

A. Mader, Verification of Modal Properties Using Boolean Equation Systems, 1997.

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

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, Proceedings of the 9th International 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

[. 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 (STTT), pp.37-56, 2005.
DOI : 10.1007/s10009-005-0194-9

URL : https://hal.archives-ouvertes.fr/inria-00084628

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

A. [. Manna and . Pnueli, The Temporal Logic of Reactive and Concurrent Systems , volume I (Specification), 1992.

[. 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

G. Pace, F. Lang, and R. Mateescu, Calculating ??-Confluence Compositionally, Proceedings of the 15th International 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

[. Stevens and C. Stirling, Practical model-checking using games, Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98, pp.85-101, 1998.
DOI : 10.1007/BFb0054166

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.5200

J. Tretmans, Test Generation with Inputs, Outputs and Repetitive Quiescence, Software ? Concepts and Tools, pp.103-120, 1996.
DOI : 10.1007/3-540-61042-1_42

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.475.9528

R. Ziller and K. Schneider, Combining supervisor synthesis and model checking, ACM Transactions on Embedded Computing Systems, vol.4, issue.2, pp.331-362, 2005.
DOI : 10.1145/1067915.1067920

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.519.8024

I. Unité-de-recherche and I. 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