Formal Models for Biological Systems

In the last thirty years, formal models have been thoroughly employed in the realm of biological systems for many reasons: (i) preventing those ambiguities that may arise when informal notations are used for system description, (ii) supporting the development of simulators, (iii) supporting the development of tools, such as model checkers, allowing for verifying whether a system satisfies a given behavioural property, (iv) offering several instruments allowing for comparing the behaviour of different systems. The work in this thesis can be divided into two contributions concerning formal models for biological systems. The first contribution is related to the study of the robustness of biochemical networks. In particular, we take inspiration from the notion of alpha-robustness, which, intuitively, verifies how by varying the initial concentration of some species, called conventionally the input species, the concentration of other species of interest, called the output species, varies at steady state. Robustness in our sense captures random effects and temporary effects that are typical of the stochastic model. We will employ: (i) the process calculi approach for specifying systems of interest, (ii) the semantic model of evolution sequences, which, intuitively, model the behaviour of a system as the sequence of probability measures over the attainable configurations, (iii) a formal notion of robustness, defined on the semantic model, and (iv) an algorithm allowing us to estimate the robustness of a system starting from its specification. We validate our approach on three case studies EnvZ/OmpR Osmoregulatory Signaling System in Escherichia Coli, which is an example of the regulatory network, the mechanism of Bacterial Chemotaxis of Escherichia Coli, and an abstract chemical reaction network, called Enzyme Activity at Saturation. We have provided a Python implementation available at https://github.com/dmanicardi/spebnr. Our second contribution is showing how the features of CospanSpan(Graph) can be exploited in modelling biological systems. CospanSpan(Graph) offers an algebraic approach for the compositional description of variable topology networks that has been only partially exploited so far for the formalisation of that kind of systems. In particular, we provide a simplified model of a human heart and a model of a dual-chamber pacemaker that can interact with the model of the heart. Then, we model a gene regulatory network, namely the Lac Operon of Escherichia Coli.