Catálogo de publicaciones - libros

The Brane Calculus is a calculus of mobile processes, intended to model the transport machinery of a cell system. In this paper, we introduce the , a modal logic for expressing formally properties about systems in Brane Calculus. Similarly to previous logics for mobile ambients, Brane Logic has specific spatial and temporal modalities. Moreover, since in Brane Calculus the activity resides on membrane surfaces and not inside membranes, we need to add a specific logic (akin Hennessy-Milner’s) for reasoning about membrane activity.

We present also a proof system for deriving valid sequents in Brane Logic. Finally, we present a model checker for a decidable fragment of this logic.

Brane calculi are a family of biologically inspired process calculi proposed in [5] for modeling the interactions of dynamically nested membranes and small molecules.

Building on the decidability of divergence for the fragment with , and operations in [1], in this paper we extend the decidability results to a broader class of properties and to larger set of interaction primitives. More precisely, we provide the decidability of divergence, control state maintainabiliy, inevitability and boundedness properties for the calculus with molecules and without the operation.

Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway.

Type checking and type inference are important concepts and methods of programming languages and software engineering. Type checking is a way to ensure some level of consistency, depending on the type system, in large programs and in complex assemblies of software components. Type inference provides powerful static analyses of pre-existing programs without types, and facilitates the use of type systems by freeing the user from entering type information. In this paper, we investigate the application of these concepts to systems biology. More specifically, we consider the Systems Biology Markup Language SBML and the Biochemical Abstract Machine BIOCHAM with their repositories of models of biochemical systems. We study three type systems: one for checking or inferring the functions of proteins in a reaction model, one for checking or inferring the activation and inhibition effects of proteins in a reaction model, and another one for checking or inferring the topology of compartments or locations. We show that the framework of abstract interpretation elegantly applies to the formalization of these abstractions and to the implementation of linear time type checking as well as type inference algorithms. Through some examples, we show that the analysis of biochemical models by type inference provides accurate and useful information. Interestingly, such a mathematical formalization of the abstractions used in systems biology already provides some guidelines for the extensions of biochemical reaction rule languages.

Starting from a biochemical signalling pathway model expressed in a process algebra enriched with quantitative information we automatically derive both continuous-space and discrete-state representations suitable for numerical evaluation. We compare results obtained using implicit numerical differentiation formulae to those obtained using approximate stochastic simulation thereby exposing a flaw in the use of the differentiation procedure producing misleading results.

Drugs are small molecules designed to regulate the activity of specific biological receptors. Design new drugs is long and expensive, because modifying the behavior of a receptor may have unpredicted side effects. Two paradigms aim to speed up the drug discovery process: molecular docking estimates if two molecules can bind, to predict unwanted interactions; systems biology studies the effects of pharmacological intervention from a system perspective, to identify pathways related to the disease. In this paper we start from process calculi theory to integrate information from molecular docking into systems biology paradigm. In particular, we introduce Beta-binders, a process calculus for representing molecular complexation driven by the shape of the ligands involved and the subsequent molecular changes.

We analyse an enhanced specification of VICE, a hypothetical prokaryote with a genome as basic as possible. Besides the most common metabolic pathways of prokaryotes in interphase, VICE also posseses a regulatory feedback circuit based on the enzyme phosphofructokinase. We use as formal description language a fragment of the stochastic -calculus. Simulations are run on BEAST, an abstract machine specially tailored to run experimentations. Two kinds of virtual experiments have been carried out, depending on the way nutrients are supplied to VICE. The result of our experimentations confirm that our virtual cell “survives” in an optimal environment, as it exhibits the homeostatic property similary to real living cells. Additionally, oscillatory patterns in the concentration of fructose-6-phosphate and fructose-1,6-bisphosphate show up, similar to the real ones.

Membrane systems were introduced as models of computation inspired by the structure and functioning of biological cells. Recently, membrane systems have also been shown to be suitable to model cellular processes. We introduce a new model called . The model has compartments enclosed by membranes, floating objects, objects associated to the internal and external surfaces of the membranes and also objects integral to the membranes. The floating objects can be processed within the compartments and can interact with the objects associated to the membranes. The model can be used to represent cellular processes that involve compartments, surface and integral membrane proteins, transport and processing of chemical substances. As examples we model a circadian clock and the G-protein cycle in yeast and present a quantitative analysis using an implemented simulator.

In order to understand complex genetic regulatory networks researchers require automated formal modelling techniques that provide appropriate analysis tools. In this paper we propose a new qualitative model for genetic regulatory networks based on Petri nets and detail a process for automatically constructing these models using logic minimization. We take as our starting point the Boolean network approach in which regulatory entities are viewed abstractly as binary switches. The idea is to extract terms representing a Boolean network using logic minimization and to then directly translate these terms into appropriate Petri net control structures. The resulting compact Petri net model addresses a number of shortcomings associated with Boolean networks and is particularly suited to analysis using the wide range of Petri net tools. We demonstrate our approach by presenting a detailed case study in which the genetic regulatory network underlying the nutritional stress response in is modelled and analysed.

This paper presents a method for regulatory network reconstruction from experimental data. We propose a mathematical model for regulatory interactions, based on the work of Thomas et al. [25] extended with a stochastic element and provide an algorithm for reconstruction of such models from gene expression time series. We examine mathematical properties of the model and the reconstruction algorithm and test it on expression profiles obtained from numerical simulation of known regulatory networks. We compare the reconstructed networks with the ones reconstructed from the same data using Dynamic Bayesian Networks and show that in these cases our method provides the same or better results. The supplemental materials to this article are available from the website