Formal Modeling and Simulation of Biological Systems with Delays

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