Article

Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates

Authors:

Roberto Barbuti,

Francesca Levi,

Guido ScatenaAuthors Info & Claims

RP '09: Proceedings of the 3rd International Workshop on Reachability Problems

Pages 64 - 78

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

Published: 27 August 2009 Publication History

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.

References

[1]

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

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

[3]

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

[4]

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

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

[6]

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

[7]

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

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

[9]

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

[10]

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

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

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

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

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

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

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

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

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

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

[22]

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

[23]

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

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

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

[26]

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

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

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

[29]

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

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

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

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

Cited By

Puggelli ALi WSangiovanni-Vincentelli ASeshia S(2013)Polynomial-Time Verification of PCTL Properties of MDPs with Convex UncertaintiesProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958115(527-542)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958115

Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
1. Applied computing
  1. Life and medical sciences
2. Theory of computation
  1. Models of computation

Recommendations

Probabilistic model checking of biological systems with uncertain kinetic rates

In this paper, we present a formalization of biological systems based on multiset rewriting and we investigate the use of abstract interpretation on its semantics. We consider a probabilistic semantics, which is well suited to represent the non-...
Interval change-point detection for runtime probabilistic model checking
ASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using interval Markov chains, i.e., Markov models with ...
Quantitative refinement and model checking for the analysis of probabilistic systems
FM'06: Proceedings of the 14th international conference on Formal Methods

For standard (ie non-probabilistic) systems of reasonable size, correctness is analysed by simulation and/or model checking, possibly with standard program-logical arguments beforehand to reduce the problem size by abstraction.

For probabilistic systems ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

RP '09: Proceedings of the 3rd International Workshop on Reachability Problems

August 2009

232 pages

ISBN:9783642044199

Editors:
Olivier Bournez
Ecole Polytechnique, Laboratoire d' Informatique (LIX), Palaiseau Cedex, France 91128
,
Igor Potapov
Department of Computer Science, Ashton Building, University of Liverpool, Liverpool, England L69 3BX

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 August 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Puggelli ALi WSangiovanni-Vincentelli ASeshia S(2013)Polynomial-Time Verification of PCTL Properties of MDPs with Convex UncertaintiesProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958115(527-542)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958115

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents