Modelling with Generalized Stochastic Petri Nets, ACM SIGMETRICS Performance Evaluation Review, vol.26, issue.2, 1995. ,
DOI : 10.1145/288197.581193
Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, Hybrid Systems, 1992. ,
DOI : 10.1007/3-540-57318-6_30
A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, 1994. ,
DOI : 10.1016/0304-3975(94)90010-8
URL : https://doi.org/10.1016/0304-3975(94)90010-8
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
Stochastic Kinetic Analysis of a Developmental Pathway Bifurcation in Phage-l Escherichia coli, Genetics, vol.149, issue.4, pp.1633-1648, 1998. ,
Model-checking CTMCs, ACM Trans. on Computational Logic, vol.1, issue.1, 2000. ,
Model checking action- and state-labelled Markov chains, International Conference on Dependable Systems and Networks, 2004, 2007. ,
DOI : 10.1109/DSN.2004.1311941
URL : http://www.inf.tu-dresden.de/content/institutes/thi/algi/publikationen/texte/03_00.pdf
Model-checking algorithms for CTMCs, IEEE Trans. on Software Eng, vol.29, issue.6, 2003. ,
Principles of Model Checking (Representation and Mind Series), 2008. ,
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
URL : http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf
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
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
URL : https://doi.org/10.1016/j.tcs.2010.02.010
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
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
URL : https://doi.org/10.1016/j.tcs.2011.10.022
Oscillatory regulation of hes1: Discrete stochastic delay modelling and simulation, PLoS Computational Biology, vol.2, issue.9, pp.1017-1030, 2006. ,
DOI : 10.1371/journal.pcbi.0020117.eor
URL : http://journals.plos.org/ploscompbiol/article/file?id=10.1371/journal.pcbi.0020117&type=printable
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
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
Delay-induced stochastic oscillations in gene regulation, Proceedings of the National Academy of Sciences, vol.84, issue.5, pp.14593-14601, 2005. ,
DOI : 10.1016/S0006-3495(03)70013-7
URL : http://www.pnas.org/content/102/41/14593.full.pdf
Quantitative model checking of CTMC against timed automata specifications, Proc. LICS'09, 2009. ,
DOI : 10.1109/lics.2009.21
URL : https://ris.utwente.nl/ws/files/5322989/tinting.pdf
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
,
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
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. ,
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
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
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
A synthetic oscillatory network of transcriptional regulators, Nature, vol.81, issue.6767, p.403, 2000. ,
DOI : 10.1021/j100540a008
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
Checking finite traces using alternating automata . Formal Methods in System Design, pp.101-127, 2004. ,
Exact stochastic simulation of coupled chemical reactions, The Journal of Physical Chemistry, vol.81, issue.25, pp.2340-2361, 1977. ,
DOI : 10.1021/j100540a008
A GSMP formalism for discrete event systems, Proceedings of the IEEE, vol.77, issue.1, 1989. ,
DOI : 10.1109/5.21067
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
Model checking performability properties, Proceedings International Conference on Dependable Systems and Networks, 2002. ,
DOI : 10.1109/DSN.2002.1028891
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
Probabilistic model checking of complex biological pathways, Theoretical Computer Science, vol.319, issue.3, pp.239-257, 2008. ,
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
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. ,
Singlemolecule dynamics of transcription of the lar promoter, Phys Biol, vol.9, issue.2, p.2012 ,
Foundations of Systems Biology, 2002. ,
The Art of Computer Programming): Seminumerical Algorithms, 1997. ,
Stochastic model checking In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, LNCS, vol.4486, pp.220-270, 2007. ,
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
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.1093/comjnl/43.3.224
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
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 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 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
SGN Sim, a Stochastic Genetic Networks Simulator, Bioinformatics, vol.13, issue.5743, pp.777-779, 2007. ,
DOI : 10.1089/cmb.2006.13.1630
Simulation, 2002. ,
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
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
Model checking of oscillatory and noisy periodic behavior in Markovian population models, 2009. ,
Characterizing Oscillatory and Noisy Periodic Behavior in Markov Population Models, Proc. QEST'13, 2013. ,
DOI : 10.1007/978-3-642-40196-1_8
Introduction to the numerical solution of Markov chains, 1994. ,
System Modeling in Cellular Biology: From Concepts to Nuts and Bolts. A Bradford book, 2010. ,
DOI : 10.7551/mitpress/9780262195485.001.0001
, Quantifying E. coli Proteome and Transcriptome with Single- Molecule Sensitivity in Single Cells, pp.329533-538, 2010.
, Uppaal-smc home page
Ymer: A Statistical Model Checker, Proc. CAV'05, 2005. ,
DOI : 10.1007/11513988_43
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
Appendix We present in this appendix further details on the experiments using the HASL based approach to analyze stochastic oscillators In Section A.1 we report on the analysis of the period duration and period fluctuation of a simple model of probabilistic square wave oscillator, Section A.2 we give details on how to reproduce the experiments on the repressilator model ,