Skip to main content
SpringerLink
Log in

Approximation Techniques for Stochastic Analysis of Biological Systems

  • Chapter
  • First Online:
Book cover Automated Reasoning for Systems Biology and Medicine

Part of the book series: Computational Biology ((COBO,volume 30))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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–213

    Chapter  Google Scholar 

  2. Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Logic 1:162–170

    Article  MathSciNet  Google Scholar 

  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. https://doi.org/10.1109/QEST.2004.1348037

  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. https://doi.org/10.1016/j.entcs.2005.10.034

    Article  Google Scholar 

  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. http://eprints.qut.edu.au/46148/

  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. https://doi.org/10.1145/5397.5399

    Article  Google Scholar 

  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–345

    Google Scholar 

  8. Courcoubetis C, Yannakakis M (1995) The complexity of probabilistic verification. J ACM 42(4):857–907

    Article  MathSciNet  Google Scholar 

  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. https://doi.org/10.1109/QEST.2012.22

  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. https://doi.org/10.1007/11691617_5

    Chapter  Google Scholar 

  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–132

    Chapter  Google Scholar 

  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–342

    Google Scholar 

  13. Fisler K, Vardi MY (2002) Bisimulation minimization and symbolic model checking. Form Methods Syst Des 21(1):39–78. https://doi.org/10.1023/A:1016091902809

    Article  Google Scholar 

  14. Gardner TS, Cantor CR, Collins JJ (2000) Construction of a genetic toggle switch in Escherichia coli. Nature 403:339–342

    Article  Google Scholar 

  15. Gillespie DT (1977) Exact stochastic simulation of coupled chemical reactions. J Chem Phys 81(25):2340–2361

    Article  Google Scholar 

  16. Grassmann W (1977) Transient solutions in Markovian queueing systems. Comput Oper Res 4(1):47–53. https://doi.org/10.1016/0305-0548(77)90007-7, http://www.sciencedirect.com/science/article/pii/0305054877900077

    Article  Google Scholar 

  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. https://doi.org/10.1287/opre.32.2.343

    Article  MathSciNet  Google Scholar 

  18. Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535

    Article  Google Scholar 

  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–47

    Chapter  Google Scholar 

  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–352

    Chapter  Google Scholar 

  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. https://doi.org/10.1007/978-3-540-70545-1_16

  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. http://dl.acm.org/citation.cfm?id=1763507.1763519

  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. http://dl.acm.org/citation.cfm?id=1770351.1770401

  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–175

    Google Scholar 

  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–270

    Google Scholar 

  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–37

    Chapter  Google Scholar 

  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–591

    Chapter  Google Scholar 

  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. https://publications.cispa.saarland/891/, pub\_id: 705. Bibtex: LaMiWo\_11:Shave. URL date: None

  29. Madsen C (2013) Stochastic analysis of synthetic genetic circuits. PhD thesis, University of Utah

    Google Scholar 

  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–39

    Article  Google Scholar 

  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. https://doi.org/10.1145/2644817

    Article  Google Scholar 

  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–18

    Chapter  Google Scholar 

  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. https://doi.org/10.1063/1.2145882

    Article  Google Scholar 

  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. https://doi.org/10.1109/TAC.2007.911361

    Article  MathSciNet  Google Scholar 

  35. Myers CJ (2009) Engineering genetic circuits. Chapman & Hall/CRC mathematical and computational biology, 1st edn. Chapman & Hall/CRC, London

    Google Scholar 

  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. https://doi.org/10.1093/bioinformatics/btp457

    Article  Google Scholar 

  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. https://doi.org/10.1063/1.1545446

    Article  Google Scholar 

  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–140

    Google Scholar 

  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. https://doi.org/10.1021/acssynbio.8b00078, pMID: 29944839

  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. https://doi.org/10.1073/pnas.1617932114, http://www.pnas.org/content/113/52/15000, http://www.pnas.org/content/113/52/15000.full.pdf

    Article  Google Scholar 

Download references

Acknowledgements

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.

Author information

Authors and Affiliations

  1. Utah State University, Logan, UT, USA

    Thakur Neupane & Zhen Zhang

  2. Boston University, Boston, MA, USA

    Curtis Madsen

  3. University of South Florida, Tampa, FL, USA

    Hao Zheng

  4. University of Utah, Salt Lake City, UT, USA

    Chris J. Myers

Authors
  1. Thakur Neupane
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhen Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Curtis Madsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hao Zheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Chris J. Myers
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhen Zhang .

Editor information

Editors and Affiliations

  1. Department of Computer Science and Technology, University of Cambridge, Cambridge, UK

    Pietro Liò

  2. School of Computing, Newcastle University, Newcastle, UK

    Paolo Zuliani

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Neupane, T., Zhang, Z., Madsen, C., Zheng, H., Myers, C.J. (2019). Approximation Techniques for Stochastic Analysis of Biological Systems. In: Liò, P., Zuliani, P. (eds) Automated Reasoning for Systems Biology and Medicine. Computational Biology, vol 30. Springer, Cham. https://doi.org/10.1007/978-3-030-17297-8_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-17297-8_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-17296-1

  • Online ISBN: 978-3-030-17297-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation