Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking

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 modelchecking 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. This is the preliminary version of a paper that was published in the Proceedings of the International Workshop From Biology To Concurrency and back (FBTC 2008), satellite workshop of ICALP 2008, July 12, 2008, Reykjavik, Iceland, ENTCS 194(3). The original publication is available at DOI:10.1016/j.entcs.2009.02.002