Approximation Techniques for Stochastic Analysis of Biological Systems

  • Thakur Neupane
  • Zhen ZhangEmail author
  • Curtis Madsen
  • Hao Zheng
  • Chris J. Myers
Part of the Computational Biology book series (COBO, volume 30)


There has been an increasing demand for formal methods in the design process of safety-critical synthetic genetic circuits. Probabilistic model checking techniques have demonstrated significant potential in analyzing the intrinsic probabilistic behaviors of complex genetic circuit designs. However, its inability to scale limits its applicability in practice. This chapter addresses the scalability problem by presenting a state-space approximation method to remove unlikely states resulting in a reduced, finite state representation of the infinite-state continuous-time Markov chain that is amenable to probabilistic model checking. The proposed method is evaluated on a design of a genetic toggle switch. Comparisons with another state-of-the-art tool demonstrate both accuracy and efficiency of the presented method.



The authors thank Verena Wolf for providing benchmarks and the STAR tool. The authors would also like to thank Dave Parker and Joachim Klein for providing assistance in interfacing with the PRISM tool. We also thank the reviewers for their feedback on an earlier version of this paper. Chris Myers is supported by the National Science Foundation under Grant No., CCF-1218095 and No., CCF-1748200. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF.


  1. 1.
    Abate A, Brim L, Češka M, Kwiatkowska M (2015) Adaptive aggregation of Markov chains: quantitative analysis of chemical reaction networks. In: Kroening D, Păsăreanu CS (eds) Computer aided verification. Springer International Publishing, Cham, pp 195–213CrossRefGoogle Scholar
  2. 2.
    Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Logic 1:162–170MathSciNetCrossRefGoogle Scholar
  3. 3.
    Baier C, Größer M, Ciesinski F (2004) Partial order reduction for probabilistic systems. In: 1st international conference on quantitative evaluation of systems (QEST 2004), Enschede, The Netherlands, 27–30 September 2004. IEEE Computer Society, pp 230–239.
  4. 4.
    Baier C, D’Argenio P, Groesser M (2006) Partial order reduction for probabilistic branching time. Electron Notes Theor Comput Sci 153(2):97–116. Scholar
  5. 5.
    Burrage K, Hegland M, Macnamara S, Sidje R (2006) A Krylov-based finite state projection algorithm for solving the chemical master equation arising in the discrete modelling of biological systems. In: Langville AN, Stewart WJ (eds) MAM 2006: Markov anniversary meeting: an international conference to celebrate the 150th anniversary of the birth of A.A. Markov. Boston Books, Charleston, South Carolina, pp 21–38.
  6. 6.
    Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263. Scholar
  7. 7.
    Courcoubetis C, Yannakakis M (1988) Verifying temporal properties of finite state probabilistic programs. In: Proceedings of the 29th annual symposium on foundations of computer science (FOCS’88). IEEE Computer Society Press, pp 338–345Google Scholar
  8. 8.
    Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857–907MathSciNetCrossRefGoogle Scholar
  9. 9.
    Díaz ÁF, Baier C, Earle CB, Fredlund L (2012) Static partial order reduction for probabilistic concurrent systems. In: Ninth international conference on quantitative evaluation of systems, QEST 2012, London, United Kingdom, 17–20 September 2012. IEEE Computer Society, pp 104–113.
  10. 10.
    Fecher H, Leucker M, Wolf V (2006) Don’t know in probabilistic systems. In: Proceedings of the 13th international conference on model checking software. Springer-Verlag, Berlin, SPIN’06, pp 71–88. Scholar
  11. 11.
    Fisler K, Vardi MY (1998) Bisimulation minimization in an automata-theoretic verification framework. In: FMCAD. Lecture notes in computer science, vol 1522. Springer, Berlin, pp 115–132CrossRefGoogle Scholar
  12. 12.
    Fisler K, Vardi MY (1999) Bisimulation and model checking. In: Pierre L, Kropf T (eds) Correct hardware design and verification methods. Springer, Berlin, pp 338–342Google Scholar
  13. 13.
    Fisler K, Vardi MY (2002) Bisimulation minimization and symbolic model checking. Form Methods Syst Des 21(1):39–78. Scholar
  14. 14.
    Gardner TS, Cantor CR, Collins JJ (2000) Construction of a genetic toggle switch in Escherichia coli. Nature 403:339–342CrossRefGoogle Scholar
  15. 15.
    Gillespie DT (1977) Exact stochastic simulation of coupled chemical reactions. J Chem Phys 81(25):2340–2361CrossRefGoogle Scholar
  16. 16.
    Grassmann W (1977) Transient solutions in Markovian queueing systems. Comput Oper Res 4(1):47–53., Scholar
  17. 17.
    Gross D, Miller DR (1984) The randomization technique as a modeling tool and solution procedure for transient Markov processes. Oper Res 32(2):343–361. Scholar
  18. 18.
    Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535CrossRefGoogle Scholar
  19. 19.
    Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2006) Probabilistic model checking of complex biological pathways. In: Priami C (ed) Computational methods in systems biology. Springer, Berlin, pp 32–47CrossRefGoogle Scholar
  20. 20.
    Henzinger TA, Mateescu M, Wolf V (2009) Sliding window abstraction for infinite Markov chains. In: Bouajjani A, Maler O (eds) Computer aided verification. Springer, Berlin, pp 337–352CrossRefGoogle Scholar
  21. 21.
    Hermanns H, Wachter B, Zhang L (2008) Probabilistic CEGAR. In: Proceedings of the 20th international conference on computer aided verification. Springer-Verlag, Berlin, CAV ’08, pp 162–175.
  22. 22.
    Katoen JP, Kemna T, Zapreev I, Jansen DN (2007a) Bisimulation minimisation mostly speeds up probabilistic model checking. In: Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems. Springer-Verlag, Berlin, TACAS’07, pp 87–101.
  23. 23.
    Katoen JP, Klink D, Leucker M, Wolf V (2007b) Three-valued abstraction for continuous-time Markov chains. In: Proceedings of the 19th international conference on computer aided verification. Springer-Verlag, Berlin, CAV’07, pp 311–324.
  24. 24.
    Kuwahara H, Myers C, Barker N, Samoilov M, Arkin A (2006) Automated abstraction methodology for genetic regulatory networks. Trans Comp Syst Biol VI:150–175Google Scholar
  25. 25.
    Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Bernardo M, Hillston J (eds) Formal methods for the design of computer, communication and software systems: performance evaluation (SFM’07). LNCS (tutorial volume), vol 4486. Springer, Berlin, pp 220–270Google Scholar
  26. 26.
    Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: Esparza J, Majumdar R (eds) Tools and algorithms for the construction and analysis of systems, pp 23–37CrossRefGoogle Scholar
  27. 27.
    Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification (CAV’11). LNCS, vol 6806. Springer, Berlin, pp 585–591CrossRefGoogle Scholar
  28. 28.
    Lapin M, Mikeev L, Wolf V (2011) Shave: stochastic hybrid analysis of Markov population models. In: Proceedings of the 14th ACM international conference on hybrid systems: computation and control, HSCC 2011, Chicago, IL, USA, 12–14 April 2011. ACM, pp 311–312., pub\_id: 705. Bibtex: LaMiWo\_11:Shave. URL date: None
  29. 29.
    Madsen C (2013) Stochastic analysis of synthetic genetic circuits. PhD thesis, University of UtahGoogle Scholar
  30. 30.
    Madsen C, Myers CJ, Patterson T, Roehner N, Stevens JT, Winstead C (2012) Design and test of genetic circuits using iBioSim. IEEE Des Test Comput 29(3):32–39CrossRefGoogle Scholar
  31. 31.
    Madsen C, Zhang Z, Roehner N, Winstead C, Myers C (2014) Stochastic model checking of genetic circuits. J Emerg Technol Comput Syst 11(3):23:1–23:21. Scholar
  32. 32.
    Mikeev L, Sandmann W, Wolf V (2013) Numerical approximation of rare event probabilities in biochemically reacting systems. In: Gupta A, Henzinger TA (eds) Computational methods in systems biology. Springer, Berlin, pp 5–18CrossRefGoogle Scholar
  33. 33.
    Munsky B, Khammash M (2006) The finite state projection algorithm for the solution of the chemical master equation. J Chem Phys 124(4):044104. Scholar
  34. 34.
    Munsky B, Khammash M (2008) The finite state projection approach for the analysis of stochastic noise in gene networks. IEEE Trans Autom Control 53(Special Issue):201–214. Scholar
  35. 35.
    Myers CJ (2009) Engineering genetic circuits. Chapman & Hall/CRC mathematical and computational biology, 1st edn. Chapman & Hall/CRC, LondonGoogle Scholar
  36. 36.
    Myers CJ, Barker N, Jones K, Kuwahara H, Madsen C, Nguyen NPD (2009) iBioSim: a tool for the analysis and design of genetic circuits. Bioinformatics 25(21):2848–2849. Scholar
  37. 37.
    Rao CV, Arkin AP (2003) Stochastic chemical kinetics and the quasi-steady-state assumption: application to the Gillespie algorithm. J Chem Phys 118(11):4999–5010. Scholar
  38. 38.
    Wachter B, Zhang L, Hermanns H (2007) Probabilistic model checking modulo theories. In: fourth international conference on the quantitative evaluation of systems (QEST 2007), pp 129–140Google Scholar
  39. 39.
    Watanabe L, Nguyen T, Zhang M, Zundel Z, Zhang Z, Madsen C, Roehner N, Myers C (0) ibiosim 3: A tool for model-based genetic circuit design. ACS Synth Biol 0(0):null., pMID: 29944839
  40. 40.
    Zheng H, Ho PY, Jiang M, Tang B, Liu W, Li D, Yu X, Kleckner NE, Amir A, Liu C (2016) Interrogating the Escherichia coli cell cycle by cell dimension perturbations. Proc Natl Acad Sci 113(52):15000–15005.,, Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Thakur Neupane
    • 1
  • Zhen Zhang
    • 1
    Email author
  • Curtis Madsen
    • 2
  • Hao Zheng
    • 3
  • Chris J. Myers
    • 4
  1. 1.Utah State UniversityLoganUSA
  2. 2.Boston UniversityBostonUSA
  3. 3.University of South FloridaTampaUSA
  4. 4.University of UtahSalt Lake CityUSA

Personalised recommendations