Expressive Statistical Model Checking of Genetic Networks with Delayed Stochastic Dynamics

1. Cosmos home page, http://www.lsv.ens-cachan.fr/software/cosmos/

2. Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)

   Google Scholar 

3. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)

   Chapter  Google Scholar 

4. Arkin, A.P., Ross, J., McAdams, H.H.: Stochastic Kinetic Analysis of a Developmental Pathway Bifurcation in Phage-l Escherichia coli. Genetics 149(4), 1633–1648 (1998)

   Google Scholar 

5. Baier, C., Cloth, L., Haverkort, B., Kuntz, M., Siegle, M.: Model checking action- and state-labelled Markov chains. IEEE Trans. on Software Eng. 33(4) (2007)

   Google Scholar 

6. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for CTMCs. IEEE Trans. on Software Eng. 29(6) (2003)

   Google Scholar 

7. Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST 2011), pp. 143–144. IEEE Computer Society Press (September 2011)

   Google Scholar 

8. Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Proc. Valuetools (2011)

   Google Scholar 

9. Ballarini, P., Guerriero, M.L.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theoretical Computer Science 411(20), 2019–2036 (2010)

   Article  MathSciNet  MATH  Google Scholar 

10. Barnat, J., Brim, L., Cerná, I., Drazan, S., Fabriková, J., Láník, J., Safránek, D., Ma, H.: Biodivine: A framework for parallel analysis of biological models. In: COMPMOD. EPTCS, vol. 6, pp. 31–45 (2009)

    Google Scholar 

11. Barrio, M., Burrage, K., Leier, A., Tian, T.: Oscillatory regulation of hes1: Discrete stochastic delay modelling and simulation. PLoS Computational Biology 2(9), 1017–1030 (2006)

    Article  Google Scholar 

12. Bernot, G., Comet, J.-P., Richard, A., Guespin, J.: Application of formal methods to biological regulatory networks: extending Thomas’ asynchronous logical approach with temporal logic. Journal of Theoretical Biology 229(3), 339–347 (2004)

    Article  MathSciNet  Google Scholar 

13. Bratsun, D., Volfson, D., Tsimring, L.S., Hasty, J.: Delay-induced stochastic oscillations in gene regulation. Proc. Natl. Acad. Sci. USA. 102(41), 14593–14598 (2005)

    Article  Google Scholar 

14. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of CTMC against timed automata specifications. In: Proc. LICS 2009 (2009)

    Google Scholar 

15. De Jong, H., Geiselmann, J., Hernandez, C., Page, M.: Genetic network analyzer: qualitative simulation of genetic regulatory networks. Bioinformatics 19(3), 244–336 (2003)

    Google Scholar 

16. Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL^TA. IEEE Trans. on Software Eng. 35 (2009)

    Google Scholar 

17. Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

18. Fages, F., Soliman, S.: Formal Cell Biology in Biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 54–80. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

19. Fages, F., Soliman, S., Rivier, C.N.: Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry 4(2), 64–73 (2004)

    Article  Google Scholar 

20. Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry 81(25), 2340–2361 (1977)

    Article  Google Scholar 

21. Hansson, H.A., Jonsson, B.: A framework for reasoning about time and reliability. In: Proc. 10th IEEE Real -Time Systems Symposium, Santa Monica, Ca, pp. 102–111. IEEE Computer Society Press (1989)

    Google Scholar 

22. Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.: Model checking performability properties. In: Proc. DSN 2002 (2002)

    Google Scholar 

23. Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theoretical Computer Science 319(3), 239–257 (2008)

    Article  MathSciNet  Google Scholar 

24. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian Approach to Model Checking Biological Systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

25. Kandhavelu, M., Hakkinen, A., Yli-Harja, O., Ribeiro, A.S.: Single-molecule dynamics of transcription of the lar promoter. Phys. Biol. 9(2) (2012)

    Google Scholar 

26. Kitano, H.: Foundations of Systems Biology. MIT Press (2002)

    Google Scholar 

27. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

28. Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface (to appear, 2011)

    Google Scholar 

29. Makela, J., Lloyd-Price, J., Yli-Harja, O., Ribeiro, A.S.: Stochastic sequence-level model of coupled transcription and translation in prokaryotes. BMC Bioinformatics 12(1), 121 (2011)

    Article  Google Scholar 

30. Megerle, J.A., Fritz, G., Gerland, U., Jung, K., Rädler, J.O.: Timing and Dynamics of Single Cell Gene Expression in the Arabinose Utilization System. Biophysical Journal 95, 2103–2115 (2008)

    Article  Google Scholar 

31. Prism home page, http://www.prismmodelchecker.org

32. Ribeiro, A., Zhu, R., Kauffman, S.A.: A general modeling strategy for gene regulatory networks with stochastic dynamics. Journal of Computational Biology: a Journal of Computational Molecular Cell Biology 13(9), 1630–1639 (2006)

    Article  MathSciNet  Google Scholar 

33. Ribeiro, A.S., Lloyd-Price, J.: SGN Sim, a stochastic genetic networks simulator. Bioinformatics 23(6), 777–779 (2007)

    Article  Google Scholar 

34. Roussel, M.R., Zhu, R.: Validation of an algorithm for delay stochastic simulation of transcription and translation in prokaryotic gene expression. Physical Biology 3(4), 274–284 (2006)

    Article  Google Scholar 

35. Schwarick, M., Rohr, C., Heiner, M.: Marcie - model checking and reachability analysis done efficiently. In: Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), pp. 91–100. IEEE CS Press (2011)

    Google Scholar 

36. Spieler, D.: Model checking of oscillatory and noisy periodic behavior in markovian population models. Master’s thesis, Saarland University (2009)

    Google Scholar 

37. Taniguchi, Y., Choi, P.J., Li, G.-W., Chen, H., Babu, M., Hearn, J., Emili, A., Xie, X.S.: Quantifying E. coli Proteome and Transcriptome with Single-Molecule Sensitivity in Single Cells. Science 329(5991), 533–538 (2010)

    Article  Google Scholar 

38. Zhu, R., Ribeiro, A.S., Salahub, D., Kauffman, S.A.: Studying genetic regulatory networks at the molecular level: Delayed reaction stochastic models. Journal of Theoretical Biology 246(4), 725–745 (2007)

    Article  MathSciNet  Google Scholar 

Download references