R. Armoni, L. Fix, and A. Flaisher, The ForSpec Temporal Logic: A New Temporal Property-Specification Language, TACAS'02, pp.296-211
DOI : 10.1007/3-540-46002-0_21

T. Arts, C. Earle, and J. Derrick, Development of a verified Erlang program for resource locking, International Journal on Software Tools for Technology Transfer, vol.27, issue.2-3, pp.205-220, 2004.
DOI : 10.1016/0304-3975(82)90125-6

H. Barringer, A. Goldberg, K. Havelund, and K. Sen, Rule-Based Runtime Verification, pp.44-57
DOI : 10.1007/978-3-540-24622-0_5

I. Beer, S. Ben-david, C. Eisner, D. Fisman, A. Gringauze et al., The Temporal Logic Sugar, CAV'01, pp.363-367
DOI : 10.1007/3-540-44585-4_33

E. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.

R. Cleaveland and B. Steffen, A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus, FMSD, vol.2, issue.2, pp.121-147, 1993.

M. Dam, Model Checking Mobile Processes (Full version), Research Report RR Swedish Institute of Computer Science, vol.94, issue.1, 1994.
DOI : 10.1007/3-540-57208-2_3

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

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

E. A. Emerson and J. Y. Halpern, ???Sometimes??? and ???not never??? revisited: on branching versus linear time temporal logic, Journal of the ACM, vol.33, issue.1, pp.151-178, 1986.
DOI : 10.1145/4904.4999

E. A. Emerson and C. Lei, Efficient Model Checking in Fragments of the Propositional Mu-Calculus, LICS'86, pp.267-278, 1986.

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, An Open Software Architecture for Verification, Simulation, and Testing, TACAS'98, pp.68-84
URL : https://hal.archives-ouvertes.fr/inria-00073337

H. Garavel and H. Hermanns, On Combining Functional Verification and Performance Evaluation Using CADP, FME'02, pp.410-429
DOI : 10.1007/3-540-45614-7_23

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

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, CAV'07, pp.158-163
DOI : 10.1007/978-3-540-73368-3_18

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

J. F. Groote and T. A. Willemse, Parameterised boolean equation systems, Theoretical Computer Science, vol.343, issue.3, pp.332-369, 2005.
DOI : 10.1016/j.tcs.2005.06.016

URL : http://doi.org/10.1016/j.tcs.2005.06.016

J. F. Groote and R. Mateescu, Verification of Temporal Properties of Processes in a Setting with Data, AMAST'98, pp.74-90
DOI : 10.1007/3-540-49253-4_8

J. Y. Halpern and J. H. Reif, The propositional dynamic logic of deterministic, well-structured programs, Theoretical Computer Science, vol.27, issue.1-2, pp.127-165, 1983.
DOI : 10.1016/0304-3975(83)90097-X

K. Hamaguchi, H. Hiraishi, and S. Yajima, Branching time regular temporal logic for model checking with linear time complexity, CAV'90
DOI : 10.1007/BFb0023739

G. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003.
DOI : 10.1109/32.588521

I. Iec, LOTOS ? A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, Int. Std, vol.8807, 1989.

C. Joubert and R. Mateescu, Distributed On-the-Fly Model Checking and Test Case Generation, pp.126-145
DOI : 10.1007/BFb0054166

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

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

K. G. Larsen, Proof Systems for Hennessy-Milner logic with Recursion, pp.215-230

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

R. Mateescu, Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus. VMCAI'98, 1998.

R. Mateescu, Efficient Diagnostic Generation for Boolean Equation Systems, TACAS'00, pp.251-265
DOI : 10.1007/3-540-46419-0_18

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

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.

A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science, vol.13, issue.1, pp.45-60, 1981.
DOI : 10.1016/0304-3975(81)90110-9

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

J. Rathke and M. Hennessy, Local Model Checking for a Value-Based Modal µcalculus, 1996.

G. Salaün, W. Serwe, Y. Thonnart, and P. Vivet, Formal Verification of CHP Specifications with CADP Illustration on an Asynchronous Network-on-Chip, 13th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'07)
DOI : 10.1109/ASYNC.2007.18

C. Stirling, Modal and Temporal Properties of Processes, 2001.
DOI : 10.1007/978-1-4757-3550-5

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

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=

W. Thomas, Computation tree logic and regular ??-languages
DOI : 10.1007/BFb0013041

B. Vergauwen and J. Lewi, A linear algorithm for solving fixed-point equations on transition systems, CAAP'92, pp.322-341
DOI : 10.1007/3-540-55251-0_18

P. Wolper, A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping. Unpublished manuscript, 1982.

P. Wolper, Temporal logic can be more expressive, 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pp.72-99, 1983.
DOI : 10.1109/SFCS.1981.44

URL : http://doi.org/10.1016/s0019-9958(83)80051-5