The development of detailed, coherent, models of complex biological systems is recognized as a key requirement for integrating the increasing amount of experimental data. In addition, in-silico simulation of bio-chemical models provides an easy way to test different experimental conditions, helping in the discovery of the dynamics that regulate biological systems. However, the computational power required by these simulations often exceeds that available on common desktop computers and thus expensive high performance computing solutions are required. An emerging alternative is represented by General-Purpose scientific computing on Graphics Processing Units (GPGPU), which offers the power of a small computer cluster at a cost of around $400. Computing with a GPU requires the development of specific algorithms, since the programming paradigm substantially differs from traditional CPU-based computing. In this paper, we review some recent efforts in exploiting the processing power of GPUs for the simulation of biological systems.
Download Technical Report

We modelled and simulated with software Redi (Reaction-Diffusion simulator) the observed gradient of the bicoid protein in the Drosophila Melanogaster embryo. We reproduced with an accuracy of 1% its experimental spatio-temporal dynamics, as recorded in a time-lapse experiment obtained by direct measurements of transgenic bicoid-enhanced green fluorescent protein. We characterized the dynamic properties of the bicoid gradient, such as predicting the kinetic rate of production and degradation, and range of variability of the average diffusion coefficient.
Download Technical Report

In this paper we introduce Continuous Markovian Logic (CML), a simple formalism inspired by coalgebraic logic, to characterize the bisimulation of Markov processes having continuous state space and continuous temporal evolution (CMPs). The alternative, continuous stochastic logic (CSL), has expressive power which comes at the price of a complicated two-layer semantics and requires a complex mathematical apparatus for calculating the probabilities of computational paths in time. CML focuses on the rates of the exponentially distributed random variables that characterize the duration of transitions, instead of explicitly expressing time-dependent probabilistic information as in the case of CSL. Thus, CML exploits the fact that the probabilistic-temporal information is encapsulated in the rates. We prove that the negation-free fragment of CML is already suficient to completely characterize bisimulation of CMPs. We also show a sound-complete axiomatization of CML and demonstrate that, unlike CSL, it enjoys the small model property.
Download Technical Report

We introduce a stochastic extension of CCS based on the mass action law and endowed with a structural operational semantics expressed in terms of measure theory. The measurable space of processes is defined for the sigma-algebra of structural congruence-closed sets. The structural operational semantics associates to each process an action-indexed class of measures over the space of processes. These compute the rates of the transitions from a state of a system to a measurable set of states. In this setting, we prove that stochastic bisimulation is a congruence that extends structural congruence.
Download Technical Report

We present CoSBiLab Graph 1.0, the freely available network visualisation and analysis module of CoSBiLab (http://www.cosbi.eu). Most of available network analysis softwares are developed by either sociologists or (molecular) systems biologists: our purpose was to create a tool that is designed by considering ecological principles but general enough for supporting multidisciplinary research. It offers classical (e.g. status) and new (e.g. trophic overlap) network indices, as well as provides a fast and comfortable environment for network ecologists. Instead of competing, we aim to cooperate with other existing softwares, by providing compatible input and output and focusing on what is missing in other applications. The key features of this software are (1) the customisable layout, representing node attributes, (2) the implementation of novel network indices and (3) the rich linkage to other modules of the CoSBiLab platform (tools for modelling reaction-diffusion systems, stochastic dynamical simulators, statistical analyis and parameter inference).
Download Technical Report

It is a key problem in current biology how to better understand the hierarchical organization of biological systems. One way how to model this is studying interactive networks representing interactions among entities at different organizational levels. Here we build a three-level network model, linking (1) a social network of individuals characterizing a species, (2) a food web of species describing a local community and (3) a spatial network of communities abstracting an ecosystem. We use the BlenX language for the structural description and the dynamical simulation of the network. This language was originally defined for the study of biochemical networks and here we investigate its expressive and analysis power in the context of ecological systems. In particular, the BlenX language, as process algebras in general, offers an alternative approach with respect to standard methods based on differential equations and graph analysis. The key question analysed is whether bottom-up (from individuals) or top-down (from the ecosystem) changes will influence more community dynamics (at the intermediate level). In order to answer these questions, we consider a stochastic framework. Stochastic simulation is appropriate in this study, since our model describes a fragmented population characterized by a certain variability.
Download Technical Report

There is a lot of information on genes causing diseases, also on the total genome and proteome. A systems biological perspective makes it possible to evaluate the roles individual genes play (and their relative importance) in the context of the whole system. Based on the i2d and OMIM databases, we have constructed (1) a total human protein network, (2) a protein network of genes causing five selected diseases plus their interacting partners (IP) and (3) a protein network of these IPs. The five diseases were (1) various cancers, (2) heart diseases, (3) obesity, (4) autism and (5) diabetes. We have quantified the number and strength of IP network-mediated indirect effects between the five groups of disease genes and identified the most important mediators in the IP network. The main contribution of this work is twofold. We firstly illustrate that understanding the role and importance of individual genes highly depends on how to define the network of study. We secondly present new findings of the most important ``hidden mediators``: proteins seemingly unimportant but playing key roles in the mutual effects among diseases
Download Technical Report

Recent innovations in experimental techniques on single molecule detection resulted in advances in the quantification of molecular noise in several systems, and provide suitable data for defining stochastic computational models of biological processes. Some of the latest stochastic models of cell cycle regulation analyzed the effect of noise on cell cycle variability. In their study, Kar et al. (Proc Natl Acad Sci U S A (2009) 106: 6471-6) found that the observed variances of cell cycle time and cell division size distributions cannot be matched with the measured long half-lives of mRNAs. Here, we investigate through modeling and simulation how the noise created by the transcription and degradation processes of a key cell cycle controller mRNA affect the statistics of cycle time and cell mass at division. Our model basically consists of an encoding of the model of Kar et al. into a stochastic Petri net, with the extensions necessary to represent multiple synthesis (gestation) and degradation (senescence) steps in the regulation of mRNAs. We found that few steps of gestation and senescence of mRNA’s are enough to give a good match for both the measured half-lives and variances. This result suggests that the complex process of transcription can be more accurately approximated by a multi-step linear process.
Download Technical Report

The process through which disordered components spontaneously arrange themselves into patterns is called self-assembly. Molecular self-assembly describes the process by which molecules adopt a defined arrangement without external guidance (e.g. formation of membranes and protein complexes). These biological processes are essential to the functioning of cells. We investigate the usage of BlenX, a process calculi based programming language, for modelling molecular self-assembly of filaments, trees and rings. Moreover, we show how these structures can be used to model actin polymerization.
Download Technical Report

The problem we deal with is the analysis of a class of large structured Markov chains. In particular we assume that the whole state space can be partitioned into disjoint sets (called macro states) in which the process corresponds to the parallel execution of independent jobs. Petri nets and process algebras with phase type (PH) distributed execution times give rise to this kind of model. These models are subject to the phenomenon of state space explosion. It is known that the infinitesimal generator of such models can be handled in a memory efficient way by storing only the structure of the infinitesimal generator as Kronecker expressions or decision diagrams. Less is known instead on how to perform the analysis of the model in a memory efficient manner because in case of most of the available methods the vector of transient or steady state probabilities are stored in an explicit manner. In this paper we consider the calculation of measures connected to the probability that the process passes through a given series of macrostates. We show that such measures can be calculated in a memory efficient manner by Laplace transform techniques. The method is illustrated by numerical examples.
Download Technical Report

In this paper we present an extensible framework that aims at making the process of understanding the results obtained by a formal language model easier, by using visualization techniques. The final goal is to have a powerful way of expressing biological models thanks to formal languages techniques united to the familiarity and easiness of pictures, cartoons and graphical representations to interpret them. The framework is general, and can be applied to several problems in which visualization of data in the form of a graph is needed. It is also modular, so that parts of it can be taken and used for different purposes. We present a practical application of this framework, namely the visualization of BlenX complexes produced as a result of the static analysis or of the dynamic simulation of BlenX models.
Download Technical Report

The paper is a survey that follows the idea of using approximated methods for quantitative Model Checking. The paper focuses mainly on Monte Carlo algorithms used to solve model checking problems for stochastic systems
Download Technical Report

Harsanyi type spaces are general probabilistic structures that have been used as semantics for probabilistic logics, as, for example, with the Aumann system. These type spaces generalize several probabilistic models, such as generative probabilistic automata, labelled Markov processes and, in general, probabilistic transition systems. In this paper we define compositionality over the class of type spaces, enabling it with an algebraic structure that encodes a general notion of synchronization of type spaces. The algebra of type spaces is used as semantics for a logic that extends the Aumann system with structural operators. Using this logic, modular and concurrent probabilistic properties of type spaces can be expressed. This logic can thus be seen as a probabilistic extension of spatial or separation logic as well as a structural extension of probabilistic logic. We present a complete axiomatization and prove the finite model property.
Download Technical Report

In this technical report we first review the key features of chaotic systems, then we show the relevance of chaos in deterministic O. D. E. models of biochemical networks, and finally we propose a method to disclose the presence of deterministic chaos in a system from incomplete experimental data.
Download Technical Report

Proteins have the ability to bind other molecules and to consequently change shape, i.e., interaction capabilities. This basic mechanism enables complex cellular functions that make life possible. Upon this observation, the idea of a protein-based computing device is fascinating, but using real proteins in a lab to execute programs is not yet feasible. Here, our purpose is to explore the computational power of a similar device by simulating protein behaviour through a formal representation. In particular, we refer to the programming language BlenX, designed on the basic protein mechanisms, to sketch the idea of using proteins to encode term rewriting systems.
Download Technical Report

Methods for parameter estimation, that are robust to the experimental uncertainties, stochastic and biological noise and requiring a minimum a priori input knowledge, are of key importance in computational systems biology. Moreover, in the ambit of dynamic modelling and analysis of biochemical networks, a model-based approach in the experimental design is attracting the attention and challenging the efforts of the theoreticians and experimentalists in developing mathematical models of parameter and data inference that can be used to estimate the accuracy of an experimental outcome, and, eventually guide experimental procedure to increase it In this paper we present present a method for deducing kinetic rates, their variance measures and their region of confidence from noisy time series of concentration. This new method was applied to a challenging parameter estimation problems of nonlinear dynamic biological systems: the twelve-state model of the SERCA pump.
Download Technical Report

Discovering the human genes that cause disease (or ``disease genes") is one of the emerging tasks in bioinformatics and biomedicine. In many ongoing research projects, protein-protein interaction networks (PPI) are being exploited in the discovery process, because there is a complex interplay between disease genes and PPI. Most current PPI-based methods only employ data regarding well-known disease genes, using supervised learning. However, there is a lot of valuable data containing information about unknown genes which could potentially enhance disease gene predictions. Combining multiple data sources for both known disease genes and unknown genes is expected to better predict which genes are likely to be disease genes. We have developed a novel method to effectively predict disease genes, by taking advantage of the wealth of existing data which may contain information about unknown genes. To this end, our method makes the best of semi-supervised learning, integrating data of human protein-protein interactions and various biological data extracted from multiple proteomic/genomic data sources. An experimental evaluation demonstrated that our proposed method outperformed other methods in terms of several measures including sensitivity, specificity, precision, accuracy, and a balanced F-score. A considerable number of potential disease genes were discovered and initially validated.
Download Technical Report

We present here a new method for estimating rate coefficients from noisy observations of concentration levels at discrete time points. The inference procedure is based on a probabilistic model of the variations in reactant concentration and it estimates the rate coefficients, the level of noise and an error range on the estimates of rate constants. Its probabilistic formulation is key to a principled handling of the noise inherent in biological data. We apply the inference model implemented by KInfer on real experimental data for deducing the "binding affinity" of the enzyme (Inhibitor kappa B kinase) to its substrate (inhibitor kappa B alpha), an integral part of the transduction of signals in the NF-kappa B signalling pathway.
Download Technical Report

To further understand the complexity of biological processes and decipher the mechanisms that lead to healthy or diseased organisms, it is important to consider protein functions in the context of complex molecular networks. This is because most diseases cannot be explained by one genetic mutation or the action of a single gene product or pathway. The vast amount of data on molecular structure, interaction and activity information being acquired provides a picture of intricate molecular networks that underlie biological function. This ever growing amount of data demands we adopt powerful computational techniques for analysing and interpreting content that is not immediately intelligible to the scientist. Whereas traditional statistics-based methods test a priori hypothesis against data, data mining strives to discover new, previously unknown and hidden patterns in large data sets; and then tries to represent and interpret these patterns in an intelligible way. Ultimately, effective data-driven dynamic modelling of molecular networks will play a pivotal role in the conversion of data to knowledge and permit detailed understanding into how protein interacts to form healthy or diseased pathways. Here we describe a methodology for guiding computational modelling of molecular networks - in particular, the p53 and NF-kappaB systems - useful for capturing different aspects of network dynamics by uncovering the behaviour of molecular species and their combinatorial interactions.
Download Technical Report

Biological systems are characterised by a large number of interacting entities whose dynamics is described by a number of reaction equations. Mathematical methods for modelling biological systems are mostly based on a centralised solution approach: the modelled system is described as a whole and the solution technique, normally the integration of a system of ODEs or the simulation of a stochastic model, is commonly computed in a centralised fashion. In recent times research efforts moved towards the definition of parallel/distributed algorithms as a means to tackle the complexity of biological models analysis. In this paper we present a survey on the progresses of such parallelization efforts describing the most promising results so far obtained.
Download Technical Report

Network analysis examines the role of different species in ecological communities. This can be achieved by several indices designed to quantify the topological position of a given species, each index emphasizing a different aspect of node centrality. Comparison of the rank order of species produced by these indices can help in understanding community organization, and also in revealing the relationships among indices. However, the rank orders disregard absolute differences between the importance values of species and therefore ranking may not completely reveal the quantitative information contained within food web data. To evaluate the consequences of differences between indices, we compared the rank order of species obtained by different node centrality indices and also the distributions of these indices, using data from six different food webs. Robust patterns emerged from the examination of similarities in rank orders, but distributions changed greatly with food web structure. This implies that the combined analysis of rank orders and distributions of centrality indices provides more information on species importance and could better serve ecologists in looking for topological keystone species.
Download Technical Report

In the last decades, many works investigated the trophic structure of communities stressing, in particular, the position of species in food webs (e.g. their trophic level and, more recently, their centrality). Despite encouraging applications on binary food web data, and the acknowledged need of studying weighted webs, we do not yet know too much about the relationship between undirected centrality measures and directed trophic height. Here we aim to contribute to the synthetic treatment of these complementary issues by studying the relationship between several indices of centrality and trophic position. Studying 19 ecosystems, we ranked the nodes according to their positional importance values (based on various centrality indices) and we compared the rank order of coefficients with various measurements of trophic position. We aimed to reveal potential biases of finding high centrality nodes among basal, intermediate and top species. Finally, we discuss the consequences of observed features on ecosystem dynamics.
Download Technical Report

Simulation is a simple means to investigate chemically reacting systems. In a deterministic framework, the evolution of concentration in time produced by numerically solving a set of differential equations can be seen to directly characterize an average behaviour. In a stochastic context, multiple simulation traces are required to produce an average with reasonable confidence, however the noise contains other useful information about the system. This report presents a new technique to extract useful information from simulation traces using Fourier analysis. The technique may be used with deterministic traces but is particularly effective when applied to stochastic simulations. Three statistical measures are defined over the frequency spectra of accumulated simulation traces, which may be used to characterise typical simulated behaviour. Two are independent measures of stochasticity while the third measures the distance between simulations, thus creating a space which may be used to compare models or simulation algorithms, for example. Concrete instances of the use of these techniques are presented in relation to characterising the viability of various mutant strains of budding yeast
Download Technical Report

Cell cycle control models used in biology involve complex biochemical kinetics of proteins, proteins kinases, and regulatory subunits, and many parameters with unknown values. The values of the parameters strongly affect the dynamics of the system and the accuracy of its model in representing the real biological behavior. Post-transcriptional mechanisms involving gene transcripts and proteins are key processes for the cell cycle control machinery. In this paper we describe how to model and infer from micro-array data, the cyclin-induced oscillations of the Cdc20 transcript, that codes for the cyclin antagonist in the cell cycle control network.
Download Technical Report

The aim of this paper is to summarize and review the main conceptual frameworks in which models of biochemical networks can be developed. In particular, we review the stochastic molecular modelling approaches, by mentioning the principal conceptualizations suggested by P. Langevin, D. T. Gillespie, N. G. van Kampfen, and recently by D. Wilkinson, and by the author.
Download Technical Report

Many systems can be described in terms of networks with characteristic structural properties. To better understand the formation and the dynamics of complex networks one can develop generative models. We propose here a generative model (named dynamic spatial game) that combines graph transformations and game theory. The idea is that a complex network is obtained by a sequence of node-based transformations determined by the interactions of nodes present in the network. We model the node-based transformations by using graph grammars and the interactions between the nodes by using game theory. We illustrate dynamic spatial games on a couple of examples: the role of cooperation in tissue formation and tumor development and the emergence of patterns during the formation of ecological networks.
Download Technical Report

Appropriately formulated quantitative computational models can support researchers in understanding the dynamic behaviour of biological pathways and support hypothesis formulation and selection by “in silico” experimentation. An obstacle to widespread adoption of this approach is the requirement to formulate a biological pathway as machine executable computer code. We have proposed a novel, biologically intuitive, narrative-style modelling language for biologists to formulate the pathway which is then automatically translated into an executable format. We introduce this approach by presenting a computational model of the gp130/JAK/STAT signalling pathway derived from a biological narrative and show that the model reproduces the dynamic behaviour of the pathway derived by biological observation. We then “experiment” on the model by simulation and sensitivity analysis to define those parameters which dominate the dynamic behaviour of the pathway. The model predicts that nuclear compartmentalisation and phosphorylation status of STAT are key determinants of the pathway and that alternative mechanisms of signal attenuation exert their influence on different timescales.
Download Technical Report

Cells life follows a cycling behaviour which starts at cell birth and leads to cell division through a number of distinct phases. The transitions through the various cell cycle phases are controlled by a complex network of signalling pathways. Many cell cycle transitions are irreversible: once they are started they must reach completion. In this study we investigate the existence of conditions which lead to cases when irreversibility may be broken. Specifically, we characterise the elements of the cell cycle signalling network that are responsible for the irreversibility and we determine conditions for which the irreversible transitions may become reversible. We illustrate our results through a formal approach in which stochastic simulation analysis and model checking verification are combined. Through probabilistic model checking we provide a quantitative measure for the probability of irreversibility in the ``Start" transition of the cell cycle.
Download Technical Report

Spatial Logics are modal logics developed for process-algebraic semantics. They have been proposed for specifying concurrent properties of dynamic systems and have been proved useful in a wide range of applications. Their expresivity often comes with the price of undecidability, however, even against finite fragments of process calculi. This paper investigates the decidability of satisfiability, validity, and model checking for various Spatial Logics against semantics based on a fragment of CCS that embodies the core features of concurrent behaviors. We prove some decidability and undecidability prop- erties for (combinations of) basic modal operators of spatial logics that entail some of the already known results in the field and provide a taxonomy for this class of problems.
Download Technical Report

The process-based Spatial Logics are multi-modal logics de- veloped for semantics on Process Algebras and designed to specify con- current properties of dynamic systems. On the syntactic level, they com- bine modal operators similar to operators of Hennessy-Milner logic, dy- namic logic, arrow logic, relevant logic, or linear logic. This combina- tion generates expressive logics, sometimes undecidable, for which a wide range of applications have been proposed. In the literature, there exist some sound proof systems for spatial logics, but the problem of completeness against process-algebraic semantics is still open. The main goal of this paper is to identify a sound-complete axiomatization for such a logic. We focus on a particular spatial logic that combines the basic spatial operators with dynamic and classical operators. The semantics is based on a fragment of CCS calculus that embodies the core features of concurrent behaviors. We prove the logic decidable both for satisfiability/validity and mode-checking, and we pro- pose a sound-complete Hilbert-style axiomatic system for it.
Download Technical Report

The convergence between computer science and biology occurred in successive waves involving deeper and deeper concepts of computing. The current status makes computer science a suitable candidate to become a philosophical foundation for systems biology with the same importance as mathematics, chemistry and physics. However, this great opportunity is not a free lunch. New development and a strong integration of different fields of computing are needed to cope with the challenges of systems biology: a complex and expanding applicative domain that can open completely new avenues of research in computing and eventually help it become a natural, quantitative science.
Download Technical Report

In this report we review the Riedel-Bruck stochastic simulation algorithm, which makes use of a cycle-leaping strategy to improve the simulation performance. We implemented the algorithmi and tested our implementation on some stochastic models, such as the Lotka-Volterra model of predation, the Brusselator model, and the Michaelis-Menten model of enzymatic catalysis. We discuss the advantages and the disadvantages of this algorithm from the viewpoint of its use in a systemic approach to modeling and simulation of biochemical and biological processes.
Download Technical Report

Recently process calculi have been used to model biological systems. We use the process calculi-based language BlenX to develop executable models starting from the composition of the description of the molecules involved in the system. BlenX programs can be run through a stochastic run-time that makes the molecules interact together, mimicking different kinds of reactions. The goal of the paper is to extract from BlenX programs a description of the same system based on chemical reactions that can be executed through chemical-based stochastic simulators. We present an algorithm that extracts the list of these reactions from the model definition given in BlenX. The translation is done without run- ning the system, but just analysing the model. The boxes in the BlenX models, used to represent molecules, often perform immediate actions (i.e. reactions with infinite rate) to change their internal state, some of which can be removed by the algorithm to optimize the model. The outcome of the algorithm is an SBML file that can be easily im- ported in SBML-supporting simulators that in some cases may run faster then executing BlenX programs due to model reduction and optimization. Furthermore, exporting our models in SBML allow us to share the models we develop in BlenX with the scientific community.
Download Technical Report

Dynamical models of inter- and intra-cellular processes contain the rate constants of the biochemical reactions. These kinetic parameters are often not accessible directly through experiments, but they can be inferred from time-resolved data. Time resolved data, that is, measurements of reactant concentration at series of time points, are usually affected by different types of error, whose source can be both experimental and biological. The noise in the input data makes the estimation of the model parameters a very difficult task, as if the inference method is not sufficiently robust to the noise, the resulting estimates are not reliable. Therefore "noise-robust" methods that estimate rate constants with the maximum precision and accuracy are needed. In this report we present the probabilistic generative model of parameter inference implemented by the software prototype KInfer and we show the ability of this tool of estimating the rate coefficients of models of biochemical network with a good accuracy even from very noisy input data.
Download Technical Report

In this report we present a new stochastic algorithm to simulate reaction-diffusion systems and its application to the simulation of spa- tial effects on the chaperone-assisted protein folding in cytoplasm.
Download Technical Report

Membrane systems with peripheral proteins are essentially standard membrane systems with the possibility of having multisets of objects (proteins) embedded in the membranes and with the presence of rules that control the transport and the change of configurations of these proteins. The model intends to abstract the activities of the receptors embedded in the cellular membranes. In this paper we use an extension of this paradigm to model and simulate some of the mechanisms underlying cell cycle and breast tumor growth. In particular we have defined a membrane system that abstracts the G2/M cell cycle phase transition and extends the corresponding Reactome model. The model has been then simulated by using the software Cyto-Sim and we have monitored the interplay between activators and inhibitors of the cell cycle.
Download Technical Report

In robust biological systems, wide deviations from highly controlled normal behavior may be rare, yet they may result in catastrophic complications. While in silico analysis has gained an appreciation as a tool to offer insights into systems-level properties of biological systems, analysis of such rare events provides a particularly challenging computational problem. This paper proposes an efficient stochastic simulation method to analyze rare events in biochemical systems. Our new approach can substantially increase the frequency of the rare events of interest by appropriately manipulating the underlying probability measure of the system, allowing high-precision results to be obtained with substantially fewer simulation runs than the conventional direct Monte Carlo simulation. Here, we show the algorithm of our new ap- proach, and we apply it to the analysis of rare deviant transitions of two systems, resulting in several orders of magnitude speedup in generating high-precision estimates compared with the conventional Monte Carlo simulation.
Download Technical Report

The estimation of parameter values (model calibration) is the bottleneck of the computational analysis of biological systems. Modeling approaches are central in systems biology, as they provide a rational framework to guide systematic strategies for key issues in medicine as well as the pharmaceutical and biotechnological industries. Inter- and intra-cellular processes require dynamic models, that contain the rate constants of the biochemical reactions. These kinetic parameters are often not accessible directly through experiments. Therefore methods that estimate rate constants with the maximum precision and accuracy are needed. We present here a new method for estimating rate coefficients from noisy observations of concentration levels at discrete time points. This is traditionally done by computing the least-squares estimator. However, estimation of the error function generally requires solving the reaction rate equations, which can become computationally unfeasible. We propose an alternative approach based on a probabilistic, generative model of the variations in reactant concentration. Our method returns the rate coefficients, the level of noise and an error range on the estimates of rate constants. Its probabilistic formulation is key to a principled handling of the noise inherent in biological data, and it allows for a number of further extensions. The mathematical procedure presented here has been implemented in a software tool, named KInfer.
Download Technical Report

This short note intends to clarify about the applicability of the Stochastic Simulation Algorithm proposed by Gillespie for the analysis of systems of coupled biochemical reactions. The derivation of Gille- spie’s results is revisited to pinpoint those steps at which, depending on the validity of the assumptions adopted about the system to be studied, approximations may be introduced. We discuss about the ways the inaccuracies entailed by the approximations may propagate and affect simulation results.
Download Technical Report

BlenX is a programming language explicitly designed for modeling biological processes inspired by Beta-binders. The actual framework assumes biochemical interactions being exponentially distributed, i.e., an underlying Markov process is associated with BlenX programs. In this paper we relax this condition by providing formal tools for managing non-Markovian processes within BlenX.
Download Technical Report

Classical modeling approaches for biology are mainly ground-ed in mathematics, and specifically on ordinary differential equations (ODE). Process calculi-based conceptual and computational tools are an alter- native and emergent approach. Here we focus our analysis on BlenX (a beta-binders inspired programming language) showing how it is possi- ble to easily re-use ODE models within this framework. An example will show then the advantages of moving into a stochastic approach.
Download Technical Report

This paper presents a new programming language, BlenX. BlenX is inspired to the process calculus Beta-binders and it is intended for modelling any system whose basic step of computation is an interaction between sub-components. The original development was thought for biological systems. Therefore this tutorial exemplifies BlenX features on biology-related systems.
Download Technical Report

The parallel simulation of biochemical reactions is a very interesting problem: biochemical systems are inherently parallel, yet the majority of the algorithms to simulate them, including the well-known and widespread Gillespie SSA, are strictly sequential. Here we investigate, in a general way, how to characterize the simulation of biochemical systems in terms of Discrete Event Simulation. We dissect their inherent parallelism in order both to exploit the work done in this area and to speed-up their simulation. We study the peculiar characteristics of discrete biological simulations in order to select the parallelization technique which provides the greater benefits, as well as to touch its limits. We then focus on reaction-diffusion systems: we design and implement an efficient parallel algorithm for simulating such systems that include both reactions between entities and movements throughout the space.
Download Technical Report

Computational models and simulation algorithms are commonly applied tools in biological sciences. Among those, discrete stochastic models and stochastic simulation proved to be able to effectively capture the effects of intrinsic noise at molecular level, improving over deterministic approaches when system dynamics is driven by a limited amount of molecules. A challenging task that is offered to researchers is then the analysis and ultimately the inference of knowledge from a set of multiple, noisy, simulated trajectories. We propose in this paper a method, based on Independent Component Analysis (ICA), to automatically analyze multiple output traces of stochastic simulation runs. ICA is a statistical technique for revealing hidden factors that underlie sets of signals. Its applications span from digital image processing, to audio signal reconstruction and economic indicators analysis. Here we propose the application of ICA to identify and describe the noise in time-dependent evolution of biochemical species and to extract aggregate knowledge on simulated biological systems. We present the results obtained with the application of the proposed methodology on the well-known MAPK cascade system, which demonstrate the ability of the proposed methodology to decompose and identify the noisy components of the evolution. Quantitative descriptions of the noise component can be further analytically characterized by a simple first order autoregressive model.
Download Technical Report

Compartments and membranes are the basis of cell topology and more than 30% of the human genome codes for membrane proteins. It is possible to represent compartments and membrane proteins in a nominal way with many mathematical formalisms used in systems biology, however few explicitly model the topology of the membranes themselves. Discrete stochastic simulation of molecular kinetics potentially oers the most accurate representation of cell dynamics. Since the details of every molecular interaction in a pathway are often not known, the relationship between chemical species in not necessarily best described by simple mass action chemistry. Moreover, modelling every individual molecular interac- tion in the cell is probably unnecessary and currently impractical. Simulation is a form of computer aided analysis, relying on human inter- pretation to derive meaning. To improve eciency and gain meaning in an automatic way, it is necessary to have a formalism based on a model which has decidable properties.
Download Technical Report

Automated verification of stochastic models has been proved to be an effective technique for the analysis of a large class of stochastically behaving systems. In this paper we show how stochastic modelchecking can be effectively applied to the analysis of biological systems. We consider a few models of biological systems taken from the literature, and we consider both their encodings as ordinary differential equations and Markovian models. We show that stochastic model-checking verification of biological systems can complement both deterministic and stochastic simulation techniques when dealing with dynamical properties of oscillators. We demonstrate how stochastic model-checking can provide exact quantitative characterization of properties of systems exhibiting oscillatory behavior, providing insights that cannot be obtained with differential equations models and that would require a large number of runs with stochastic simulation approaches. 1
Download Technical Report

The genetic regulation of the Trp operon in the bacterium E. coli relies on a sophisticated control mechanism. It tightly couples the advance of transcribing RNA polymerase to the efficiency of the contemporaneous translation of the nascent transcript by a ribosome. The concurrent control of this process involves interdependencies between multiple molecular actors. Within process algebra based modeling languages focused on pairwise interaction, its representation required sophisticated coding tricks. In this work, we abstract the mechanism of transcriptional attenuation within a novel rule base modeling language. It allows non-trivial concurrent control by representing molecules as parametrized terms.
Download Technical Report

We present some decidability and undecidability results for subsets of the BlenX Language, a process-calculi-based programming language developed for modelling biological processes. We show that for a core subset of the language (which considers only communications primitives) termination is decidable. Moreover, we prove that by adding either global priorities or events to this core language, we obtain Turing equivalent languages. The proof is through encodings of Random Access Machines (RAMs), a well known Turing equivalent formalism, into our subsets of BlenX. All the encodings are shown to be correct.
Download Technical Report

The SOS response is an inducible DNA repair system that allows bacteria to survive in presence of an increased level of DNA damage. More than 40 genes are induced in response to DNA damage as part of the SOS regulon in Escherichia coli. Two main proteins play a key role in the regulation of this response: a repressor LexA that prevents the expression of these genes and an inducer RecA that induces the LexA cleavage reaction and the subsequent expression of the response genes. Most of these response genes are responsible for error-free DNA-damage repair and for the regulation of cell division. In this thesis we have investigated a network of nine genes including the principal mediators of the SOS response: lexA, recA, ssB, recF, dinI and umuDC and three sigma factor genes: rpoD, rpoH and rpoS.
Download Technical Report

In the area of membrane computing, time-freeness has been defined as the ability for a timed membrane system to produce always the same result, independently of the execution times associated to the rules. In this paper, we use a similar idea in the framework of spiking neural P systems, a model inspired by the structure and the functioning of neural cells. In particular, we introduce stochastic spiking neural P systems where the time of firing for an enabled spiking rule is probabilistically chosen and we investigate when, and how, these probabilities can influence the ability of the systems to simulate, in a reliable way, universal machines, such as register machines.
Download Technical Report

Master Thesis
Second Level International Master in Computational and Systems Biology

Advisor: Adaoha Ihekwaba
Co-advisor: Corrado Priami
Student: Roberto Larcher
Download Technical Report

Master Thesis
Second Level International Master in Computational and Systems Biology

Advisor: Alessandro Quattrone
Co-advisor: Angela Re
Student: Ilenia Fronza
Download Technical Report

We study a modeling framework and computational paradigm called Colonies of Syn- chronizing Agents (CSAs), which abstracts intracellular and intercellular mechanisms of biological tissues. The model is based on a multiset of agents (cells) in a com- mon environment. Each agent has a local contents, stored in the form of a multiset of atomic objects, updated by multiset rewriting rules which may act on individual agents (intracellular action) or synchronize the contents of pairs of agents (intercellu-lar action). In this paper we investigate dynamic properties of CSAs, by means of temporal logic, and we give a logical characterization of some notions inspired by evolutionary biology such as robustness, mutants and species. We reveal the relation that exists between the concept of robustness for CSAs and the bisimulation relation on colonies. We also present some decidability results for particular cases of robustness.
Download Technical Report

This report presents the definition, solution and validation of a stochastic model of the budding yeast cell cycle, based on Stochastic Petri Nets. A well-established deterministic model, based on ODEs, is considered as the basis for the stochastic modeling. A specific class of Stochastic Petri Nets is selected for building a stochastic version of the deterministic model, with applying the same abstractions of biological phenomena as the ones adopted in the deterministic model. We describe in the report the procedure followed in defining the SPN model from the deterministic one, a procedure that can be largely automated. The validation of the SPN model is conducted with respect to both the results provided by the deterministic one and the results available from wet-lab experiments. A very good match is obtained for the budding yeast wild type and for a variety of mutants that have been experimentally constructed in wet-labs. The results of the two models were compared against experimental data. We show that the stochasticity allows predicting characteristics that cannot be determined with the deterministic model. Moreover, we also show that the stochastic model can fine-tune the results of the deterministic model, enriching the breadth and the quality of the model.
Download Technical Report

The stochastic kinetics of a well-stirred mixture of molecular species interacting through different biochemical reactions can modelled by the chemical master equation. Till now the scientific computing community has focussed mostly on the development of numerical techniques to approximate the solution of the chemical master equation many realizations of the associated Markov jump process. Consequeltly, the domain of exact algorithms for directly solving a chemiacl master equation is still an open research area. In this work we present a method to solve analytically a chemical master equation to describe a reversible molecular reaction and we propose a method to solve a system of such equations. In this method molecular populations are considered as time-dependent, integer-valued random variables. Moreover, we developed mathematical procedures for solving a system of chemical master equations referred to a set of parallel and interdependent biochemical interactions. The causal dependence between reactions is modeled on the time scale in the following way: a reaction starts when its antecessor has produced a sufficient quantity of reactants.
Download Technical Report

We present a novel method for estimating rate coefficients from noisy observations of concentration levels at discrete time points. This is traditionally done by computing the least-squares estimator. However, estimation of the error function generally requires solving the reaction rate equations, which can become computationally unfeasible. Here we present an alternative approach based on a probabilistic, generative model of the variations in reactant concentration. Our method returns the rate coefficients, the level of noise and an error range on the estimates of rate constants. Its probabilistic formulation is key to a principled handling of the noise inherent in biological data, and it allows a number of further extensions.
Download Technical Report

This paper proposes a simplification of the stochastic Petri nets graphical notation with the purpose of defining a more compact and clearer graphical way of building formal models of biological phenomena. Three biological examples are first presented, then modeled with the classical SPN modeling formalism, and their key modeling patterns distilled to identify the main features that need to be represented in a stochastic model. The key features are then the object of the original part of the paper, in which a simplified and more concise, although formal, graphical notation, is proposed, and applied to the selected examples. The paper demonstrates the effectiveness of the simplified notation in producing more compact and understandable models of biological phenomena, still retaining the nice properties of Stochastic Petri Nets, i.e., their flexible abstraction level and formal semantics.
Download Technical Report

The interaction between lymphocyte in the circulation and endothelial cells lining the blood vessels is a crucial control point in the mechanism of chemotactic detection of inflammation sites. This interaction is mediated by a multisptep process, termed lymphocyte recruit ment, involving lymphocyte rolling along the endothelium, activation of lymphocyte integrins, adhesion to endothelial ligands and lymphocyte crossing the endothelium. The events of the lymphocyte extravasation, called diapedesis is crucial in the pathogenesis of autoimmune neurological diseases, like multiple sclerosis. Recent wet-labs studies provided the data and the observations proving that chemokines modulate the control of the lymphocyte-endothelial cell recognition and regulate the arrest of lymphocyte. In this paper we present a model of lymphocyte recruitment expressed in the formalism of beta-binders and we explore its sensitivity in response to changes of the rates of interaction between chemokines and their receptors. The study is motivated by the intention to individuate those ligand/receptor interactions and their kinetic parameters that are significantly influential in determining the firm arrest of the lymphocyte. We focuses the analysis on the rate coefficients of the chemokines interations. By tuning these parameters we estimate the sensitivity of the model to the rapidity of the lymphocyte adhesion, that recent in vivo observations suggest to be an important factor determining the final result of the rolling process.
Download Technical Report

Beta-binders is a comparatively new modeling formalism introduced for systems biology. To execute Beta-binders models, suitable simulators are required which translate the operational semantics of Beta-binders into a sound and efficent execution. Efficiency can be reached by parallel and distributed simulation and by a proper representation of models to ensure a fast manipulation. Both possibilities are considered in the implementation of the described hierarchical Beta-binders simulator. The description includes a tree structure which reflects p-calculus and Beta-binders processes and the algorithm of the simulator which enables a distributed and optimistic, parallel execution.
Download Technical Report

This paper introduces Protein Calculus, a special modeling language designed for encoding and calculating the behaviors of compartmentilized biological systems. The formalism combines, in a unified framework, two successful computational paradigms - process algebras and membrane systems. The goal of Protein Calculus is to provide a formal tool for transforming collected information from in vivo experiments into coded definition of the different types of proteins, complexes of proteins, and membrane-organized systems of such entities. Using this encoded information as input, our calculus computes, in silico, the possible behaviors of a living system.
Download Technical Report

Chemotaxis is the ability of bacteria to locate high attractant sources in the environment. The extensive knowledge gained from the pathway in the model organism Escherichia coli shows that adaptation to stimuli is a hallmark underlying chemotaxis. Studies on certain mutant strains and other bacterial species, however, indicate that some form of chemotaxis could also be achieved without adaptation. It is not clear how efficient such chemotaxis is, how it could be mediated, and how widespread it is among different bacterial species. In order to explore alternative pathway structures and dynamics that can underlie chemotaxis, we employ an evolutionary approach. This approach starts with a population of bacteria that move in a virtual environment based on the dynamics of simple pathways they harbour. As mutations lead to changes in pathway structure and dynamics, bacteria with better ability to localize with high attractant sources gain a selective advantage. We find that chemotaxis via non-adaptive dynamics evolves consistently under different model assumptions and environments. These dynamics directly couple tumbling probability of the cell to increasing attractant levels. Further analyses of evolved pathway structures show that this alternative behaviour can be mediated with as few as two components. The non-adaptive mechanisms mediating chemotaxis provide an explanation for experimental observations made in mutant strains of E. coli and in wild type Rhodobacter sphaeroides and that could not be explained with existing knowledge. These mechanisms could allow a straightforward link between cell metabolism and chemotaxis. Furthermore, they could have acted as the origin of the conventional chemotaxis involving adaptation.
Download Technical Report

The paradigmatic shift occurred in biology that led ¯rst to high-throughput experimental techniques and later to computational sys- tems biology must be applied also to the analysis paradigm of the relation between local models and data to obtain an e®ective prediction frame- work. In this work we show that the new relation between systems biol- ogy models and high-throughput data permits new integrations on the systemic scale like the use of in silico predictions to support the mining of gene expression datasets. We introduce a unifying notational frame- work in which we propose two applications concerning the use of system level models to support the di®erential analysis of microarray expression data. The approach is tested with a speci¯c microarray experiment on the phosphate system in Saccharomyces cerevisiae and a computational model of the PHO pathway that supports the systems biology concepts.
Download Technical Report

We present a formal approach to the study of evolution of biological pathways. The basic idea is to use the Beta Workbench to model and simulate pathway in connection with evolutionary algorithms to implement mutations. A fitness function is used to select individuals at any generation. The feasibility of the approach is demonstrated on the MAPK pathway.
Download Technical Report

The aim of this work is twofold. First, we propose an high level textual modelling language, which is meant to be biologically intuitive and hence easily usable by life scientists in modelling intra-cellular systems. Secondly, we provide an automatic translation of the proposed language into Beta-binders, a bio-inspired process calculus, which allows life scientists to formally analyse and simulate their models. We use the Gp130 signalling pathway as a case study.
Download Technical Report

We propose a modelling framework and computational paradigm called Colonies of Synchronizing Agents (CSAs) inspired by the intracellular and intercellular mechanisms present in biological tissue. The proposed model is based on a multiset of agents present in a common environment. Each agent has a local state, stored in the form of a multiset of atomic objects, which is updated by global multiset rewriting rules either asynchronously or in synchrony with another agent. We first define the model, then study its computational power, considering trade-offs between internal rewriting (i.e., intracellular mechanism) and synchronization among the agents (i.e., intercellular mechanisms). We also investigate dynamic properties of CSAs, including behavioral robustness (ability to generate a core behavior despite agents or rule failure) and safety of synchronization (ability for an agent to synchronize with another agent, whenever needed).
Download Technical Report

The paper presents a new approach based on process calculi to systems modeling suitable for biological systems. The main characteristic of process calculi is a linguistic description level to dene incrementally and compositionally executable models. The formalism is suitable to be exploited on the same systems at dierent levels of abstractions connected through well dened formal rules. The abstraction principle that represents biological entities as interacting computational units is the basis of the computational thinking that can help biology to unravel the functions of the cell machinery. We discuss then the perspectives that process calculi can open to life sciences and the impact that this can in turn produce on computer science.
Download Technical Report

We consider here spiking neural P systems with a non-synchronized (i.e., asynchronous) use of rules: in any step, a neuron can apply or not apply its rules which are enabled by the number of spikes it contains (further spikes can come, thus changing the rules enabled in the next step). Because the time between two firings of the output neuron is now irrelevant, the result of a computation is the number of spikes sent out by the system, not the distance between certain spikes leaving the system. The additional non-determinism introduced in the functioning of the system by the non-synchronization is proved not to decrease the computing power in the case of using extended rules (several spikes can be produced by a rule). That is, we obtain again the equivalence with Turing machines (interpreted as generators of sets of (vectors of) numbers). However, this problem remains open for the case of restricted spiking neural P systems, whose rules can only produce one spike. On the other hand we prove that asynchronous systems, with extended rules, and where each neuron is either bounded or unbounded, are not computationally complete. For these systems, the configuration reachability, membership (in terms of generated vectors), emptiness, infiniteness, and disjointness problems are shown to be decidable. However, containment and equivalence are undecidable.
Download Technical Report

Multisite phosphorylation is known to be an important and dynamic mechanism for regulating the activity of transcription factors. Here we propose a stochastic pi-calculus modelling approach able to handle the complexity of post-translational modifications and to overcome the limitations of the ordinary differential equations based methods. The model can be applied without a priori assumptions to every (multisite) phosphorylation regulation for which some basic rates are known or can be indirectly set with experimental data. We apply it to the multisite phosphorylation of the Pho4 transcription factor that plays a crucial role in the phosphate starvation signalling in Saccharomyces cerevisiae using available in vitro experiments for the model tuning and validation. The innovative modelling of the sub-path with the stochastic pi-calculus allows quantitative analyses of the kinetic characteristics of the Pho4 phosphorylation, the different phosphorylation dynamics for each site (possibly combined) and the variation of the kinase activity as the reaction goes to completion. One of the performed predictions indicates that the Pho80-Pho85 kinase activity on the Pho4 substrate is nearly distributive and not semi-processive as previously found analysing only the phosphoform concentrations in vitro. This result is obtained because the model can consider and quantify the binding events without phosphorylations that cannot be experimentally measured. Thanks to the compositionality property of process algebras, we also developed the whole PHO pathway model that gives new suggestions and confirmations about its general behaviour. The potentialities of process calculi based in silico simulations for biological systems are highlighted and discussed.
Download Technical Report

The signals detected during physiological activation of the brain with F-deoxyglucose DG PET reflect predominantly uptake of this tracer into astrocytes. This notion provides a cellular and molecular basis for the FDG PET technique. Although in recent years the functional brain imaging has experienced enormous advances, the cellular and, in particular, the molecular mechanisms generating the signals detected by these techniques are not completely known. In this paper, we present a computational model that attempts to disentangle the intricate nature of the molecular interactions governing the brain energy metabolism. The model describes the glutamate-stimulated glucose uptake and use into astrocytes. It consists of a set of ordinary dif- ferential equations, each of which specifying the time-behavior of the main molecular species involved in the astrocytic glucose use (i. e. glutamate, glucose, Na+, beta-threohydroxyaspartate) and the dynam- ical rates of glutamate, glucose and Na+ uptake. The kinetic rates constants of the model have been identified on a set of dynamic PET images. As far as we know, a mathematical and computational model of the brain energy metabolism at the molecular level has been never proposed. The relevance of such a model to the PET functional brain imaging consists in providing an in silico framework, in which to experiment the molecular glucose dynamics and elucidate their still elusive aspects.
Download Technical Report

A growing body of evidence suggests that the accumulation of misfolded proteins in brain tissues is a crucial event in the Parkinson's disease neurodegeneration. Pathogenic mutations may directly induce abnormal protein conformations or compromise the ability of the cellular machinery to detect and degrade misfolded proteins. Although the recent explosion in the rate of discovery of genetic defects linked to Parkinson's disease (PD) have provided tangible clues to the neurobiology of the disorder, they have provided neither direct explanation for the disease process or its key biochemical mechanism. The aim of the work is to provide quantitative models for in silico experiments, that can help the researchers either to elucidate important and still elusive aspects of the Parkinson's disease or to design new wet-experiments. Here we present three stochastic models of a faulty mechanism of protein re-folding and degradation of misfolded proteins. Our models are specified in biochemical stochastic pi-calculus and are based on what is currently known about the genetic mutations causing PD. The expressive capabilities of this formalism in the description of parallel and competive nature of biochemical interactions make it particularly suitable for modeling the intricate mechanism of proteins folding, re-folding and eventually degradation. Furthermore, the simulation results point out those kinetic quantitative parameters, whose variations lead to significant changes in the capability of the system to react to the accumulation of dangerous proteins.
Download Technical Report

This paper proposes the Effective Index, a formal tool to support decision processes in drug discovery. The Effective Index is based on concurrency theory and process calculi to describe incrementally complex biological systems and on Markov process theory to handle quantitative information. A running case study concerning the pathways and the drugs related to hypertension exploits the approach.
Download Technical Report

The present models and simulation algorithms of intracellular kinetics are usually based on the premise that diffusion is so fast that the concentrations of all the involved species are homogeneous in space. However, recents experimental measurements of intracellular diffusion constants indicate that the assumption of a homogeneous well-stirred cytosol is not necessarily valid even for small prokaryotic cells. In this work we first present a mathematical description of the diffusion induced by concentration gradient. In our model the diffusion coefficients and mechanical quantities as frictional forces are dependent on the local values of solutes concentration. We then present an algorithm implementing our model and simulating a reaction-diffusion system. The algorithm is an efficient modification of the well known Gillespie alg
Download Technical Report

This paper presents a system to model and simulate biological processes. It is based on process calculi theory and incorporates a language, a compiler, the execution environment and some graphical interface components. The language is based on Beta-binders, a recently introduced process algebra bio-inspired and developed to be suitable for the biological applicative domain. The runtime environment is based on a stochastic abstract machine that extends and improve the classical Gillespie’s approach. The quantitative aspects included in the stochastic information associated with the language allow to simulate and plot quantitative parameters of the system under investigation. We define the syntax, semantics and implementation of the language comparing our design choices with the most common features of process calculi applied to biology. A relevant part of this work is the description of design patterns for the most common biological features in molecular interactions. This is an important aspect in exploiting the expressive power of the language and in providing a preliminary guide to the use of the compositional properties of process calculi.
Download Technical Report

We propose a new logic designed for modelling and reasoning about information flow and information exchange between spatially located (but potentially mobile), interconnected agents witnessing a distributed computation. This is a major problem in the field of distributed systems, covering many different issues, with potential applications from Computer Science and Economy to Chemistry and Systems Biology. Underpinning on the dual algebraical-coalgebraical characteristics of process calculi, we design a decidable and completely axiomatizad logic that combines the processalgebraical/ equational and the modal/coequational features and is developed for process-algebraical semantics. The construction is done by mixing operators from dynamic and epistemic logics with operators from spatial logics for distributed and mobile systems.
Download Technical Report

While detection and analysis of functional modules in biological systems have received great attention in recent years, we still lack a complete understanding of how such modules emerge. One theory is that systems must encounter a varying selection (i.e. environment) in order for modularity to emerge. Here, we provide an alternative and simpler explanation using a realistic model of biological signaling pathways and simulating their evolution. These evolutionary simulations start with a homogenous population of a minimal pathway containing two effectors coupled to two signals via a single receptor. This population is allowed to evolve under a constant selection pressure for mediating two separate responses. Results of these evolutionary simulations show that under such a selective pressure, mutational processes easily lead to the emergence of pathways with two separate sub-pathways (i.e. modules) each mediating a distinct response only to one of the signals. Such functional modules are maintained as long as mutations leading to creation of new interactions among existing proteins in the pathway are rare. While supporting a neutralistic view for the emergence of modularity in biological systems, these findings highlight the relevant rate of different mutational processes and the distribution of functional pathways in the topology space as key factors for its maintenance.
Download Technical Report

Several approaches have been proposed to model biological systems by means of the formal techniques and tools available in computer science. To mention just a few of them, some representations are inspired by Petri Nets theory, and some other by stochastic processes. A most recent approach consists in interpreting the living entities as terms of process calculi where the behavior of the represented systems can be inferred by applying syntax-driven rules. A comprehensive picture of the state of the art of the process calculi approach to biological modeling is still missing. This paper goes in the direction of providing such a picture by presenting a comparative survey of the process calculi that have been used and proposed to describe the behavior of living entities.
Download Technical Report

Transport of substances and communication between compartments are fundamental biological processes, often mediated by the presence of complementary proteins attached to the surfaces of membranes. Within compartments, substances are acted upon by local biochemical rules. Inspired by this behaviour we present a model based on Membrane Systems, with objects attached to the sides of the membranes and floating objects that can be moved between the regions of the system. Moreover, in each region there are evolution rules that rewrite the transported objects, mimicking chemical reactions. We investigate qualitative properties, like configuration reachability, in relation to the use of cooperative or non-cooperative evolution and transport rules and in the contexts of free- and maximal-parallel evolution.
Download Technical Report

Motivated by several techniques for observing molecular processes in real-time we introduce a computing device that stresses the role of the observer in biological computations and that is based on the observed behavior of a splicing system. The basic idea is to introduce a marked DNA strand into a test tube with other DNA strands and restriction enzymes. Under the action of these enzymes the DNA starts to splice. An external observer monitors and registers the evolution of the marked DNA strand. The input marked DNA strand is then “accepted” if its observed evolution follows a certain expected pattern. We prove that using simple observers (finite automata), applied on finite splicing systems (finite set of rules, i.e., enzymes and finite set of axioms, i.e., initial strands), the class of recursively enumerable languages can be recognized.
Download Technical Report

In this work we propose an extension of Beta-binders with biological transactions, called TBeta-binders, in order to model a sequence of elementary actions atomically. This extension is useful when we need to specify multi-reactant multi-product reactions or when we use a sequence of actions to represent a single biological interaction. Some properties of these transactions are reported. Finally, some simple but explicative examples are described to validate our extension.
Download Technical Report

We investigate static hierarchies of biological systems through Beta-binders, a recently developed process calculus. We rely on a general interpretation of beta-processes as structured communicating objects. We extend the calculus with the notion of compartment. Objects can either be internal to compartments or reside on compartment borders. Movement in and out of compartments is requested by internal objects and mediated by border objects. We equip the extended calculus with the notion of locality and we define various kinds of relations between actions. Furthermore, we compare our proposal with similar formalisms and we show its application on a biological example.
Download Technical Report

Chemical and biochemical systems are presented as collectives of interacting stochastic automata: each automaton represents a molecule that undergoes state transitions. This framework constitutes an artificial biochemistry, where automata interact by the equivalent of the law of mass action. We analyze several example systems and networks, both by stochastic simulation and by ordinary differential equations.
Download Technical Report

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 Membrane Systems with Peripheral and Integral Proteins. 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 saccharomyces cerevisiae and present a quantitative analysis using an implemented simulator.
Download Technical Report

Beta-binders is a recent process algebra developed for modeling and simulating biological systems. As usual for process calculi, the semantic definition heavily relies on a structural congruence. The treatment of the structural congruence is essential for implementation. The proof of the decidability of this congruence, reported in this paper, is a first step towards implementations.
Download Technical Report

Abstracts of the talks of the Scientific Opening of the Microsoft Research - University of Trento Centre for Computational and Systems Biology held in Trento on April 3-5, 2006
Download Technical Report

Transport of substances and communication between compartments are fundamental biological processes, often mediated by the presence of opportune and complementary proteins attached to the surfaces of membranes. Within compartments, substances are acted upon by local biochemical rules. Inspired by this behaviour we present a model based on membrane systems, with objects attached to the sides of the membranes and floating objects that can move between the regions of the system. Moreover, in each region there are evolution rules that rewrite the transported objects, mimicking chemical reactions. We first analyse the system, showing that interesting qualitative properties can be decided (like reachability of configurations) and then present a simulator based on a stochastic version of the introduced model and show how it can be used to simulate relevant quantitative biological processes.
Download Technical Report

We propose a new logic for expressing properties of concurrent and distributed systems, Dynamic Epistemic Spatial Logic, as an extension of Hennessy-Milner logic with spatial and epistemic operators. Aiming to provide a completely axiomatized and decidable logic for concurrency, we devise epistemic operators, indexed by processes, to replace the guarantee operator in the classical spatial logics. The knowledge of a process, considered as epistemic agent, is understood as the information, locally available to our process, about the overall-global system/process in which it is an agent/subprocess. Dynamic Epistemic Spatial Logic supports a semantics based on a fragment of CCS against which the classical spatial logics have been proved to be undecidable. Underpinning on a new congruence relation on processes - the structural bisimulation - we prove the finite model property for our logic, thus concluding on its decidability against the same semantics. A sound complete Hilbert-style axiomatic system is developed, comprehending the behavior of spatial operators in relation with dynamic/temporal and epistemic ones. Eventually we emphasize on the similarities with the classical axioms and rules of knowledge, that present our logic as an authentic dynamic-epistemic logic.
Download Technical Report

In this work we extend the pi-calculus with a simple class of transactions, suitable to model multi-reactant, multi-product chemical reactions. Some examples are reported to validate our extension.
Download Technical Report

Causal relations allow us to understand the causes of single transitions/ events in a computation and, consequently, to acquire information on the whole systems. In this paper a definition of a causal relation and of an enabling relation for Beta-binders is given, together with the description of some important properties of these relations; in particular we show that the concurrency relation is the complement of the union of causal and enabling relations for each possible computation. The application domains which we are mostly interested in are biology and medical sciences, thus the application of the defined relations to a model of the intensively studied ERK/MAPK pathway is described.
Download Technical Report