A. Bouali, A. Ressouche, V. Roy, R. , and S. , The Fc2Tools set: a Toolset for the Verification of Concurrent Systems, Proceedings of the 8th Conference on Computer-Aided Verification volume 1102 of Lecture Notes in Computer Science, 1996.

J. Volker-braun, T. Kreileder, B. Margaria, and . Steffen, The ETI Online Service in Action, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp.439-443, 1999.
DOI : 10.1007/3-540-49059-0_31

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

E. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, 10th Annual Symposium on Principles of Programming Languages, 1983.
DOI : 10.1145/5397.5399

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in Property Specifications for Finite-State Verification, Proceedings of the 21st International Conference on Software Engineering ICSE'99, 1999.

J. Fernandez, An implementation of an efficient algorithm for bisimulation equivalence, Science of Computer Programming, vol.13, issue.2-3, pp.219-236, 1990.
DOI : 10.1016/0167-6423(90)90071-K

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

J. Fernandez and L. Mounier, A Local Checking Algorithm for Boolean Equation Systems, 1995.

H. Garavel, Compilation et vérification de programmes LOTOS, Thèse de Doctorat, 1989.

H. Garavel, Compilation of LOTOS Abstract Data Types, Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89, pp.147-162, 1989.

H. Garavel, Binary Coded Graphs: Definition of the BCG Format, 1991.

H. Garavel, An Overview of the Eucalyptus Toolbox, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, pp.76-88, 1996.

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 and F. Lang, SVL: A Scripting Language for Compositional Verification, Proceedings of the 21st IFIP WG 6.1 International 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, C. Viho, and M. Zendri, System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation, Springer International Journal on Software Tools for Technology Transfer (STTT), vol.3, issue.3, pp.314-331, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072597

J. Friso-groote and F. Vaandrager, An efficient algorithm for branching bisimulation and stuttering equivalence, Proceedings of the 17th ICALP, pp.626-638
DOI : 10.1007/BFb0032063

J. F. Groote and J. C. Van-pol, State space reduction using partial tau-confluence, 2000.
DOI : 10.1007/3-540-44612-5_34
URL : http://library.tue.nl/csp/dare/LinkToRepository.csp?recordnumber=660478

M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol.32, issue.1, pp.137-161, 1985.
DOI : 10.1145/2455.2460

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, 1988.

T. Jéron and P. Morel, Test Generation Derived from Model-Checking, Proceedings of the Conference on Computer-Aided Verification CAV'99, pp.108-122, 1999.
DOI : 10.1007/3-540-48683-6_12

J. Krimm and L. Mounier, Compositional State Space Generation from LOTOS Programs Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of TACAS'97, 1997.

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, pp.251-265, 2000.
DOI : 10.1007/3-540-46419-0_18
URL : https://hal.archives-ouvertes.fr/inria-00072795

R. Mateescu and H. Garavel, XTL: A Meta-Language and Tool for Temporal Logic Model-Checking, Proceedings of the International Workshop on Software Tools for Technology Transfer STTT'98, pp.33-42, 1998.

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

R. , D. Nicola, and F. W. Vaandrager, Action versus State based Logics for Transition Systems, Semantics of Concurrency, pp.407-419, 1990.

R. Paige and R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing, vol.16, issue.6, pp.973-989, 1987.
DOI : 10.1137/0216062

C. Pecheur, Improving the Specification of Data Types in Lotos, Collection of Publications of the Faculty of Applied Sciences, 1996.

J. Queille and J. Sifakis, Fairness and related properties in transition systems ? a temporal logic to deal with fairness, Acta Informatica, vol.19, issue.3, pp.195-220, 1983.
DOI : 10.1007/BF00265555

V. Roy, R. De, and S. , Auto/Autograph
DOI : 10.1007/bf00121126

B. Steffen, T. Margaria, and V. Braun, The Electronic Tool Integration platform: concepts and design, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.9-30, 1997.
DOI : 10.1007/s100090050003

B. Stepien, J. Tourrilhes, and J. Sincennes, ELUDO: The University of Ottawa LO- TOS Toolkit, 1994.

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