Applications of an expressive statistical model checking approach to the analysis of genetic circuits. (English) Zbl 1337.92138

Summary: Stochastic temporal logics have demonstrated their efficiency in the analysis of discrete-state stochastic models. In this paper we consider the application of a recently introduced formalism, namely the hybrid automata stochastic language (HASL), to the analysis of biological models of genetic circuits. In particular we demonstrate the potential of HASL by focusing on two aspects: first the analysis of a genetic oscillator and then the analysis of gene expression. With respect to oscillations, we formalize a number of HASL based measures which we apply on a realistic model of a three-gene repressilator. With respect to gene expression, we consider a model with delayed stochastic dynamics, a class of systems whose dynamics includes both Markovian and non-Markovian events, and we identify a number of relevant and sophisticated measures. To assess the HASL defined measures we employ the COSMOS tool, a statistical model checker designed for HASL model checking.


92D10 Genetics and epigenetics
92C42 Systems biology, networks
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Ajmone Marsan, M.; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with generalized stochastic Petri nets, (1995), John Wiley & Sons · Zbl 0843.68080
[2] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Hybrid Systems, LNCS, vol. 736, (1992))
[3] Alur, R.; Dill, D. L., A theory of timed automata, Theoret. Comput. Sci., 126, 2, (1994) · Zbl 0803.68071
[4] Amparore, E. G.; Ballarini, P.; Beccuti, M.; Donatelli, S.; Franceschinis, G., Expressing and computing passage time measures of GSPN models with HASL, (Colom, J. M.; Desel, J., Petri Nets, Lecture Notes in Computer Science, vol. 7927, (2013), Springer), 110-129 · Zbl 1381.68193
[5] 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)
[6] Aziz, A.; Sanwal, K.; Singhal, V.; Brayton, R., Model-checking ctmcs, ACM Trans. Comput. Log., 1, 1, (2000)
[7] Baier, C.; Cloth, L.; Haverkort, B.; Kuntz, M.; Siegle, M., Model checking action- and state-labelled Markov chains, IEEE Trans. Softw. Eng., 33, 4, (2007)
[8] Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J.-P., Model-checking algorithms for ctmcs, IEEE Trans. Softw. Eng., 29, 6, (2003)
[9] Baier, C.; Katoen, J.-P., Principles of model checking, Representation and Mind Series, (2008), MIT Press
[10] Ballarini, P.; Djafri, H.; Duflot, M.; Haddad, S.; Pekergin, N., COSMOS: a statistical model checker for the hybrid automata stochastic logic, (Proceedings of the 8th International Conference on Quantitative Evaluation of Systems, QEST’11, (Sep. 2011), IEEE Computer Society Press), 143-144
[11] Ballarini, P.; Djafri, H.; Duflot, M.; Haddad, S.; Pekergin, N., HASL: an expressive language for statistical verification of stochastic models, (Proc. Valuetools, (2011))
[12] Ballarini, P.; Guerriero, M., Query-based verification of qualitative trends and oscillations in biochemical systems, Theoret. Comput. Sci., 411, 20, 2019-2036, (2010) · Zbl 1209.68310
[13] Ballarini, P.; Mäkelä, J.; Ribeiro, A. S., Expressive statistical model checking of genetic networks with delayed stochastic dynamics, (CMSB, (2012)), 29-48
[14] Barbuti, R.; Levi, F.; Milazzo, P.; Scatena, G., Probabilistic model checking of biological systems with uncertain kinetic rates, Theoret. Comput. Sci., 419, 2-16, (Feb. 2012) · Zbl 1234.92020
[15] Barrio, M.; Burrage, K.; Leier, A.; Tian, T., Oscillatory regulation of hes1: discrete stochastic delay modelling and simulation, PLoS Comput. Biol., 2, 9, 1017-1030, (2006)
[16] 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, J. Theoret. Biol., 229, 3, 339-347, (Aug. 2004)
[17] Bobbio, A.; Puliafito, A.; Telek, M.; Trivedi, K. S., Recent developments in non-Markovian stochastic Petri nets, J. Circuits Syst. Comput., 8, 1, 119-158, (1998)
[18] 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)
[19] Chen, T.; Han, T.; Katoen, J.-P.; Mereacre, A., Quantitative model checking of CTMC against timed automata specifications, (Proc. LICS’09, (2009))
[20] Cloth, L.; Katoen, J.-P.; Khattri, M.; Pulungan, R., Model checking Markov reward models with impulse rewards, (Proc. International Conference on Dependable Systems and Networks, DSN’05, (2005), IEEE Computer Society Press), 722-731
[21] Cosmos home page
[22] David, A.; Larsen, K. G.; Legay, A.; Mikucionis, M.; Wang, Z., Time for statistical model checking of real-time systems, (Proc. 23rd International Conference on Computer Aided Verification, CAV’11, (2011)), 349-355
[23] David, A.; Larsen, K. G.; Legay, A.; Mikučionis, M.; Poulsen, D. B.; Sedwards, S., Runtime verification of biological systems, (Proceedings of the 5th International Conference on Leveraging Applications of Formal Methods, Verification and Validation: Technologies for Mastering Change, Part I, ISoLA’12, (2012), Springer-Verlag Berlin, Heidelberg), 388-404
[24] David, A.; Larsen, K. G.; Legay, A.; Mikučionis, M.; Poulsen, D. B.; Van Vliet, J.; Wang, Z., Statistical model checking for networks of priced timed automata, (Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’11, (2011), Springer-Verlag Berlin, Heidelberg), 80-96 · Zbl 1348.68130
[25] Donatelli, S.; Haddad, S.; Sproston, J., Model checking timed and stochastic properties with \(\mathit{CSL}^{\mathit{TA}}\), IEEE Trans. Softw. Eng., 35, (2009)
[26] Eickhoff, M.; McNickle, D.; Pawlikowski, K., Detecting the duration of initial transient in steady state simulation of arbitrary performance measures, (Proceedings of the 2nd International Conference on Performance Evaluation Methodologies and Tools, ValueTools ’07, (2007), ICST Brussels, Belgium), 42:1-42:7, ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering)
[27] Elowitz, M.; Leibler, S., A synthetic oscillatory network of transcriptional regulators, Nature, 403, 335, (2000)
[28] Fages, F.; Soliman, S.; Rivier, C. N., Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM, J. Biol. Phys. Chem., 4, 2, 64-73, (2004)
[29] Finkbeiner, B.; Sipma, H., Checking finite traces using alternating automata, Form. Methods Syst. Des., 24, 2, 101-127, (2004) · Zbl 1073.68053
[30] Gillespie, D., Exact stochastic simulation of coupled chemical reactions, J. Phys. Chem., 81, 25, 2340-2361, (1977)
[31] Glynn, P. W., A GSMP formalism for discrete event systems, Proc. I.E.E.E., 77, 14-23, (1989)
[32] Gorrieri, R.; Herzog, U.; Hillston, J., Unified specification and performance evaluation using stochastic process algebras, Perform. Eval., 50, 2/3, 79-82, (2002) · Zbl 1159.68516
[33] Haverkort, B.; Cloth, L.; Hermanns, H.; Katoen, J.-P.; Baier, C., Model checking performability properties, (Proc. DSN’02, (2002))
[34] He, R.; Jennings, P.; Basu, S.; Ghosh, A. P.; Wu, H., A bounded statistical approach for model checking of unbounded until properties, (Proc. ASE’10, (2010))
[35] Heath, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Tymchyshyn, O., Probabilistic model checking of complex biological pathways, Theoret. Comput. Sci., 319, 3, 239-257, (2008) · Zbl 1133.68043
[36] Jégourel, C.; Legay, A.; Sedwards, S., 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, (2012)), 498-503 · Zbl 1352.68156
[37] Júlvez, J.; Kwiatkowska, M.; Norman, G.; Parker, D., Evaluation of sustained stochastic oscillations by means of a system of differential equations, Int. J. Comput. Appl., 19, 2, 101-111, (2012)
[38] Kandhavelu, M.; Hakkinen, A.; Yli-Harja, O.; Ribeiro, A. S., Single-molecule dynamics of transcription of the lar promoter, Physical Biology, 9, 2, (2012)
[39] Kitano, H., Foundations of systems biology, (2002), MIT Press
[40] Knuth, D. E., The art of computer programming, vol. 2: seminumerical algorithms, (1997), Addison-Wesley Longman Publishing Co., Inc. Boston, MA, USA · Zbl 0895.65001
[41] Kwiatkowska, M.; Norman, G.; Parker, D., Stochastic model checking, (Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, LNCS, vol. 4486, (2007), Springer), 220-270 · Zbl 1323.68379
[42] Kwiatkowska, M.; Norman, G.; Parker, D., Prism 4.0: verification of probabilistic real-time systems, (Proc. 23rd International Conference on Computer Aided Verification, CAV’11, (2011)), 585-591
[43] Lakin, M.; Parker, D.; Cardelli, L.; Kwiatkowska, M.; Phillips, A., Design and analysis of DNA strand displacement devices using probabilistic model checking, J. R. Soc. Interface, 9, 72, 1470-1485, (2012)
[44] Makela, J.; Lloyd-Price, J.; Yli-Harja, O.; Ribeiro, A., Stochastic sequence-level model of coupled transcription and translation in prokaryotes, BMC Bioinformatics, 12, 1, 121, (2011)
[45] Megerle, J.; Fritz, G.; Gerland, U.; Jung, K.; Rädler, J., Timing and dynamics of single cell gene expression in the arabinose utilization system, Biophys. J., 95, 2103-2115, (2008)
[46] Ribeiro, A.; Zhu, R.; Kauffman, S. A., A general modeling strategy for gene regulatory networks with stochastic dynamics, J. Comput. Biol., 13, 9, 1630-1639, (Nov. 2006)
[47] Ribeiro, A.; Zhu, R.; Kauffman, S. A., A general modeling strategy for gene regulatory networks with stochastic dynamics, J. Comput. Biol., 13, 9, 1630-1639, (2006)
[48] Ribeiro, A. S.; Lloyd-Price, J., SGN sim, a stochastic genetic networks simulator, Bioinformatics (Oxford, England), 23, 6, 777-779, (Mar. 2007)
[49] Ross, S. M., Simulation, (2002), Academic Press, Elsevier
[50] 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)
[51] Sen, K.; Viswanathan, M.; Agha, G., VESTA: a statistical model-checker and analyzer for probabilistic systems, (Proc. QEST’05, (2005))
[52] Spieler, D., Model checking of oscillatory and noisy periodic behavior in Markovian population models, (2009), Saarland University, Master’s thesis
[53] Spieler, D., Characterizing oscillatory and noisy periodic behavior in Markov population models, (Proc. QEST’13, (2013))
[54] Stewart, W., Introduction to the numerical solution of Markov chains, (1994), Princeton Univ. Press Princeton, NJ
[55] Szallasi, Z.; Stelling, J.; Periwal, V., System modeling in cellular biology: from concepts to nuts and bolts, Bradford Books, (2010), Mit Press · Zbl 1274.92012
[56] Taniguchi, Y.; Choi, P. J.; Li, G.-W.; Chen, H.; Babu, M.; Hearn, J.; Emili, A.; Xie, X., Quantifying E. coli proteome and transcriptome with single-molecule sensitivity in single cells, Science, 329, 5991, 533-538, (July 2010)
[57] Uppaal-SMC home page
[58] Younes, H., Ymer: a statistical model checker, (Proc. CAV’05, LNCS, vol. 3576, (2005)) · Zbl 1081.68642
[59] Zhu, R.; Ribeiro, A.; Salahub, D.; Kauffman, S., Studying genetic regulatory networks at the molecular level: delayed reaction stochastic models, J. Theoret. Biol., 246, 4, 725-745, (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.