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

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

G. Ausiello and G. F. Italiano, On-line algorithms for polynomially solvable satisfiability problems, The Journal of Logic Programming, vol.10, issue.1, pp.69-90, 1991.
DOI : 10.1016/0743-1066(91)90006-B

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

J. A. Bergstra, A. Ponse, and S. A. Smolka, Handbook of Process Algebra, 2001.

A. Bouajjani, J. Fernandez, S. Graf, C. Rodríguez, and J. Sifakis, Safety for branching time semantics, Proceedings of 18th ICALP, 1991.
DOI : 10.1007/3-540-54233-7_126
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.1049

S. D. Brookes, C. A. Hoare, and A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM, vol.31, issue.3, pp.560-599, 1984.
DOI : 10.1145/828.833

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 M. Hennessy, Testing equivalence as a bisimulation equivalence, Formal Aspects of Computing, vol.85, issue.n. 2, pp.1-20, 1993.
DOI : 10.1007/BF01211314

R. Cleaveland and O. Sokolsky, Equivalence and Preorder Checking for Finite-State Systems, Handbook of Process Algebra, chapter 6, pp.391-424, 2001.
DOI : 10.1016/B978-044482830-9/50024-2

R. Cleaveland and B. Steffen, Computing behavioural relations, logically, Proceedings of the 18th Internationan Colloquium on Automata, Languages, and Programming ICALP'91, pp.127-138, 1991.
DOI : 10.1007/3-540-54233-7_129
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.6069

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.

A. Dovier, C. Piazza, and A. Policriti, An efficient algorithm for computing bisimulation equivalence, Theoretical Computer Science, vol.311, issue.1-3, pp.221-256, 2004.
DOI : 10.1016/S0304-3975(03)00361-X
URL : http://doi.org/10.1016/s0304-3975(03)00361-x

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.7380

J. Fernandez and L. Mounier, Verifying Bisimulations On the Fly, Proceedings of the 3rd International Conference on Formal Description Techniques FORTE'90

J. Fernandez and L. Mounier, A tool set for deciding behavioral equivalences, Proceedings of CONCUR'91, 1991.
DOI : 10.1007/3-540-54430-5_78

K. Fisler and M. Y. Vardi, Bisimulation Minimization and Symbolic Model Checking, pp.39-78, 2002.
DOI : 10.1007/3-540-48153-2_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.399

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, R. Mateescu, and W. Serwe, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, Proceedings of the 19th International Conference on Computer Aided Verification CAV'2007, pp.158-163, 2007.
DOI : 10.1007/978-3-540-73368-3_18
URL : https://hal.archives-ouvertes.fr/inria-00189021

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

J. Friso-groote and M. Keinänen, Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points, Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS, pp.436-450, 2004.
DOI : 10.1007/978-3-540-24730-2_33

A. Ingolfsdottir and B. Steffen, Characteristic Formulae for Processes with Divergence. Information and Computation, pp.149-163, 1994.

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

S. C. Kleene, Introduction to Metamathematics, 1952.

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

X. Liu and S. A. 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

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

A. J. Martin, Compiling communicating processes into delay-insensitive VLSI circuits, Distributed Computing, vol.20, issue.8, pp.226-234, 1986.
DOI : 10.1007/BF01660034
URL : http://authors.library.caltech.edu/26661/2/postscript.pdf

R. Mateescu, Efficient Diagnostic Generation for Boolean Equation Systems, Proceedings of 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2000, 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, Proceedings 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, 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

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.

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

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

S. K. Shukla, H. B. Hunt, I. , and D. J. Rosenkrantz, HORNSAT, model checking, verification and games, Proceedings of the 8th International Conference on Computer Aided Verification CAV'96, pp.99-110
DOI : 10.1007/3-540-61474-5_61
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.7132

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.327.8418

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

A. Valmari and M. Tienari, Compositional failure-based semantic models for Basic LOTOS, Formal Aspects of Computing, vol.37, issue.9, pp.440-468, 1995.
DOI : 10.1007/BF01211218
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.739

R. J. Van-glabbeek and W. P. Weijland, Branching-Time and Abstraction in Bisimulation Semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Also in proc. IFIP 11th World Computer Congress, 1989.

R. Van-glabbeek, The Linear Time ? Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes, Handbook of Process Algebra, pp.3-100, 2001.

. Vasy, The VLTS Benchmark Suite, 2003.

B. Vergauwen and J. Lewi, Efficient local correctness checking for single and alternating boolean equation systems, Proceedings of the 21st ICALP (Vienna), pp.304-315, 1994.
DOI : 10.1007/3-540-58201-0_77

I. Centre-de-recherche and . Futurs, 4, rue Jacques Monod -Bât. G -91893 Orsay Cedex (France) Centre de recherche INRIA Nancy ? Grand Est : 615, rue du Jardin Botanique -54600 Villers-lès-Nancy (France) Centre de recherche INRIA Rennes ? Bretagne Atlantique : Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Centre de recherche INRIA Paris ? Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Centre de recherche, 2004.