zbMATH — the first resource for mathematics

Analysing biochemical oscillation through probabilistic model checking. (English) Zbl 1283.92023
Cannata, Nicola (ed.) et al., Proceedings of the 2nd workshop – from biology to concurrency and back (FBTC 2008), Reykjavik, Iceland, July 12, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 229, No. 1, 3-19 (2009).
Summary: Automated verification of stochastic models has been proved to be an effective technique for the analysis of a large class of stochastically behaving systems. In this paper we show how stochastic model-checking can be effectively applied to the analysis of biological systems. We consider a few models of biological systems taken from the literature, and we consider both their encodings as ordinary differential equations and Markovian models. We show that stochastic model-checking verification of biological systems can complement both deterministic and stochastic simulation techniques when dealing with dynamical properties of oscillators. We demonstrate how stochastic model-checking can provide exact quantitative characterization of properties of systems exhibiting oscillatory behavior, providing insights that cannot be obtained with differential equations models and that would require a large number of runs with stochastic simulation approaches.
For the entire collection see [Zbl 1278.92003].

92C40 Biochemistry, molecular biology
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Baier, C.; Haverkort, B.; Hermann, H.; Katoen, J.-P., Model-checking algorithms for continuous-time Markov chains, IEEE trans. on software eng., 29, 6, 524-541, (June 2003)
[2] P. Ballarini, R. Mardare, and I. Mura. Query-based verification of biochemical oscillations through probabilistic model checking, TR 05/2008, available at http://www.cosbi.eu. Technical report, CoSBi, 2008 · Zbl 1283.92023
[3] L. Cardelli. Artificial biochemistry. Technical report, The Microsoft Research - CoSBi, 2006
[4] M. Cavaliere and S. Sedwards. Modelling cellular processes using membrane systems with peripheral and integral proteins. In Springer, editor, Proceedings of the fourth International Conference on Computational Methods in Systems Biology (CMSB2006), LNBI-LNCS 4210, 2006 · Zbl 1277.68072
[5] Ciocchetta, F.; Hillston, J., Bio-PEPA: an extension of the process algebra PEPA for biochemical networks, Proceedings of FBTC 2007, Electronic notes in theoretical computer science, 194, 103-117, (2008) · Zbl 1279.68254
[6] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press
[7] Dematté, L.; Priami, C.; Romanel, A., Modelling and simulation of biological processes in blenx, SIGMETRICS performance evaluation review, 35, 4, 32-39, (2008) · Zbl 1160.68678
[8] Clarke, E.; Emerson, E.; Sistla, A., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM transactions on programming languages and systems, 8, 2, 244-263, (1986) · Zbl 0591.68027
[9] Gilbert, D.; Heiner, M.; Lehrack, S., A unifying framework for modelling and analysing biochemical pathways using Petri nets, ()
[10] Gillespie, G.T., Exact stochastic simulation of coupled chemical reactions, J. phys. chem., 81, 25, 2340-2361, (1977)
[11] Hansson, H.A.; Jonsson, B., A framework for reasoning about time and reliability, (), 102-111
[12] Hoops, S.; Sahle, S.; Gauges, R.; Lee, C.; Pahle, J.; Simus, N.; Singhal, M.; Xu, L.; Mendes, P.; Kummer, U., COPASI — a complex pathway simulator, Bioinformatics, 22, 3067-3074, (2006)
[13] Heath, John; Kwiatkowska, Marta; Norman, Gethin; Parker, Dave; Tymchyshyn, Oksana, Probabilistic model checking of complex biological pathways, Theoretical computer science, 391, 239-257, (2008) · Zbl 1133.68043
[14] Foundations of systems biology, ()
[15] Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic symbolic model checking with probabilistic symbolic model checking with \scprism, () · Zbl 1043.68576
[16] Marsan, M.A.; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with generalized stochastic Petri nets, (1995), Wiley · Zbl 0843.68080
[17] Sedwards, S.; Mazza, T., Cyto-sim: A formal language model and stochastic simulator of membrane-enclosed biochemical processes, Bioinformatics, (2007)
[18] Sible, J.C.; Tyson, J.J., Mathematical modeling as a tool for for investigating cell cycle control networks, Methods, 41, 238-247, (2007)
[19] Stewart, W.J., Introduction to numerical solution of Markov chains, (1994), Princeton · Zbl 0821.65099
[20] Volterra, V., Variations and fluctuations of the number of individuals in animal species living together, Animal ecology, (1931)
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.