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

H. R. Andersen and B. Vergauwen, Efficient checking of behavioural relations and modal assertions using fixed-point inversion, Proc. of the 7th International Conference on Computer Aided Verification CAV'95, pp.142-154, 1995.
DOI : 10.1007/3-540-60045-0_47

A. Arnold and P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems, Information Processing Letters, vol.29, issue.2, pp.57-66, 1988.
DOI : 10.1016/0020-0190(88)90029-4

J. C. Baeten and R. J. Van-glabbeek, Another look at abstraction in process algebra, Proc. of ICALP'87, pp.84-94, 1987.
DOI : 10.1007/3-540-18088-5_8

A. Bouajjani, J. Fernandez, S. Graf, C. Rodríguez, and J. Sifakis, Safety for branching time semantics, Proc. of the 18th International Colloquium on Automata, Languages , and Programming ICALP'91, 1991.
DOI : 10.1007/3-540-54233-7_126

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, p.35, 1986.
DOI : 10.1109/TC.1986.1676819

R. Mateescu, Man page of the Caesar Solve 1 library, INRIA Rhône-Alpes, 2005.

E. M. Clarke, E. A. Emerson, and A. P. 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

E. M. Clarke, O. Grumberg, K. L. Mcmillan, and X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation conference , DAC '95, pp.427-432, 1995.
DOI : 10.1145/217474.217565

R. Cleaveland, J. Parrow, and B. Steffen, The concurrency workbench, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.36-72, 1993.
DOI : 10.1007/3-540-52148-8_3

R. Cleaveland and B. Steffen, Computing behavioural relations, logically
DOI : 10.1007/3-540-54233-7_129

R. Cleaveland and B. Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus, Proc. of the 3rd International Conference on Computer Aided Verification CAV'91, pp.48-58, 1991.
DOI : 10.1007/3-540-55179-4_6

R. Cleaveland and B. Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus, Formal Methods in System Design, pp.121-147, 1993.

W. F. Dowling and J. H. Gallier, Linear-time algorithms for testing the satisfiability of propositional horn formulae, The Journal of Logic Programming, vol.1, issue.3, pp.267-284, 1984.
DOI : 10.1016/0743-1066(84)90014-1

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

E. A. Emerson and C. Lei, Efficient model checking in fragments of the propositional mu-calculus, Proc. of the 1st LICS, pp.267-278, 1986.

A. Fantechi, S. Gnesi, and G. Ristori, From ACTL to mu-calculus, Proc. of the ERCIM Workshop on Theory and Practice in Verification, pp.3-10, 1992.

J. Fernandez, C. Jard, T. Jéron, L. Nedelka, and C. Viho, Using on-the-fly verification techniques for the generation of test suites, Proc. of the 8th International Conference on Computer-Aided Verification CAV'96, pp.348-359, 1996.
DOI : 10.1007/3-540-61474-5_82
URL : https://hal.archives-ouvertes.fr/inria-00073711

J. Fernandez and L. Mounier, ???On the fly??? verification of behavioural equivalences and preorders, Proc. of the 3rd International Workshop on Computer-Aided Verification CAV'91, 1991.
DOI : 10.1007/3-540-55179-4_18

M. J. Fischer and R. E. 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, Proc. of the 1st 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, An overview of CADP European Association for Software Science and Technology (EASST) Newsletter, pp.13-24, 2001.

H. Garavel, R. Mateescu, and . Seq, OPEN: a tool for efficient trace-based verification, Proc. of the 11th International SPIN Workshop on Model Checking of Software SPIN Lecture Notes in Computer Science 2989, pp.150-155, 2004.

J. F. Groote and M. Keinänen, Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points, Proc. of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS Lecture Notes in Computer Science 2988, pp.436-450, 2004.
DOI : 10.1007/978-3-540-24730-2_33

J. F. Groote and J. Van, State Space Reduction Using Partial ??-Confluence, Proc. of the 25th International Symposium on Mathematical Foundations of Computer Science MFCS'2000 Lecture Notes in Computer Science 1893, pp.383-393, 2000.
DOI : 10.1007/3-540-44612-5_34

H. Hermanns and M. Siegle, Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation, Proc. of the 5th International AMAST Workshop ARTS'99 Lecture Notes in Computer Science 1601, pp.244-265, 1999.
DOI : 10.1007/3-540-48778-6_15

A. J. Hu, Techniques for efficient formal verification using binary decision diagrams, 1995.

A. Ingolfsdottir and B. Steffen, Characteristic formulae for processes with divergence, Information and Computation, vol.110, issue.1, pp.149-163, 1994.

O. Kupferman, M. Vardi, and P. Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM, vol.47, issue.2, pp.312-360, 2000.
DOI : 10.1145/333979.333987

K. G. Larsen, Efficient local correctness checking, Proc. of the 4th International Workshop in Computer Aided Verification CAV'92, pp.30-43, 1992.
DOI : 10.1007/3-540-56496-9_4

X. Liu, C. R. Ramakrishnan, and S. A. Smolka, Fully local and efficient evaluation of alternating fixed points, Proc. of the 1st International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 Lecture Notes in Computer Science 1384, pp.5-19, 1998.
DOI : 10.1007/BFb0054161

X. Liu and S. A. Smolka, Simple linear-time algorithms for minimal fixed points, Proc. of the 25th International Colloquium on Automata, Languages, and Programming ICALP'98 Lecture Notes in Computer Science 1443, pp.53-66, 1998.
DOI : 10.1007/BFb0055040

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

R. Mateescu, Efficient Diagnostic Generation for Boolean Equation Systems, Proc. of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2000, pp.251-265, 2000.
DOI : 10.1007/3-540-46419-0_18
URL : https://hal.archives-ouvertes.fr/inria-00072795

R. Mateescu, Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems, Proc. of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2002, pp.281-295, 2002.
DOI : 10.1007/3-540-46002-0_20
URL : https://hal.archives-ouvertes.fr/inria-00072158

R. 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. Milner, Communication and Concurrency, 1989.

R. , D. Nicola, and F. W. Vaandrager, Action versus state based logics for transition systems, Semantics of Concurrency, pp.407-419, 1990.

R. De-nicola, U. Montanari, and F. Vaandrager, Back and forth bisimulations, Centrum voor Wiskunde en Informatica, 1990.
DOI : 10.1007/BFb0039058

G. Pace, F. Lang, and R. Mateescu, Calculating ??-Confluence Compositionally, Proc. 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

D. Park, Concurrency and automata on infinite sequences, Theoretical Computer Science, pp.167-183, 1981.
DOI : 10.1007/BFb0017309

B. Steffen, A. Classen, M. Klein, J. Knoop, and T. Margaria, The fixpoint-analysis machine, Proc. of the 6th International Conference on Concurrency Theory CONCUR'95, pp.72-87, 1995.
DOI : 10.1007/3-540-60218-6_6

B. Steffen, T. Margaria, A. Classen, and V. Braun, The METAFrame'95 environment, Proc. of the 8th Conference on Computer-Aided Verification CAV'96 Lecture Notes in Computer Science 1102, pp.450-453, 1996.
DOI : 10.1007/3-540-61474-5_100

B. Steffen, T. Margaria, and V. Braun, The Electronic Tool Integration platform: concepts and design, International Journal on Software Tools for Technology Transfer (STTT), pp.1-29, 1997.
DOI : 10.1007/s100090050003

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

R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

M. Thorup, Near-optimal fully-dynamic graph connectivity, Proceedings of the thirty-second annual ACM symposium on Theory of computing , STOC '00, 2000.
DOI : 10.1145/335305.335345

R. J. Van-glabbeek and W. P. Weijland, Branching-time and abstraction in bisimulation semantics (extended abstract) Computer Science Report CS R8911, Centrum voor Wiskunde en Informatica, Proc. of IFIP 11th World Computer Congress, 1989.

B. Vergauwen and J. Lewi, A linear algorithm for solving fixed-point equations on transition systems, Proc. of the 17th Colloquium on Trees in Algebra and Programming CAAP'92, pp.322-341, 1992.
DOI : 10.1007/3-540-55251-0_18

B. Vergauwen and J. Lewi, Efficient local correctness checking for single and alternating boolean equation systems, Proc. of the 21st International Colloquium on Automata, Logic, and Programming ICALP'94, pp.304-315, 1994.
DOI : 10.1007/3-540-58201-0_77

B. Vergauwen, J. Wauman, and J. Lewi, Efficient fixpoint computation, Proc. of the 1st International Static Analysis Symposium SAS'94, pp.314-328, 1994.
DOI : 10.1007/3-540-58485-4_49

B. Yang, R. E. Bryant, D. R. O-'hallaron, A. Biere, O. Coudert et al., A Performance Study of BDD-Based Model Checking, Proc. of FMCAD'98, pp.255-289, 1998.
DOI : 10.1007/3-540-49519-3_18

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