R. Mateescu and A. J. Wijs, Property-Dependent Reductions for the Modal Mu-Calculus, Proceedings of the 18th International SPIN Workshop on Model Checking Software (SPIN'11), pp.2-19, 2011.
DOI : 10.1007/978-3-642-22306-8_2
URL : https://hal.archives-ouvertes.fr/inria-00609585

J. Baeten, A brief history of process algebra, Theoretical Computer Science, vol.335, issue.2-3, pp.131-146, 2005.
DOI : 10.1016/j.tcs.2004.07.036

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, pp.333-354, 1983.
DOI : 10.7146/dpb.v11i146.7420

R. D. Nicola and F. W. Vaandrager, Action versus state based logics for transition systems, Semantics of Systems of Concurrent Processes, pp.407-419, 1990.
DOI : 10.1007/3-540-53479-2_17

R. V. Glabbeek and W. Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM, vol.43, issue.3, pp.555-600, 1996.
DOI : 10.1145/233551.233556

R. Barbuti, N. De-francesco, A. Santone, and G. Vaglini, Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems, Journal of Computer and System Sciences, vol.59, issue.3, pp.537-556, 1999.
DOI : 10.1006/jcss.1999.1660

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

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

A. Fantechi, S. Gnesi, and G. Ristori, Modelling transition systems within an action based logic, 1995.

A. Fantechi, S. Gnesi, F. Mazzanti, R. Pugliese, and E. Tronci, A Symbolic Model Checker for ACTL, Proceedings of the International Workshop on Current Trends in Applied Formal Methods FM-Trends'98, pp.228-242, 1998.
DOI : 10.1007/3-540-48257-1_14

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2011: a toolbox for the construction and analysis of distributed processes, International Journal on Software Tools for Technology Transfer, vol.1, issue.1/2, pp.89-107, 2013.
DOI : 10.1007/s10009-012-0244-z
URL : https://hal.archives-ouvertes.fr/hal-00715056

R. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing , STOC '81, pp.121-141, 1982.
DOI : 10.1145/800076.802492

E. A. Emerson and C. Lei, Efficient model checking in fragments of the propositional mu-calculus, Proceedings of the 1st International Symposium on Logic in Computer Science LICS'86, pp.267-278, 1986.

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

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

S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS, Proceedings of the 11th International Colloquium on Automata, Languages and Programming (ICALP'84), pp.222-234, 1984.
DOI : 10.1007/3-540-13345-3_20

M. Müller-olm, Derivation of Characteristic Formulae, Proceedings of the MFCS'98 Workshop on Concurrency, pp.159-170, 1998.
DOI : 10.1016/S1571-0661(05)80257-9

B. Steffen and A. Ingólfsdóttir, Characteristic Formulas for Processes with Divergence, Information and Computation, vol.110, issue.1, pp.149-163, 1994.
DOI : 10.1006/inco.1994.1028

L. Aceto, A. Ingólfsdóttir, and J. Sack, Characteristic Formulae for Fixed- Point Semantics: A General Framework, Proceedings of the 16th International Workshop on Expressiveness in Concurrency (EXPRESS'09) of Electronic Proceedings in Theoretical Computer Science, pp.1-15, 2009.

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

R. V. Glabbeek, B. Luttik, and N. Tr?ka, Computation Tree Logic with Deadlock Detection, Logical Methods in Computer Science, vol.5, issue.4, pp.1-24, 2009.
DOI : 10.2168/LMCS-5(4:5)2009

M. Dam, CTL??? and ECTL??? as fragments of the modal ??-calculus, Theoretical Computer Science, vol.126, issue.1, pp.77-96, 1994.
DOI : 10.1016/0304-3975(94)90269-0

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, Proceedings of the 15th International Symposium on Formal Methods (FM'08), pp.148-164, 2008.
DOI : 10.1007/978-3-540-68237-0_12
URL : https://hal.archives-ouvertes.fr/inria-00315312

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

R. Mateescu and C. 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

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), pp.411-420, 1999.

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.

N. Coste, H. Garavel, H. Hermanns, F. Lang, R. Mateescu et al., Ten Years of Performance Evaluation for Concurrent Systems Using CADP, Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'10), Part II, pp.128-142, 2010.
DOI : 10.1007/978-3-642-16561-0_18
URL : https://hal.archives-ouvertes.fr/inria-00532914

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 IFIP, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

E. Lantreibecq and W. Serwe, Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP, Science of Computer Programming, to appear

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

R. Mateescu and A. J. Wijs, Efficient On-the-Fly Computation of Weak Tau-Confluence, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00407381

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 and A. J. Wijs, Sequential and distributed on-the-fly computation of weak tau-confluence, Science of Computer Programming, vol.77, issue.10-11, pp.10-11
DOI : 10.1016/j.scico.2011.07.004
URL : https://hal.archives-ouvertes.fr/hal-00676451

A. J. Wijs, What To Do Next?: Analysing and Optimising System Behaviour in Time, 2007.

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

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