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

M. Antoniotti, A. Policriti, N. Ugel, and B. Mishra, Model Building and Model Checking for Biochemical Processes, Cell Biochemistry and Biophysics, vol.38, issue.3, pp.271-286, 2003.
DOI : 10.1385/CBB:38:3:271

R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg et al., The ForSpec Temporal Logic: A New Temporal Property-Specification Language, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'02, pp.296-211, 2002.
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.2-3205, 2004.
DOI : 10.1016/0304-3975(82)90125-6

J. Barnat, L. Brim, I. Cerná, S. Drazan, and D. Safranek, Parallel model checking largescale genetic regulatory networks with DiVinE, From Biology to Concurrency and Back, 2007.

H. Barringer, A. Goldberg, K. Havelund, and K. Sen, Rule-Based Runtime Verification, Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'04, pp.44-57, 2004.
DOI : 10.1007/978-3-540-24622-0_5

G. Batt, D. Bergamini, H. De-jong, H. Gavarel, and R. Mateescu, Model Checking Genetic Regulatory Networks Using GNA and CADP, Eleventh International SPIN Workshop on Model Checking of Software, pp.158-163, 2004.
DOI : 10.1007/978-3-540-24732-6_12

G. Batt, H. De-jong, M. Page, and J. Geiselmann, Symbolic reachability analysis of genetic regulatory networks using discrete abstractions, Automatica, vol.44, issue.4, pp.982-989, 2008.
DOI : 10.1016/j.automatica.2007.08.004
URL : https://hal.archives-ouvertes.fr/hal-00319485

G. Batt, D. Ropers, H. De-jong, J. Geiselmann, R. Mateescu et al., Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli, Bioinformatics, vol.21, issue.Suppl 1, pp.19-28, 2005.
DOI : 10.1093/bioinformatics/bti1048
URL : https://hal.archives-ouvertes.fr/hal-00171939

I. Beer, S. Ben-david, C. Eisner, D. Fisman, A. Gringauze et al., The Temporal Logic Sugar, Proceedings of the 13th International Conference on Computer Aided Verification CAV, pp.363-367, 2001.
DOI : 10.1007/3-540-44585-4_33

I. Beer, S. Ben-david, and A. Landver, On-the-fly model checking of RCTL formulas, Proceedings of the 10th International Conference on Computer Aided Verification CAV'98, pp.184-194, 1998.
DOI : 10.1007/BFb0028744

G. Bernot, J. Comet, A. Richard, and J. Guespin, Application of formal methods to biological regulatory networks: extending Thomas??? asynchronous logical approach with temporal logic, Journal of Theoretical Biology, vol.229, issue.3, pp.339-348, 2004.
DOI : 10.1016/j.jtbi.2004.04.003

T. Brázdil and I. Cerná, Model checking of RegCTL, Computers and Artificial Intelligence, vol.25, issue.1, 2006.

J. A. Brzozowski, Derivatives of Regular Expressions, Journal of the ACM, vol.11, issue.4, pp.481-494, 1964.
DOI : 10.1145/321239.321249

M. Calder, V. Vyshemirsky, D. Gilbert, and R. Orton, Analysis of signalling pathways using the PRISM model checker, Computational Methods in Systems Biology, CMSB-05, pp.79-90, 2005.

N. Chabrier-rivier, M. Chiaverini, V. Danos, F. Fages, and V. Schächter, Modeling and querying biomolecular interaction networks, Theoretical Computer Science, vol.325, issue.1, pp.25-44, 2004.
DOI : 10.1016/j.tcs.2004.03.063

C. Chaouiya, Petri net modelling of biological networks, Briefings in Bioinformatics, vol.8, issue.4, pp.210-219, 2007.
DOI : 10.1093/bib/bbm029

K. C. Chen, L. Calzone, A. Csikasz-nagy, F. R. Cross, B. Novak et al., Integrative Analysis of Cell Cycle Control in Budding Yeast, Molecular Biology of the Cell, vol.15, issue.8, pp.3841-3862, 2004.
DOI : 10.1091/mbc.E03-11-0794

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer (STTT), pp.410-425, 2000.
DOI : 10.1007/s100090050046

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. Formal Methods in System Design, pp.121-147, 1993.

H. De and J. , Modeling and simulation of genetic regulatory systems: A literature review, Journal of Computational Biology, vol.9, issue.1, pp.67-103, 2002.

H. De-jong, J. Gouzé, C. Hernandez, M. Page, T. Sari et al., Qualitative simulation of genetic regulatory networks using piecewise-linear models, Bulletin of Mathematical Biology, vol.66, issue.2, pp.301-340, 2004.
DOI : 10.1016/j.bulm.2003.08.010
URL : https://hal.archives-ouvertes.fr/hal-00173849

D. Dubnau and R. Losick, Bistability in bacteria, Molecular Microbiology, vol.196, issue.3, pp.564-572, 2006.
DOI : 10.1111/j.1365-2958.2005.04659.x

E. A. Emerson and J. Y. Halpern, "Sometimes" and "not never" revisited, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.127-140151, 1983.
DOI : 10.1145/567067.567081

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.

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

J. Fisher and T. A. Henzinger, Executable cell biology, Nature Biotechnology, vol.2034, issue.11, pp.1239-1250, 2007.
DOI : 10.1038/nbt1356

J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development, PLoS Computational Biology, vol.77, issue.5, p.92, 2007.
DOI : 0016-6731(1974)077[0071:TGOCE]2.0.CO;2

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, and R. Mateescu, Compiler Construction Using LOTOS NT, Proceedings of the 11th International Conference on Compiler Construction CC'2002, pp.9-13, 2002.
DOI : 10.1007/3-540-45937-5_3

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 M. Sighireanu, Towards a second generation of formal description techniques ? rationale for the design of E-LOTOS, Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems FMICS'98, pp.187-230, 1998.

L. Glass and S. A. Kauffman, The logical analysis of continuous, non-linear biochemical control networks, Journal of Theoretical Biology, vol.39, issue.1, pp.103-129, 1973.
DOI : 10.1016/0022-5193(73)90208-7

K. Hamaguchi, H. Hiraishi, and S. Yajima, Branching time regular temporal logic for model checking with linear time complexity, Proceedings of the 2nd International Conference on Computer Aided Verification CAV'90, pp.253-262, 1990.
DOI : 10.1007/BFb0023739

G. Holzmann, The SPIN Model Checker ? Primer and Reference Manual, 2003.

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.

C. Joubert and R. Mateescu, Distributed Local Resolution of Boolean Equation Systems, 13th Euromicro Conference on Parallel, Distributed and Network-Based Processing, 2005.
DOI : 10.1109/EMPDP.2005.19
URL : https://hal.archives-ouvertes.fr/hal-00683892

C. Joubert and R. Mateescu, Distributed On-the-Fly Model Checking and Test Case Generation, Proceedings of the 13th International SPIN Workshop on Model Checking of Software SPIN'2006, pp.126-145, 2006.
DOI : 10.1007/BFb0054166
URL : https://hal.archives-ouvertes.fr/inria-00071388

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

E. Klipp, B. Nordlander, R. Krüger, P. Gennemark, and S. Hohmann, Integrative model of the response of yeast to osmotic shock, Nature Biotechnology, vol.53, issue.8, pp.975-982, 2005.
DOI : 10.1016/0006-3002(58)90330-5

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

F. Lang and . Exp, OPEN 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods, Proceedings of the 5th International Conference on Integrated Formal Methods IFM'2005, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070339

K. G. Larsen, Proof systems for Hennessy-Milner Logic with recursion, Proceedings of the 13th Colloquium on Trees in Algebra and Programming CAAP'88, pp.215-230, 1988.
DOI : 10.1007/BFb0026106

J. Leloup and A. Goldbeter, Toward a detailed computational model for the mammalian circadian clock, Proceedings of the National Academy of Sciences of the USA, pp.7051-7056, 2003.
DOI : 10.1073/pnas.1132112100

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, volume I: Specification, 1992.

A. J. Martin, Compiling communicating processes into delay-insensitive VLSI circuits, Distributed Computing, pp.226-234, 1986.
DOI : 10.1007/BF01660034

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. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, Proceedings of the 15th International Symposium on Formal Methods FM'08, 2008.
DOI : 10.1007/978-3-540-68237-0_12
URL : https://hal.archives-ouvertes.fr/inria-00315312

P. T. Monteiro, D. Ropers, R. Mateescu, A. T. Freitas, H. De et al., Temporal logic patterns for querying dynamic models of cellular interaction networks, Bioinformatics, vol.24, issue.16, 2008.
DOI : 10.1093/bioinformatics/btn275
URL : https://hal.archives-ouvertes.fr/inria-00357805

A. Regev and E. Shapiro, Cells as Computation, Nature, vol.419, issue.6905, p.343, 2002.
DOI : 10.1007/3-540-36481-1_1

D. Ropers, H. De-jong, M. Page, D. Schneider, and J. Geiselmann, Qualitative simulation of the carbon starvation response in Escherichia coli, Biosystems, vol.84, issue.2, pp.124-152, 2006.
DOI : 10.1016/j.biosystems.2005.10.005
URL : https://hal.archives-ouvertes.fr/hal-00171698

B. Schoeberl, C. Eichler-jonsson, E. Gilles, and G. Mller, Computational modeling of the dynamics of the MAP kinase cascade activated by surface and internalized EGF receptors, Nature Biotechnology, vol.20, issue.4, pp.370-375, 2002.
DOI : 10.1038/nbt0402-370

R. Streett, Propositional dynamic logic of looping and converse. Information and Control, 1982.

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

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.