ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-06152011-113458


Tipo di tesi
Tesi di dottorato di ricerca
Autore
CARAVAGNA, GIULIO
URN
etd-06152011-113458
Titolo
Formal Modeling and Simulation of Biological Systems with Delays
Settore scientifico disciplinare
INF/01
Corso di studi
INFORMATICA
Relatori
tutor Prof. Barbuti, Roberto
relatore Dott. Milazzo, Paolo
Parole chiave
  • Stochastic Simulation
  • Process Algebras
  • non-Markov Processes
  • Master Equations
  • Gillespie Algorithm
  • Systems Biology
Data inizio appello
21/06/2011
Consultabilità
Completa
Riassunto
Delays in biological systems may be used to model events for which the
underlying dynamics cannot be precisely observed, or to provide abstraction
of some behavior of the system resulting in more compact models. Deterministic modeling
of biological systems with delays is usually based on Delay Differential Equations
(DDEs), an extension of ordinary ones where the derivative of the unknown function depends on past-states of the system. Stochastic modeling is done by using non-Markovian stochastic processes, namely processes whose sojourn time in a state and the probability of a transition are not necessarily
exponentially distributed. Moreover, in the literature Delay Stochastic Simulation Algorithms
(DSSAs) have been proposed as extension of a well-known Stochastic Simulation Algorithm
(SSA) for non-delayed models.

In the first part of the thesis we study different DSSAs. The first two algorithms we present treat delays by means of some scheduling policy. One algorithm is based on the idea of
``delays as durations'' approach (DDA), the other is based on a ``purely delayed''
interpretation (PDA) of delays. We perform deterministic and stochastic analysis of
a cell cycle model. Results suggest that the algorithms differ in the sense that
the PDA, even in a naive definition, is more suitable than the DDA to model systems in which species involved in a delayed interaction can be involved at the same time in other interactions. We investigate the mathematical foundations of the algorithms by means of the associated Delay Chemical Master Equations (DCMEs). Result of the comparison is that both are correct with respect to their DCMEs, but they refer to systems ruled by different DCMEs. These results endorse our intuition on the difference between the algorithms. Improvements of the naive PDA lead to a definition of
a more precise algorithm, the PDA with markings, which is finally combined with the DDA.

The last algorithm we propose, the DSSA with Delayed Propensity Functions (DPF),
is inspired by DDEs in its definition. In the DPF changes in the current state of the system are
affected by the history of the system. We prove this algorithm to be correct, we show
that systems ruled by the DCME associated with this algorithm are the same ruled by those target
of the PDA, and then argue that the DPF and the PDA are equivalent.


We then study formal models of biological systems with delays. Initially, we start adding delayed actions to CCS. This leads to two new algebras, CCSd and CCSp, the former where actions follow the DDA{}, the latter where actions follow the PDA{}. For both the algebras we define a notion of process, process configurations, and we give a Structural Operational Semantics (SOS) in the Starting-Terminating (ST) style, meaning that the start and the completion of an action are observed as two separate events, as required by
actions with delays. We define bisimulations in both CCSd and CCSp, and we prove bisimulations
to be congruences even in the case of delayed actions.

Finally, we enrich the stochastic process algebra BioPEPA with the possibility of assigning DDA -like delays to actions, yielding a new non-Markovian stochastic process algebra: BioPEPAd. This is a conservative extension meaning that the original syntax of BioPEPA is retained and moving from existing BioPEPA models to models with delays is straightforward. We define process configurations and a SOS in the ST-style for BioPEPAd. We formally define the encoding of BioPEPAd models in Generalized semi-Markov Processes (GSMPs), a class of non-Markov processes, in input for the DDA and in sets of DDEs. Finally, we investigate the relation between
BioPEPA and BioPEPAd models.
File