Skip to main content
SpringerLink
Log in

Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates

  • Conference paper
Reachability Problems (RP 2009)

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

Included in the following conference series:

Abstract

We present an abstraction of the probabilistic semantics of Multiset Rewriting to formally express systems of reactions with uncertain kinetic rates. This allows biological systems modelling when the exact rates are not known, but are supposed to lie in some intervals. On these (abstract) models we perform probabilistic model checking obtaining lower and upper bounds for the probabilities of reaching states satisfying given properties. These bounds are under- and over-approximations, respectively, of the probabilities one would obtain by verifying the models with exact kinetic rates belonging to the intervals.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55–69 (1999)

    Google Scholar 

  2. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM Press, New York (1977)

    Google Scholar 

  3. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE, Los Alamitos (1991)

    Google Scholar 

  4. Kozine, I., Utkin, L.V.: Interval-valued finite markov chains. Reliable Computing 8(2), 97–113 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  5. Fecher, H., Leucker, M., Wolf, V.: Don’t Know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Villasana, M., Radunskaya, A.: A delay differential equation model for tumor growth. J. of Math. Biol. 47, 270–294 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  7. Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: LICS, pp. 351–360. IEEE, Los Alamitos (2003)

    Google Scholar 

  8. Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  10. Kearfott, R.B.: Interval computations: Introduction, uses, and resources. In: Euromath Bulletin, vol. 2, pp. 95–112. European Mathematical Trust (1996)

    Google Scholar 

  11. Weichselberger, K.: The theory of interval-probability as a unifying concept for uncertainty. In: Cooman, G.D., Cozman, F.G., Moral, S., Walley, P. (eds.) ISIPTA, pp. 387–396 (1999)

    Google Scholar 

  12. Coletta, A., Gori, R., Levi, F.: Approximating probabilistic behaviors of biological systems using abstract interpretation. ENTCS, vol. 229, pp. 165–182. Elsevier, Amsterdam (2009)

    MATH  Google Scholar 

  13. D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. AMSR2PRISM, http://www.di.unipi.it/~milazzo/biosims/

  15. PRISM model checker, http://www.prismmodelchecker.org

  16. Huth, M.: On finite-state approximants for probabilistic computation tree logic. Theor. Comput. Sci. 246, 113–134 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  17. Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  18. Škulj, D.: Finite Discrete Time Markov Chains with Interval Probabilities. In: Lawry, J., Miranda, E., Bugarín, A., Li, S., Gil, M.A., Grzegorzewski, P., Hryniewicz, O. (eds.) SMPS, pp. 299–306. Springer, Heidelberg (2006)

    Google Scholar 

  19. Blanc, J.P.C., Hertog, D.D.: On Markov Chains with Uncertain Data. CentER Discussion Paper Series 50, Tilburg Univ., Center for Economic Research (2008)

    Google Scholar 

  20. Danos, V., Feret, J., Fontana, W., Krivine, J.: Abstract interpretation of cellular signalling networks. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 83–97. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Fages, F., Soliman, S.: Formal Cell Biology in Biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 54–80. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Monniaux, D.: Abstract interpretation of programs as Markov decision processes. In: Sci. Comput. Program, vol. 58, pp. 179–205. Springer, Heidelberg (2005)

    Google Scholar 

  23. Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: towards probabilistic abstract interpretation. In: PPDP, pp. 127–138. ACM, New York (2000)

    Chapter  Google Scholar 

  24. Wilkinson, S.J., Benson, N., Kell, D.B.: Proximate parameter tuning for biochemical networks with uncertain kinetic parameters. In: Mol. bioSys., vol. 4, pp. 74–97. RSC Publishing (2008)

    Google Scholar 

  25. Batt, G., Belta, C., Weiss, R.: Model Checking Genetic Regulatory Networks with Parameter Uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 61–75. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Manca, V.: The Metabolic Algorithm for P Systems: Principles and Applications. Theor. Comput. Sci. 404, 142–155 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  27. Donaldson, R., Gilbert, D.: A Model Checking Approach to the Parameter Estimation of Biochemical Pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Fages, F., Soliman, S.: Model Revision from Temporal Logic Properties in Systems Biology. In: De Raedt, L., Frasconi, P., Kersting, K., Muggleton, S.H. (eds.) Probabilistic Inductive Logic Programming. LNCS, vol. 4911, pp. 287–304. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Form. Asp. Comput. 19, 93–109 (2007)

    Article  MATH  Google Scholar 

  30. Han, T., Katoen, J.P., Mereacre, A.: Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability. In: RTSS, pp. 173–182. IEEE, Los Alamitos (2008)

    Google Scholar 

  31. Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-Valued Abstraction for Continuous-Time Markov Chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  32. Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci. 345, 2–26 (2005)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Informatica, Univ. di Pisa, Largo B. Pontecorvo 3, 56127, Pisa, Italy

    Roberto Barbuti, Francesca Levi & Paolo Milazzo

  2. IMT Lucca Inst. for Advanced Studies, Piazza San Ponziano 6, 55100, Lucca, Italy

    Guido Scatena

Authors
  1. Roberto Barbuti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesca Levi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paolo Milazzo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Guido Scatena
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ecole Polytechnique, Laboratoire d’ Informatique (LIX), 91128, Palaiseau Cedex, France

    Olivier Bournez

  2. Department of Computer Science, Ashton Building, University of Liverpool, L69 3BX, Liverpool, England

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barbuti, R., Levi, F., Milazzo, P., Scatena, G. (2009). Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates. In: Bournez, O., Potapov, I. (eds) Reachability Problems. RP 2009. Lecture Notes in Computer Science, vol 5797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04420-5_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04420-5_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04419-9

  • Online ISBN: 978-3-642-04420-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation