M. A. Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modelling with Generalized Stochastic Petri Nets, ACM SIGMETRICS Performance Evaluation Review, vol.26, issue.2, 1995.
DOI : 10.1145/288197.581193

R. Alur, C. Courcoubetis, T. A. Henzinger, and P. Ho, Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, Hybrid Systems, 1992.
DOI : 10.1007/3-540-57318-6_30

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, 1994.

E. G. Amparore, P. Ballarini, M. Beccuti, S. Donatelli, and G. Franceschinis, Expressing and Computing Passage Time Measures of GSPN Models with HASL, Petri Nets, pp.110-129, 2013.
DOI : 10.1007/978-3-642-38697-8_7

URL : https://hal.archives-ouvertes.fr/hal-00848708

A. P. Arkin, J. Ross, and H. H. Mcadams, Stochastic Kinetic Analysis of a Developmental Pathway Bifurcation in Phage-l Escherichia coli, Genetics, vol.149, issue.4, pp.1633-1648, 1998.

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Model-checking CTMCs, ACM Trans. on Computational Logic, vol.1, issue.1, 2000.

C. Baier, L. Cloth, B. Haverkort, M. Kuntz, and M. Siegle, Model checking action- and state-labelled Markov chains, International Conference on Dependable Systems and Networks, 2004, 2007.
DOI : 10.1109/DSN.2004.1311941

C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, Model-checking algorithms for CTMCs, IEEE Trans. on Software Eng, vol.29, issue.6, 2003.

C. Baier and J. Katoen, Principles of Model Checking (Representation and Mind Series), 2008.

P. Ballarini, H. Djafri, M. Duflot, S. Haddad, and N. Pekergin, COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic, 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp.143-144, 2011.
DOI : 10.1109/QEST.2011.24

P. Ballarini, H. Djafri, M. Duflot, S. Haddad, and N. Pekergin, HASL: an Expressive Language for Statistical Verification of Stochastic Models, Proceedings of the 5th International ICST Conference on Performance Evaluation Methodologies and Tools, 2011.
DOI : 10.4108/icst.valuetools.2011.245710

URL : https://hal.archives-ouvertes.fr/hal-01113442

P. Ballarini and M. Guerriero, Query-based verification of qualitative trends and oscillations in biochemical systems, Theoretical Computer Science, vol.411, issue.20, pp.2019-2036, 2010.
DOI : 10.1016/j.tcs.2010.02.010

P. Ballarini, J. Mäkelä, and A. S. Ribeiro, Expressive Statistical Model Checking of Genetic Networks with Delayed Stochastic Dynamics, CMSB, pp.29-48, 2012.
DOI : 10.1007/978-3-642-33636-2_4

URL : https://hal.archives-ouvertes.fr/hal-00832096

R. Barbuti, F. Levi, P. Milazzo, and G. Scatena, Probabilistic model checking of biological systems with uncertain kinetic rates, Theoretical Computer Science, vol.419, pp.2-16, 2012.
DOI : 10.1016/j.tcs.2011.10.022

M. Barrio, K. Burrage, A. Leier, and T. Tian, Oscillatory regulation of hes1: Discrete stochastic delay modelling and simulation, PLoS Computational Biology, vol.2, issue.9, pp.1017-1030, 2006.

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-347, 2004.
DOI : 10.1016/j.jtbi.2004.04.003

A. Bobbio, A. Puliafito, M. Telek, and K. S. Trivedi, RECENT DEVELOPMENTS IN NON-MARKOVIAN STOCHASTIC PETRI NETS, Journal of Circuits, Systems and Computers, vol.08, issue.01, pp.119-158, 1998.
DOI : 10.1142/S0218126698000067

D. Bratsun, D. Volfson, L. S. Tsimring, and J. Hasty, Delay-induced stochastic oscillations in gene regulation, Proceedings of the National Academy of Sciences, vol.102, issue.41, pp.14593-14601, 2005.
DOI : 10.1073/pnas.0503858102

T. Chen, T. Han, J. Katoen, and A. Mereacre, Quantitative model checking of CTMC against timed automata specifications, Proc. LICS'09, 2009.

L. Cloth, J. Katoen, M. Khattri, and R. Pulungan, Model Checking Markov Reward Models with Impulse Rewards, 2005 International Conference on Dependable Systems and Networks (DSN'05), pp.722-731, 2005.
DOI : 10.1109/DSN.2005.64

A. David, K. G. Larsen, A. Legay, M. Mikucionis, and Z. Wang, Time for Statistical Model Checking of Real-Time Systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.349-355, 2011.
DOI : 10.1007/s10009-005-0187-8

A. David, K. G. Larsen, A. Legay, M. Miku?ionis, D. B. Poulsen et al., Runtime verification of biological systems Verification and Validation: technologies for mastering change -Volume Part I, ISoLA'12, Proceedings of the 5th international conference on Leveraging Applications of Formal Methods, pp.388-404, 2012.

A. David, K. G. Larsen, A. Legay, M. Miku?ionis, D. B. Poulsen et al., Statistical Model Checking for Networks of Priced Timed Automata, Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, pp.80-96, 2011.
DOI : 10.1145/1755952.1755987

S. Donatelli, S. Haddad, and J. Sproston, Model Checking Timed and Stochastic Properties with CSL^{TA}, IEEE Transactions on Software Engineering, vol.35, issue.2, 2009.
DOI : 10.1109/TSE.2008.108

M. Eickhoff, D. Mcnickle, and K. Pawlikowski, DETECTING THE DURATION OF INITIAL TRANSIENT IN STEADY STATE SIMULATION OF ARBITRARY PERFORMANCE MEASURES, Proceedings of the 2nd International ICST Conference on Performance Evaluation Methodologies and Tools, pp.1-42, 2007.
DOI : 10.4108/valuetools.2007.1937

M. Elowitz and S. Leibler, A synthetic oscillatory network of transcriptional regulators, Nature, issue.335, p.403, 2000.

F. Fages, S. Soliman, and C. N. Rivier, Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM, Journal of Biological Physics and Chemistry, vol.4, issue.2, pp.64-73, 2004.
DOI : 10.4024/2040402.jbpc.04.02

URL : https://hal.archives-ouvertes.fr/hal-01431345

B. Finkbeiner and H. Sipma, Checking finite traces using alternating automata . Formal Methods in System Design, pp.101-127, 2004.

D. Gillespie, Exact stochastic simulation of coupled chemical reactions, The Journal of Physical Chemistry, vol.81, issue.25, pp.2340-2361, 1977.
DOI : 10.1021/j100540a008

P. W. Glynn, A GSMP formalism for discrete event systems, Proceedings of the IEEE, vol.77, issue.1, 1989.
DOI : 10.1109/5.21067

R. Gorrieri, U. Herzog, and J. Hillston, Unified specification and performance evaluation using stochastic process algebras, Performance Evaluation, vol.50, issue.2-3, pp.79-82, 2002.
DOI : 10.1016/S0166-5316(02)00100-1

B. Haverkort, L. Cloth, H. Hermanns, J. Katoen, and C. Baier, Model checking performability properties, Proceedings International Conference on Dependable Systems and Networks, 2002.
DOI : 10.1109/DSN.2002.1028891

R. He, P. Jennings, S. Basu, A. P. Ghosh, and H. Wu, A bounded statistical approach for model checking of unbounded until properties, Proceedings of the IEEE/ACM international conference on Automated software engineering, ASE '10, 2010.
DOI : 10.1145/1858996.1859043

J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, Probabilistic model checking of complex biological pathways, Theoretical Computer Science, vol.319, issue.3, pp.239-257, 2008.

C. Jégourel, A. Legay, and S. Sedwards, A Platform for High Performance Statistical Model Checking ??? PLASMA, Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), pp.498-503, 2012.
DOI : 10.1007/978-3-642-28756-5_37

J. Júlvez, M. Kwiatkowska, G. Norman, and D. Parker, Evaluation of sustained stochastic oscillations by means of a system of differential equations, International Journal of Computers and Applications (IJCA), vol.19, issue.2, pp.101-111, 2012.

M. Kandhavelu, A. Hakkinen, O. Yli-harja, and A. S. Ribeiro, Singlemolecule dynamics of transcription of the lar promoter, Phys Biol, vol.9, issue.2, p.2012

H. Kitano, Foundations of Systems Biology, 2002.

D. E. Knuth, The Art of Computer Programming): Seminumerical Algorithms, 1997.

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic model checking In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, LNCS, vol.4486, pp.220-270, 2007.

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17

URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Lakin, D. Parker, L. Cardelli, M. Kwiatkowska, and A. Phillips, Design and analysis of DNA strand displacement devices using probabilistic model checking, Journal of The Royal Society Interface, vol.43, issue.12, 2011.
DOI : 10.1073/pnas.95.12.6750

J. Makela, J. Lloyd-price, O. Yli-harja, and A. Ribeiro, Stochastic sequence-level model of coupled transcription and translation in prokaryotes, BMC Bioinformatics, vol.12, issue.1, p.121, 2011.
DOI : 10.1146/annurev.micro.62.081307.162948

J. Megerle, G. Fritz, U. Gerland, K. Jung, and J. Rädler, Timing and Dynamics of Single Cell Gene Expression in the Arabinose Utilization System, Biophysical Journal, vol.95, issue.4, pp.2103-2115, 2008.
DOI : 10.1529/biophysj.107.127191

A. Ribeiro, R. Zhu, and S. A. Kauffman, A General Modeling Strategy for Gene Regulatory Networks with Stochastic Dynamics, Journal of Computational Biology, vol.13, issue.9, pp.1630-1639, 2006.
DOI : 10.1089/cmb.2006.13.1630

A. Ribeiro, R. Zhu, and S. A. Kauffman, A General Modeling Strategy for Gene Regulatory Networks with Stochastic Dynamics, Journal of Computational Biology, vol.13, issue.9, pp.1630-1639, 2006.
DOI : 10.1089/cmb.2006.13.1630

A. S. Ribeiro and J. Lloyd-price, SGN Sim, a Stochastic Genetic Networks Simulator, Bioinformatics, vol.23, issue.6, pp.777-779, 2007.
DOI : 10.1093/bioinformatics/btm004

S. M. Ross, Simulation, 2002.

M. R. Roussel and R. Zhu, Validation of an algorithm for delay stochastic simulation of transcription and translation in prokaryotic gene expression, Physical Biology, vol.3, issue.4, pp.274-284, 2006.
DOI : 10.1088/1478-3975/3/4/005

K. Sen, M. Viswanathan, and G. Agha, VESTA: A statistical model-checker and analyzer for probabilistic systems, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), 2005.
DOI : 10.1109/QEST.2005.42

D. Spieler, Model checking of oscillatory and noisy periodic behavior in Markovian population models, 2009.

D. Spieler, Characterizing Oscillatory and Noisy Periodic Behavior in Markov Population Models, Proc. QEST'13, 2013.
DOI : 10.1007/978-3-642-40196-1_8

W. Stewart, Introduction to the numerical solution of Markov chains, 1994.

Z. Szallasi, J. Stelling, and V. Periwal, System Modeling in Cellular Biology: From Concepts to Nuts and Bolts. A Bradford book, 2010.
DOI : 10.7551/mitpress/9780262195485.001.0001

H. Younes, Ymer: A Statistical Model Checker, Proc. CAV'05, 2005.
DOI : 10.1007/11513988_43

R. Zhu, A. Ribeiro, D. Salahub, and S. Kauffman, Studying genetic regulatory networks at the molecular level: Delayed reaction stochastic models, Journal of Theoretical Biology, vol.246, issue.4, pp.725-745, 2007.
DOI : 10.1016/j.jtbi.2007.01.021