×

zbMATH — the first resource for mathematics

Probabilistic model checking of biological systems with uncertain kinetic rates. (English) Zbl 1234.92020
Summary: We present a formalization of biological systems based on multiset rewriting and we investigate the use of abstract interpretation of its semantics. We consider a probabilistic semantics, which is well suited to represent the non-deterministic evolution of real biological systems. Abstract interpretation allows us to deal with systems in which the kinetic rates of the evolution rules are not precisely known. On the (abstract) systems, we perform probabilistic model checking obtaining lower and upper bounds for the probabilities of reaching states satisfying the given properties. We apply abstract probabilistic model checking to verify reachability properties in a model of tumor growth.

MSC:
92C42 Systems biology, networks
68Q42 Grammars and rewriting systems
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)
Software:
CEGAR; PASS; PRISM
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] AMSR2PRISM tool: http://www.di.unipi.it/msvbio/wiki/amsr2prism.
[2] Baier, C.; Hermanns, H.; Katoen, J.P.; Haverkort, B.R., Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, Theoret. comput. sci., 345, 2-26, (2005) · Zbl 1081.90066
[3] Baier, C.; Katoen, J.P., Principles of model checking, (2008), The MIT Press
[4] Barbuti, R.; Caravagna, G.; Maggiolo-Schettini, A.; Milazzo, P.; Pardini, G., The calculus of looping sequences, (), 387-423
[5] Barbuti, R.; Levi, F.; Milazzo, P.; Scatena, G., Probablisitic model checking of biological systems with uncertain kinetic rates, (), 64-78 · Zbl 1260.68226
[6] Bensalem, S.; Lakhnech, Y.; Owre, S., Computing abstractions of infinite state systems compositionally and automatically, (), 319-331
[7] Cardelli, L., On process rate semantics, Theoret. comput. sci., 391, 190-215, (2008) · Zbl 1133.68054
[8] Cervesato, I.; Durgin, N.A.; Lincoln, P.; Mitchell, J.C.; Scedrov, A., A meta-notation for protocol analysis, (), 55-69
[9] Chutinan, A.; Krogh, B.H., Verification of infinite-state dynamic systems using approximate quotient transition systems, Trans. autom. control, 26, 1401-1410, (2001) · Zbl 1031.93123
[10] Coletta, A.; Gori, R.; Levi, F., Approximating probabilistic behaviors of biological systems using abstract interpretation, (), 165-182 · Zbl 1283.92037
[11] Coppo, M.; Damiani, F.; Drocco, M.; Grassi, E.; Troina, A., Stochastic calculus of wrapped compartments, (), 82-98
[12] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (), 238-252
[13] Dams, D.; Gerth, R.; Grumberg, O., Abstract interpretation of reactive systems, Toplas, 19, 253-291, (1997)
[14] Danos, V.; Feret, J.; Fontana, W.; Krivine, J., Abstract interpretation of cellular signalling networks, (), 83-97 · Zbl 1138.68650
[15] Danos, V.; Feret, J.; Fontana, W.; Russell, H.; Krivine, J., Abstracting the differential semantics of rule-based models: exact and automated model reduction, (), 362-381
[16] D’Argenio, P.R.; Jeannet, B.; Jensen, H.E.; Larsen, K.G., Reachability analysis of probabilistic systems by successive refinements, (), 39-56 · Zbl 1007.68131
[17] Di Pierro, A.; Wiklicky, H., Concurrent constraint programming: towards probabilistic abstract interpretation, (), 127-138
[18] Donaldson, A.; Miller, A.; Parker, D., GRIP: generic representatives in PRISM, (), 115-116
[19] Fecher, H.; Leucker, M.; Wolf, V., Don’t know in probabilistic systems, (), 71-88 · Zbl 1178.68341
[20] Gori, R.; Levi, F., Abstract interpretation for probabilistic termination of biological systems, (), 137-153
[21] Haddad, S.; Pekergin, N., Using stochastic comparison for efficient model checking of uncertain Markov chains, (), 177-186
[22] Hahn, E.M.; Hermanns, H.; Wachter, B.; Zhang, L., Time-bounded model checking of infinite-state continuous-time Markov chains, Fund. inform., 95, 129-155, (2009) · Zbl 1214.68213
[23] Hahn, E.M.; Hermanns, H.; Wachter, B.; Zhang, L., PASS: abstraction refinement for infinite probabilistic models, (), 353-357
[24] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. asp. comput., 6, 512-535, (1994) · Zbl 0820.68113
[25] Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (), 162-175 · Zbl 1155.68438
[26] Huth, M., On finite-state approximants for probabilistic computation tree logic, Theoret. comput. sci., 246, 113-134, (2005) · Zbl 1080.68064
[27] Jonsson, B.; Larsen, K.G., Specification and refinement of probabilistic processes, (), 266-277
[28] Katoen, J.P.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for continuous-time Markov chains, (), 311-324 · Zbl 1135.68476
[29] J. Katoen, D. Klink, M. Leucker, V. Wolf, Three-valued abstraction for probabilistic systems, Tech. Report AIB-2007-20, RWTH Aachen, Germany, 2007. · Zbl 1277.68219
[30] Kattenbelt, M.; Kwiatkowska, M.Z.; Norman, G.; Parker, D., Game-based probabilistic predicate abstraction in PRISM, (), 5-21 · Zbl 1286.68316
[31] Kearfott, R.B., Interval computations: introduction, uses, and resources, Euromath bull., 2, 95-112, (1996)
[32] D. Klink, Three-valued abstraction for stochastic systems, Ph.D. Thesis, RWTH Aachen University, Germany, 2010.
[33] Kozine, I.; Utkin, L.V., Interval-valued finite Markov chains, Reliab. comput., 8, 97-113, (2002) · Zbl 1001.65007
[34] Kwiatkowska, M.Z.; Norman, G.; Parker, D., PRISM: probabilistic symbolic model checker, (), 200-204 · Zbl 1047.68533
[35] Kwiatkowska, M.Z., Model checking for probability and time: from theory to practice, (), 351-360
[36] Kwiatkowska, M.Z.; Norman, G.; Parker, D., Game-based abstraction for Markov decision processes, (), 157-166
[37] Mamoun, M.B.; Pekergin, N., Model checking of infinite state space Markov chains by stochastic bounds, (), 264-278
[38] Monniaux, D., Abstract interpretation of programs as Markov decision processes, Sci. comput. programming, 58, 179-205, (2005) · Zbl 1088.68039
[39] Paˇun, G., Membrane computing. an introduction, (2002), Springer-Verlag · Zbl 1034.68037
[40] Sen, K.; Viswanathan, M.; Agha, G., Model-checking Markov chains in the presence of uncertainties, (), 394-410 · Zbl 1180.68179
[41] Skulj, D., Finite discrete time Markov chains with interval probabilities, (), 299-306 · Zbl 1106.60066
[42] Skulj, D., Discrete time Markov chains with interval probabilities, Internat. J. approx. reason., 50, 1314-1329, (2009) · Zbl 1195.60100
[43] Villasana, M.; Radunskaya, A., A delay differential equation model for tumor growth, J. math. biol., 47, 270-294, (2003) · Zbl 1023.92014
[44] Wachter, B.; Zhang, L.; Hermanns, H., Probabilistic model checking modulo theories, (), 129-140
[45] K. Weichselberger, The theory of interval-probability as a unifying concept for uncertainty, in: G. De Cooman, F. Gagliardi Cozman, S. Moral, P. Walley (Eds.), Imprecise Probabilities and their Applications, ISIPTA 1999, pp. 387-396.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.