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 alpharobustness, 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 dualchamber pacemaker that can interact with the model of the heart. Then, we model a gene regulatory network, namely the Lac Operon of Escherichia Coli.
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 alpharobustness, 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 dualchamber pacemaker that can interact with the model of the heart. Then, we model a gene regulatory network, namely the Lac Operon of Escherichia Coli.
Formal Models for Biological Systems / Desiree Manicardi , 2024 May 22. 36. ciclo, Anno Accademico 2022/2023.
Formal Models for Biological Systems
MANICARDI, DESIREE
20240522
Abstract
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 alpharobustness, 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 dualchamber pacemaker that can interact with the model of the heart. Then, we model a gene regulatory network, namely the Lac Operon of Escherichia Coli.File  Dimensione  Formato  

manicardiPhDthesis.pdf
accesso aperto
Descrizione: Formal Models for Biological Systems
Tipologia:
Tesi di dottorato
Dimensione
1.61 MB
Formato
Adobe PDF

1.61 MB  Adobe PDF  Visualizza/Apri 
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.