Skip to main content
SpringerLink
Log in

Bounding Mean First Passage Times in Population Continuous-Time Markov Chains

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12289))

Included in the following conference series:

Abstract

We consider the problem of bounding mean first passage times and reachability probabilities for the class of population continuous-time Markov chains, which capture stochastic interactions between groups of identical agents. The quantitative analysis of such models is notoriously difficult since typically neither state-based numerical approaches nor methods based on stochastic sampling give efficient and accurate results. Here, we propose a novel approach that leverages techniques from martingale theory and stochastic processes to generate constraints on the statistical moments of first passage time distributions. These constraints induce a semi-definite program that can be used to compute exact bounds on reachability probabilities and mean first passage times without numerically solving the transient probability distribution of the process or sampling from it. We showcase the method on some test examples and tailor it to models exhibiting multimodality, a class of particularly challenging scenarios from biology.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Similar content being viewed by others

References

  1. Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Parameter identification for Markov models of biochemical reactions. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 83–98. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_8

    Chapter  Google Scholar 

  2. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61474-5_75

    Chapter  Google Scholar 

  3. Backenköhler, M., Bortolussi, L., Wolf, V.: Moment-based parameter estimation for stochastic reaction networks in equilibrium. IEEE/ACM Trans. Comput. Biol. Bioinform. 15(4), 1180–1192 (2017)

    Article  Google Scholar 

  4. Backenköhler, M., Bortolussi, L., Wolf, V.: Control variates for stochastic simulation of chemical reaction networks. In: Bortolussi, L., Sanguinetti, G. (eds.) CMSB 2019. LNCS, vol. 11773, pp. 42–59. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31304-3_3

    Chapter  Google Scholar 

  5. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

    Article  Google Scholar 

  6. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_28

    Chapter  Google Scholar 

  7. Barzel, B., Biham, O.: Calculation of switching times in the genetic toggle switch and other bistable systems. Phys. Rev. E 78(4), 041919 (2008)

    Article  Google Scholar 

  8. Bel, G., Munsky, B., Nemenman, I.: The simplicity of completion time distributions for common complex biochemical processes. Phys. Biol. 7(1), 016003 (2009)

    Article  Google Scholar 

  9. Bernardo, M., De Nicola, R., Hillston, J. (eds.): Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems. LNCS, vol. 9700. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8

    Book  Google Scholar 

  10. Bogomolov, S., Henzinger, T.A., Podelski, A., Ruess, J., Schilling, C.: Adaptive moment closure for parameter inference of biochemical reaction networks. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 77–89. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23401-4_8

    Chapter  Google Scholar 

  11. Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: a tutorial. Perform. Eval. 70(5), 317–349 (2013)

    Article  Google Scholar 

  12. Bortolussi, L., Lanciani, R.: Model checking Markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_9

    Chapter  Google Scholar 

  13. Bortolussi, L., Lanciani, R.: Stochastic approximation of global reachability probabilities of Markov population models. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 224–239. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10885-8_16

    Chapter  Google Scholar 

  14. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26–42. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24310-3_4

    Chapter  MATH  Google Scholar 

  15. Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science, pp. 309–318. IEEE (2009)

    Google Scholar 

  16. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transf. 17(3), 351–367 (2015)

    Article  Google Scholar 

  17. Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A STORM is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

    Chapter  Google Scholar 

  18. Diamond, S., Boyd, S.: CVXPY: a Python-embedded modeling language for convex optimization. J. Mach. Learn. Res. 17(83), 1–5 (2016)

    MathSciNet  MATH  Google Scholar 

  19. Dowdy, G.R., Barton, P.I.: Bounds on stochastic chemical kinetic systems at steady state. J. Chem. Phys. 148(8), 084106 (2018)

    Article  Google Scholar 

  20. Dowdy, G.R., Barton, P.I.: Dynamic bounds on stochastic chemical kinetic systems using semidefinite programming. J. Chem. Phys. 149(7), 074103 (2018)

    Article  Google Scholar 

  21. Engblom, S.: Computing the moments of high dimensional solutions of the master equation. Appl. Math. Comput. 180(2), 498–515 (2006)

    MathSciNet  MATH  Google Scholar 

  22. Gast, N., Bortolussi, L., Tribastone, M.: Size expansions of mean field approximation: transient and steady-state analysis. Perform. Eval. 129, 60–80 (2019). https://doi.org/10.1016/j.peva.2018.09.005

    Article  Google Scholar 

  23. Ghusinga, K.R., Vargas-Garcia, C.A., Lamperski, A., Singh, A.: Exact lower and upper bounds on stationary moments in stochastic biochemical systems. Phys. Biol. 14(4), 04LT01 (2017)

    Google Scholar 

  24. Gihman, I., Skorohod, A.: The Theory of Stochastic Processes II. Springer, Heidelberg (1975)

    MATH  Google Scholar 

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

    Article  Google Scholar 

  26. Gupta, A., Briat, C., Khammash, M.: A scalable computational framework for establishing long-term behavior of stochastic reaction networks. PLoS Comput. Biol. 10(6), e1003669 (2014)

    Article  Google Scholar 

  27. Hasenauer, J., Wolf, V., Kazeroonian, A., Theis, F.J.: Method of conditional moments (MCM) for the chemical master equation. J. Math. Biol. 69(3), 687–735 (2014)

    Article  MathSciNet  Google Scholar 

  28. Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. Theor. Comput. Sci. 413(1), 106–141 (2012)

    Article  MathSciNet  Google Scholar 

  29. Helmes, K., Röhl, S., Stockbridge, R.H.: Computing moments of the exit time distribution for Markov processes by linear programming. Oper. Res. 49(4), 516–530 (2001)

    Article  MathSciNet  Google Scholar 

  30. Hespanha, J.: Moment closure for biochemical networks. In: 2008 3rd International Symposium on Communications, Control and Signal Processing, pp. 142–147. IEEE (2008)

    Google Scholar 

  31. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_29

    Chapter  Google Scholar 

  32. Iyer-Biswas, S., Zilman, A.: First-passage processes in cellular biology. Adv. Chem. Phys. 160, 261–306 (2016)

    Google Scholar 

  33. Kashima, K., Kawai, R.: Polynomial programming approach to weak approximation of lévy-driven stochastic differential equations with application to option pricing. In: 2009 ICCAS-SICE, pp. 3902–3907. IEEE (2009)

    Google Scholar 

  34. Kazeroonian, A., Theis, F.J., Hasenauer, J.: Modeling of stochastic biological processes with non-polynomial propensities using non-central conditional moment equation. IFAC Proc. Vol. 47(3), 1729–1735 (2014)

    Article  Google Scholar 

  35. Kuntz, J., Thomas, P., Stan, G.B., Barahona, M.: Rigorous bounds on the stationary distributions of the chemical master equation via mathematical programming. arXiv preprint arXiv:1702.05468 (2017)

  36. Kuntz, J., Thomas, P., Stan, G.B., Barahona, M.: Approximation schemes for countably-infinite linear programs with moment bounds. arXiv preprint arXiv:1810.03658 (2018)

  37. Kuntz, J., Thomas, P., Stan, G.B., Barahona, M.: The exit time finite state projection scheme: bounding exit distributions and occupation measures of continuous-time Markov chains. SIAM J. Sci. Comput. 41(2), A748–A769 (2019)

    Article  MathSciNet  Google Scholar 

  38. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  39. Lasserre, J.B.: Moments, Positive Polynomials and Their Applications, vol. 1. World Scientific, Singapore (2010)

    MATH  Google Scholar 

  40. Lasserre, J.B., Prieto-Rumeau, T., Zervos, M.: Pricing a class of exotic options via moments and sdp relaxations. Math. Finance 16(3), 469–494 (2006)

    Article  MathSciNet  Google Scholar 

  41. Mikeev, L., Neuhäußer, M.R., Spieler, D., Wolf, V.: On-the-fly verification and optimization of DTA-properties for large Markov chains. Form. Methods Syst. Des. 43(2), 313–337 (2013)

    Article  Google Scholar 

  42. MOSEK ApS: MOSEK Optimizer API for C 8.1.0.67 (2018). https://docs.mosek.com/8.1/capi/index.html

  43. Munsky, B., Nemenman, I., Bel, G.: Specificity and completion time distributions of biochemical processes. J. Chem. Phys. 131(23), 12B616 (2009)

    Article  Google Scholar 

  44. O’Donoghue, B., Chu, E., Parikh, N., Boyd, S.: SCS: splitting conic solver, version 2.1.0, November 2017. https://github.com/cvxgrp/scs

  45. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)

    Article  MathSciNet  Google Scholar 

  46. Porter, M.A., Gleeson, J.P.: Dynamical Systems on Networks. FADSRT, vol. 4. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-26641-1

    Book  MATH  Google Scholar 

  47. Sakurai, Y., Hori, Y.: A convex approach to steady state moment analysis for stochastic chemical reactions. In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pp. 1206–1211. IEEE (2017)

    Google Scholar 

  48. Sakurai, Y., Hori, Y.: Bounding transient moments of stochastic chemical reactions. IEEE Control. Syst. Lett. 3(2), 290–295 (2019)

    Article  Google Scholar 

  49. Schnoerr, D., Cseke, B., Grima, R., Sanguinetti, G.: Efficient low-order approximation of first-passage time distributions. Phys. Rev. Lett. 119, 210601 (2017). https://doi.org/10.1103/PhysRevLett.119.210601

    Article  Google Scholar 

  50. Schnoerr, D., Sanguinetti, G., Grima, R.: Comparison of different moment-closure approximations for stochastic chemical kinetics. J. Chem. Phys. 143(18), 185101 (2015). https://doi.org/10.1063/1.4934990

    Article  Google Scholar 

  51. Schnoerr, D., Sanguinetti, G., Grima, R.: Approximation and inference methods for stochastic biochemical Kinetics’a tutorial review. J. Phys. Math. Theor. 50(9), 093001 (2017). https://doi.org/10.1088/1751-8121/aa54d9

    Article  MathSciNet  MATH  Google Scholar 

  52. Spieler, D., Hahn, E.M., Zhang, L.: Model checking CSL for Markov population models. arXiv preprint arXiv:1111.4385 (2011)

  53. Stekel, D.J., Jenkins, D.J.: Strong negative self regulation of prokaryotic transcription factors increases the intrinsic noise of protein expression. BMC Syst. Biol. 2(1), 6 (2008)

    Article  Google Scholar 

  54. Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation: the Mathematical Basis of Performance Modeling. Princeton University Press, Princeton (2009)

    Book  Google Scholar 

  55. Ullah, M., Wolkenhauer, O.: Stochastic approaches for systems biology. Wiley Interdiscip. Rev. Syst. Biol. Med. 2, 385–97 (2009). https://doi.org/10.1002/wsbm.78

  56. Vandenberghe, L.: The CVXOPT linear and quadratic cone program solvers (2010). http://cvxopt.org/documentation/coneprog.pdf

Download references

Acknowledgements

We would like to thank Andreas Karrenbauer for helpful comments on the usage of SDP solvers and Gerrit Großmann for the valuable comments on this manuscript. This work is supported by the DFG project “MULTIMODE”, and partially supported by the italian PRIN project “SEDUCE” n. 2017TWRCNB.

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Michael Backenköhler, Luca Bortolussi & Verena Wolf

  2. Saarbrücken Graduate School of Computer Science, Saarbrücken, Germany

    Michael Backenköhler

  3. University of Trieste, Trieste, Italy

    Luca Bortolussi

Authors
  1. Michael Backenköhler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Bortolussi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Verena Wolf
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Backenköhler .

Editor information

Editors and Affiliations

  1. Politecnico di Milano, Milan, Italy

    Marco Gribaudo

  2. Chinese Academy of Sciences, Beijing, China

    David N. Jansen

  3. University of Münster, Münster, Germany

    Anne Remke

1 Electronic supplementary material

Below is the link to the electronic supplementary material.

Supplementary material 1 (pdf 194 KB)

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Backenköhler, M., Bortolussi, L., Wolf, V. (2020). Bounding Mean First Passage Times in Population Continuous-Time Markov Chains. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds) Quantitative Evaluation of Systems. QEST 2020. Lecture Notes in Computer Science(), vol 12289. Springer, Cham. https://doi.org/10.1007/978-3-030-59854-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-59854-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-59853-2

  • Online ISBN: 978-3-030-59854-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation