We propose a new framework for rigorous robustness analysis of stochastic biochemical systems that is based on probabilistic model checking techniques. We adapt the general definition of robustness introduced by Kitano to the class of stochastic systems modelled as continuous time Markov Chains in order to extensively analyse and compare robustness of biological models with uncertain parameters. The framework utilises novel computational methods that enable to effectively evaluate the robustness of models with respect to quantitative temporal properties and parameters such as reaction rate constants and initial conditions. We have applied the framework to gene regulation as an example of a central biological mechanism where intrinsic and extrinsic stochasticity plays crucial role due to low numbers of DNA and RNA molecules. Using our methods we have obtained a comprehensive and precise analysis of stochastic dynamics under parameter uncertainty. Furthermore, we apply our framework to compare several variants of two-component signalling networks from the perspective of robustness with respect to intrinsic noise caused by low populations of signalling components. We have successfully extended previous studies performed on deterministic models (ODE) and showed that stochasticity may significantly affect obtained predictions. Our case studies demonstrate that the framework can provide deeper insight into the role of key parameters in maintaining the system functionality and thus it significantly contributes to formal methods in computational systems biology.

Systems Biology Laboratory at Faculty of Informatics Masaryk University Brno Czech Republic

Zobrazit více v PubMed

Kitano H (2004) Biological robustness. Nat Rev Genet 5: 826–837. PubMed

Kitano H (2007) Towards a theory of biological robustness. Molecular Systems Biology 3: 137. PubMed PMC

Ueda M, Shibata T (2007) Stochastic signal processing and transduction in chemotactic response of eukaryotic cells. Biophysical journal 93: 11. PubMed PMC

El Samad H, Khammash M, Petzold L, Gillespie D (2005) Stochastic modelling of gene regulatory networks. International Journal of Robust and Nonlinear Control 15: 691–711.

Gillespie DT (1977) Exact Stochastic Simulation of Coupled Chemical Reactions. Journal of Physical Chemistry 81: 2340–2381.

Aziz A, Sanwal K, Singhal V, Brayton R (1996) Verifying continuous time Markov chains. In: Computer Aided Verification, Springer, volume 1102 of LNCS. 269–276. doi:10.1007/3-540-61474-5 75.

Kwiatkowska M, Norman G, Pacheco A (2006) Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. Computers & Mathematics with Applications 51: 305–316.

Brim L, Češka M, Dražan S, Šafrănek D (2013) Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Computer Aided Verification. Springer Berlin Heidelberg, volume 8044 of LNCS, 107–123. doi:10.1007/978-3-642-39799-8 7.

Swat M, Kel A, Herzel H (2004) Bifurcation analysis of the regulatory modules of the mammalian g1/s transition. Bioinformatics 20: 1506–1511. PubMed

Steuer R, Waldherr S, Sourjik V, Kollmann M (2011) Robust signal processing in living cells. PLoS computational biology 7: e1002218. PubMed PMC

Munsky B, Khammash M (2006) The finite state projection algorithm for the solution of the chemical master equation. The Journal of chemical physics 124: 044104. PubMed

Henzinger TA, Mateescu M, Wolf V (2009) Sliding Window Abstraction for Infinite Markov Chains. In: Computer Aided Verification, Springer, volume 5643 of LNCS. 337–352. doi:10.1007/978-3-642-02658-4 27.

Didier F, Henzinger TA, Mateescu M, Wolf V (2009) Fast Adaptive Uniformization of the Chemical Master Equation. In: High Performance Computational Systems Biology. IEEE Computer Society, 118–127. PubMed

Barnat J, Brim L, Šafránek D (2010) High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker. Briefings in Bioinformatics 11: 301–312. PubMed

Donz A, Fanchon E, Gattepaille LM, Maler O, Tracqui P (2011) Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6: e24246. PubMed PMC

Rizk A, Batt G, Fages F, Soliman S (2009) A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25: i169–i178. PubMed PMC

Mikeev L, Neuhäuβer M, Spieler D, Wolf V (2012) On-the-y Verification and Optimization of DTAproperties for Large Markov Chains. Form Method Syst Des : 1–25.

Andreychenko A, Mikeev L, Spieler D, Wolf V (2011) Parameter Identification for Markov Models of Biochemical Reactions. In: Computer Aided Verification. Springer, LNCS, 83–98. doi:10.1007/978-3-642-22110-1 8.

Reinker S, Altman R, Timmer J (2006) Parameter Estimation in Stochastic Biochemical Reactions. IEEE Proc Syst Biol 153: 168–78. PubMed

Daigle B, Roh M, Petzold L, Niemi J (2012) Accelerated Maximum Likelihood Parameter Estimation for Stochastic Biochemical Systems. BMC Bioinformatics 13: 68–71. PubMed PMC

Hasenauer J, Wolf V, Kazeroonian A, Theis F (2013) Method of conditional moments (mcm) for the chemical master equation. Journal of Mathematical Biology : 1–49. PubMed

Bortolussi L, Hillston J (2012) Fluid model checking. In: Koutny M, Ulidowski I, editors, CONCUR 2012 Concurrency Theory, Springer Berlin Heidelberg, volume 7454 of Lecture Notes in Computer Science. 333–347. doi:10.1007/978-3-642-32940-1 24.

Golightly A, Wilkinson DJ (2011) Bayesian Parameter Inference for Stochastic Biochemical Network Models Using Particle Markov Chain Monte Carlo. Interface Focus 1: 807–820. PubMed PMC

Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, et al... (2009) A Bayesian Approach to Model Checking Biological Systems. In: Computational Methods in Systems Biology. Springer, 218–234.

Koh CH, Palaniappan S, Thiagarajan P, Wong L (2012) Improved Statistical Model Checking Methods for Pathway Analysis. BMC Bioinformatics 13: S15. PubMed PMC

Bernardini F, Biggs C, Derrick J, Gheorghe M, Niranjan M, et al... (2007) Parameter Estimation and Model Checking in a Model of Prokaryotic Autoregulation. Technical report, University of Sheffield.

Ballarini P, Forlin M, Mazza T, Prandi D (2009) Efficient Parallel Statistical Model Checking of Biochemical Networks. In: Parallel and Distributed Methods in verifiCation. volume 14 of EPTCS, 47–61.

Bartocci E, Bortolussi L, Nenzi L, Sanguinetti G (2013) On the Robustness of Temporal Properties for Stochastic Models. ArXiv e-prints.

Hoops S, Sahle S, Gauges R, Lee C, Pahle J, et al. (2006) COPASI - a COmplex PAthway SImulator. Bioinformatics 22: 3067–3074. PubMed

Loew L, Schaff J (2001) The Virtual Cell: a software environment for computational cell biology. Trends in biotechnology 19: 401–406. PubMed

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

Fainekos G, Pappas G (2009) Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410: 4262–4291.

Rizk A, Batt G, Fages F, Soliman S (2009) A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25: 169–178. PubMed PMC

Donzé A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems, Springer, volume 6246 of LNCS. 92–106. doi:10.1007/978-3-642-15297-9 9.

Donzé A (2010) Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In: Computer Aided Verification, Springer, volume 6174 of LNCS. 167–170. doi:10.1007/978-3-642-14295-6 17.

Barnat J, Brim L, Krejčí A, Streck A, Šafránek D, et al. (2012) On parameter synthesis by parallel model checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics 9: 693–705. PubMed

Chen B, Chen P (2008) Robust engineered circuit design principles for stochastic biochemical networks with parameter uncertainties and disturbances. Biomedical Circuits and Systems, IEEE Transactions on 2: 114–132. PubMed

Hill AV (1910) The possible effects of the aggregation of the molecules of hamoglobin on its dissociation curves. The Journal of Physiology 40: iv–vii.

Madsen C, Myers C, Roehner N, Winstead C, Zhang Z (2012) Utilizing stochastic model checking to analyze genetic circuits. In: Computational Intelligence in Bioinformatics and Computational Biology. IEEE Computer Society, 379–386. doi:10.1109/CIBCB.2012.6217255.

Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Formal Methods for Performance Evaluation, Springer, volume 4486 of LNCS. 220–270. doi:10.1007/978-3-540-72522-0 6.

Baier C, Haverkort B, Hermanns H, Katoen J (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29: 524–541.

Kwiatkowska MZ, Norman G, Parker D (2008) Using Probabilistic Model Checking in Systems Biology. SIGMETRICS Performance Evaluation Review 35: 14–21.

Baier C, Haverkort B, Hermanns H, Katoen JP (2000) Model Checking Continuous-Time Markov Chains by Transient Analysis. In: Computer Aided Verification, Springer, volume 1855 of LNCS. 358–372. doi:10.1007/10722167 28.

Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification. Springer, volume 6806 of LNCS, 585–591.

Kel AE, Deineko I, Kel-Margoulis OV, Wingender E, Ratner V (2000) Modeling of gene regulatory network of cell cycle control. role of e2f feedback loops. In: German Conference on Bioinformatics’ 00: 107–114.

Garai A, Waclaw B, Nagel H, Meyer-Ortmanns H (2012) Stochastic description of a bistable frustrated unit. Journal of Statistical Mechanics: Theory and Experiment 2012: P01009.

Sanft K, Gillespie D, Petzold L (2011) Legitimacy of the stochastic michaelis-menten approximation. Systems Biology, IET 5: 58–69. PubMed

Yang E, van Nimwegen E, Zavolan M, Rajewsky N, Schroeder Mk, et al. (2003) Decay Rates of Human mRNAs: Correlation With Functional Characteristics and Sequence Attributes. Genome Research 13: 1863–1872. PubMed PMC

Batchelor E, Goulian M (2003) Robustness and the cycle of phosphorylation and dephosphorylation in a two-component regulatory system. Proceedings of the National Academy of Sciences 100: 691–696. PubMed PMC

Shinar G, Milo R, Martnez MR, Alon U (2007) Inputoutput robustness in simple bacterial signaling systems. Proceedings of the National Academy of Sciences 104: 19931–19935. PubMed PMC

Zaslaver A, Mayo AE, Rosenberg R, Bashkin P, Sberro H, et al. (2004) Just-in-time transcription program in metabolic pathways. Nature Genetics 36: 486–491. PubMed

Zhang J, Watson LT, Cao Y (2009) Adaptive aggregation method for the chemical master equation. International Journal of Computational Biology and Drug Design 2: 134–148. PubMed

van Moorsel APA, Sanders WH (1994) Adaptive uniformization. ORSA Communications in Statistics: Stochastic Models, vol 10, no 3 619–648.

Funahashi A, Morohashi M, Kitano H, Tanimura N (2003) Celldesigner: a process diagram editor for gene-regulatory and biochemical networks. BIOSILICO 1: 159–162.

Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data