Scatena, Guido (2011) Abstract probabilistic semantics for the analysis of biological systems models. Advisor: Barbuti, Prof. Roberto. Coadvisor: Levi, Prof. Francesca . pp. 167. [IMT PhD Thesis]
|
Text
Scatena_phdthesis.pdf - Published Version Available under License Creative Commons Attribution No Derivatives. Download (2MB) | Preview |
Abstract
This Thesis concerns the development of probabilistic semantics tailored to model the dynamic behavior of biological systems in order to formally analyze them. More specifically, it attempts to overcome problems, related to uncertainty and to the state space explosion, inherent to models describing biological systems. Recently, many formalisms originated from Computer Science have been successfully applied to describe biological systems. Many of these formalisms include probabilistic aspects, and techniques like stochastic simulation and probabilistic model checking have been proposed to study biological systems properties. However, the practical application of formal analysis tools in this context is still limited. The size of state space associated with models is often prohibitively large. Moreover, the knowledge of biological processes is often incomplete, resulting in models with uncertain parameters. For these reasons the application of available Computer Science tools is often difficult. In addition, usual tools deal with models in which concurrency is described by interleaving semantics. However, interleaving is not suitable for modelling certain classes of biological systems. To overcome these problems, in this Thesis, we propose to apply abstraction techniques to probabilistic semantics of biological systems models. The application of such techniques presents several advantages. On one hand, these techniques can help in reducing the state space associated to models. On the other hand, they can help in handling models with uncertainty. About the management of uncertainty in models, we consider the uncertainty in stochastic parameters. Often, having incomplete knowledge of the kinetics of a system, we are not able to choose among models differing only for parameters. Hence, we define a framework to study models with parameters expressed as intervals, obtaining results that hold for all models with parameters included in the specified intervals. In more detail, probabilistic model checking can be performed on biochemical reactions systems models when kinetic rates, expressing the propensity of the interaction events, are not expressed precisely as point values, but as intervals. We define an effective method to derive an abstract semantics for such models and to obtain conservative bounds on probability of reachability properties. The abstract semantics, given in terms of Interval Markov Chain (IMC), is derived from a Labeled Transition System (LTS) semantics. It is proven to be correct, by means of abstract interpretation techniques, with respect to the Discrete Time Markov Chain (DTMC) semantics, usually associated with these systems. As example of application, we study how the behavior of a model of tumor cell growth changes when different intervals of kinetic rates are used. Subsequently, we face the problems related to the use of interleaving semantics and to the size of state space size of models. In particular, we define the probabilistic semantics for systems evolving in a maximally parallel way: in each step of the system evolution, as many interactions happen synchronously. Using the proposed semantics we are able to reproduce in vivo experiments outcomes on a model of C. elegans vulval development. Moreover, we develop an abstraction framework for the proposed maximally parallel probabilistic semantics. The framework is based on a form of predicate abstraction computing an abstract semantics in terms of IMC. Since the abstraction is parametric on a set of predicates, the abstract probabilistic model can be refined until a right compromise between dimension and precision is reached. We prove that conservative bounds on probabilities of reachability properties of systems evolving in a maximally parallel way can be computed on the abstract semantics. We show the efficacy of the approach, in terms of state and transition number reduction, by analysis probabilistic reachability on a simple model of seasonal animal reproduction.
| Item Type: | IMT PhD Thesis |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| PhD Course: | Computer Science and Engineering |
| Identification Number: | https://doi.org/10.6092/imtlucca/e-theses/31 |
| NBN Number: | urn:nbn:it:imtlucca-27067 |
| Date Deposited: | 10 Jul 2012 14:00 |
| URI: | http://e-theses.imtlucca.it/id/eprint/31 |
Actions (login required, only for staff repository)
 |
View Item |
