RICERCA ITALIANA     

Systems Biology: modeling, languages and analysis (Sybilla)

Università degli Studi di Trento

Abstract

We plan to determine techniques to model (both at a linguuistic and at a graphic level) complex biological systems. We then equip our formalisms with tools to analyse the dynamic behaviour and the dynamic evolution of the system in hand recovering most of the results coming from concurrency and language theory. We also exploit in this project results from the simulation world by including quantitative information in the specifications of the case studies. Eventually, we also investigate how logical formalisms can be used and adapted to the new biological applicative domain.

The above development is tuned, tested and validated over case studies coming from the literature and from the interactions that any group involved in this project has with biologists under other funded initiatives.

The feasibility of the approach is shown by realizating proof-of-concept software tools based on the theoretical framework developed in the first phase of the investigation.

The main focus of the activities reported here is on the computer science side as they should produce new language primitives and analysis tools that are then instantiated to a biological setting. The positive side effect of this research is that new computational paradigms could emerge taking inspiration from the way in which living matter process information. <<<

Principal Investigator

Corrado PRIAMI Università degli Studi di TRENTO

Research Objectives

The ultimate goal of systems biology is to predict the behavior of living matter. If we can devise framework that can model biological systems and analyse and simulate them, then are on the right track. Ultimately, we want to understand the functioning of cells at useful levels of abstraction, and we want to be able to predict unknown behavior. Those achievement should then enable us to use biological matter as flexible information and material processing devices. <<<

First Results

The results attended out of this phase are:

- definition of new primitives for modeling biological systems through process calculi and their stochastic extension to cope with quantitative parameters;

- new models based on hybrid automata and temporal logics taking inspiration from biological phenomena;

- Extension of membrane systems with probabilities to define interaction within biological systems;The expected results are:

- generalization of hybrid automata and definition of efficient algorithms to analyse properties of biological systems;

- definition of basic simulation tools for hybrid models, process calculi and membrane systems;

- new techniques to handle the protein folding problem;

- re-use of existing tools to model check logical specifications of biological systems;

- cross-influence between computer security and biological models of, e.g., the immune system;The expected results are:

- modeling and analysis of biological case studies to tune and validate the ideas and tools proposed; <<<

Timescale

24 months

National and international background

One of the main problems of contemporary biology is understanding the dynamics of genes and proteins inside the cellular molecular machinery, when they give rise to a living organism [Kitano02]. Unfortunately, nowadays there are no experimental techniques able to track the dynamics of the complete metabolome of a cell. A promising approach is to represent all the known relationships between the elements in a metabolome in silico, so building up a sort of a virtual cell [LS01]. There are many proposals of biochemical modelling [GP98,DL03,NOMK99] (see also www.cellml.org). Here, we concentrate our attention to those based on formal methods.

We shall briefly survey those approaches that exploit the similarities between networks of biochemical cells and networks of computing processes. Indeed, a network of bio-cells can be seen as a computing machinery, made of processing agents which interact and cooperate to achieve a common goal. Agents autonomously compute on their own and exchange information with each other [RS02]. This informal description applies to concurrent system as well, in the so-called global computing field. These systems are made of large number of geographically dispersed, possibly mobile and communicating computing agents. It is thus natural to use techniques from the global computing field to study the behaviour of biological cells. Particularly promising is the use of process calculi, which are formalisms used to describe mobile, concurrent systems. Process calculi are mathematically sound, and come equipped with tools for the static and dynamic analysis of global applications. These tools can be therefore used in the field of biological organisms, as well. The pioneering work on modelling biochemical systems with a calculus is the work by Fontana and Buss [FB96] where a version of the lambda-calculus is used. A better account of pathways descriptions is proposed by Regev, Silverman and Shapiro [RSS01], who use the pi-calculus [MPW92], a well-known formalism for mobility.
Then, Priami, Regev, Silverman and Shapiro enrich in [PRSS01] the pi-calculus with quantitative aspects, exploiting a stochastic variant, originally proposed by Priami in [Priami95], to evaluate the performance of concurrent and mobile processes. Curti, Degano, Priami and Baldari use an enhanced semantics of the pi-calculus in [CDPB04] to represent aspects of process behaviour related to causality and locality, thereby improving the expressivity of specifications and allowing for graphical
representations of computations. This enhanced pi-calculus is also used in [CCDM] to specify and analyse a hypothetical cell with a genome as basic as possible. This virtual prokaryote exhibits in silico a behaviour similar to that of living ones, so the authors validate their specification. Among the calculi used in system biology, we mention also the Bio-calculus proposed by Nagasaki, Onami, Miyano and Kitano in [NOMK99], a framework that include an equation editor, an interpreter and a graphical interface; its users describe pathways by using conventional biochemical equations. Recently, Regev proposed Bio-ambients [Reg03], a variant of Cardelli and Gordon's Ambient Calculi [CG98], in which
compartments are described as a hierarchy of boundary ambients. This hierarchy can be modified by suitable operations that have an immediate biological interpretation. For example, the interactions between compounds that reside in the cytosol and in the
nucleus are represented through parent-child communications, exploiting a notion of compartment. Danos and Laneve [DL03,DL03a] and Chiaverini and Danos [CD03] recently proposed the Core Formal Molecular Biology, building up on the basic primitives of the pi-calculus. As in the other language-based models mentioned above, processes represent compounds, set of processes represent solutions, and their behaviour is given by a set of rewriting rules which account for, e.g. activation, synthesis, complexation. Petri Nets are another graphical formalism used to model concurrent systems. Essentially, they are automata whose states are sets of distributed components, and transitions may transform only some elements of a state. Variants of Petri Nets has been widely used in System Biology [GP98,HT98,KL91], also because of their intuitive graphical representation; as expected, places represent molecules, while transitions represent reactions. In [RLM96], Place/Transition Petri Nets are used for a qualitative analysis of biochemical processes. Recently [HKW03] uses the semantics of the formalism to decide coherency of models. Self-modified Petri Nets are used to represent a quantitative model of biochemical networks [HT98] and Hybrid Petri Nets [MDNM00] model regulatory networks by taking in account concentrations of proteins and RNA.
Stochastic Activity Networks extend Petri Nets, and are used in [ML97] for representing biological pathways and simulating their kinetics. MetaNets [KL91] are a graph theoretical model of metabolic gene-expression networks. We also mention some recent approaches based on statecharts that build a qualitative model of cellular systems with molecular
components [HB98,KCH02]. Among the various tools for the dynamic analysis of processes are the concurrency (e.g. www.dcs.ad.ac.uk/home/cwb) e mobility workbenches
(e.g. www.it.uu.se/research/group/mobility/mwb). These workbenches are semantics-based tools which cater for the manipulation and dynamic analysis of mobile concurrent systems. They perform various analyses of behaviours of processes, specified using a process calculus, such
analysing the state space or checking various semantic equivalences and preorders.
Similar tools for the analysis of systems described by a stochastic model are available as well. One example is the PEPA workbench (www.dcs.ed.ac.uk/pepa/), where the model is expressed in the stochastic process algebras PEPA. Another one is BIO-SPI [PRSS01]. Another example is given by TwoTowers (www.uniurb.it/bernardo/twotowers/), a software tool for the functional verification and performance evaluation of computer, communications and software systems formally modelled with stochastic process algebra. In the last years, encouraging results have been obtained by the use of a particular static technique, called Control Flow Analysis, for validating security and safety issues for concurrent and mobile systems. A Control Flow Analysis for these calculi [BDNN01ic] should focus on the use of channels and of values. In fact, it predicts safe and computable approximations to the set of values that the objects of a program may assume during its execution. As other static techniques, Control Flow Analysis provides a repertoire of automatic and decidable methods and tools for analysing properties of systems. These tools can be hopefully exploited to analyse processes also when they model biological systems.


Membrane systems are a new computability model related to the area of molecular computing, recently introduced by G. Paun. The model is inspired from the observation that all the cellular-level processes, where different chemical reactions and flow of different materials among different compartments take place, can be viewed as computing processes. Any non-trivial biological system is a construct in which various components execute different "computations", and the results of these computations can be communicated among the components. Each component is well delimited by various types of membranes, that keep them separated and act as semi-permeable barriers, ensuring that certain substances always stay into the compartment while other substances stay out of it. To define a mathematical counterpart of the cell, we need to define a structure which models the hierarchical architecture of the cell. Such a structure is the membrane structure, a set of membranes hierarchically embedded in a given main membrane, called the skin membrane. Once defined the membrane structure, we can add objects (DNA strands, molecules, etc.) and evolution rules (chemical reactions) associated with each region. The evolution rules operate on objects, by modifying them, and on the membrane structure, by dissolving, create or divide membranes. The molecules present in the cell can move from a region to another one by passing through the membranes.
A computation device is obtained: it is called a Membrane System or a P system. We start from an initial configuration, with a certain number of objects in certain membranes, and we let the system evolve. If a computation halts, that is no further evolution rule
can be applied, then the result of the computation is defined on the basis of the objects we obtain in a specified membrane (or expelled through the skin membrane). One of the most attractive feature of such systems is their intrinsic parallelism: all objects
having access to a rule should use that rule, and all membranes work in parallel [A8].
Nonetheless, this is not the only interesting aspect of these systems. As said, membrane systems are inspired from the functioning of the cell. Hence, it is very natural to consider them to model different cell processes and natural living systems, so to acquire useful
information for biologists. The first steps in this direction have already been made: energy aspects connected to cellular reaction have been considered in [A11]; simulation of photosynthesis in [A15]; communication processes within the cell in [A5]; different aspects concerning biological organisms and systems have been considered in [A1,A4,A14,A22,A25].


In the late seventies, the Artificial Intelligence community developed systems like Mycin and various pathway databases such as BioCyc (www.biocyc.org), KEGG (www.genome.ad.jp/kegg/), PathDB (www.ncgr.org/pathdb), WIT (www.mcs.anl.gov/WIT2), etc. Current systems in this area concentrate on representing the descriptive aspects of metabolic and regulatory pathways, gene networks, or protein-protein interactions. More quantitative approaches, concentrating on the modeling of biological systems, have been developed, most notable among them being the works by Voit and Savageau [44] and Tyson and Novak [40]. These efforts are primarily characterized and constrained by the attention paid to simulation of the mathematical models developed. Simulation based approaches range from Gillespie's work [16] in the seventies to the more recent System Biology Workbench (www.sbw-sbml.org) (with the companion SBML model exchange XML format (http://www.smb-sbml.org/sbml/docs/index.html)), many components of the BioSpice system (www.biospice.org), the E-CELL system [39], the Virtual Cell [36], and GEPASI (gepasi.dbs.aber.ac.uk/softw/gepasi.html). Reasoning tools based on symbolic algebra, temporal logic, and control-theoretic approaches belong to a fourth class of research. These tools have only started to be considered as viable tools for the goals we have set forth, and, to the best of our knowledge, are not yet in the common vocabulary of the systems biologists. During the mid-nineties and later, there has been a growing interest in Hybrid Systems within the Computer Science and Engineering field. This growing interest stemmed from a need to reconcile the body of knowledge about discrete systems and continuous systems. In essence, a hybrid system is a Finite State Automaton (FSA), where each state has an associated set of (algebraic) differential equations. In other words, a hybrid system is simply a description of a (biological) system where certain discrete modes of behavior are recognized. The behavior of the system within each mode is modeled by a system of differential equations, and the mode-transitions are described by true/false conditions, along with some "change" indications of the underlying
observables. "Modes" are also called states and "conditions" are also called guards. Many biological systems can be modeled by hybrid systems. For example, in the Cell Cycle the halving of the observable cell mass after cell division—-a transition between two operating modes—-is one of the discrete and discontinuous "changes" in the observable variables. The ability of hybrid systems to represent regulatory pathways, where repression or inhibition of a gene changes the behavior of a set of metabolic and regulatory pathways, is the particular characteristic that makes them attractive as a tool for modeling bio-molecular systems ([1]). In [5, 14, 42] simulators and analyzers of hybrid systems have been implemented. Moreover, languages capable of encoding both hybrid systems and other similar systems, where the underlying timing and synchronization structure is a mixture of both synchronous and asynchronous transitions [4], have been developed. These languages are expressive and intuitive to the extent that a non-mathematical user can rigorously and faithfully communicate the structure of a biological system effortlessly.
Apart from simulation, hybrid systems can be analyzed in several ways, some more computationally tractable than others. In most cases, we are interested in the verification of properties; for example, safety-—the concentration of protein P will never exceed X µMol-—a reachability property, or liveness--the concentration of mRNA R will always oscillate between a and b. To check the properties of discrete systems (safety, liveness, etc.) we employ several tools and techniques. Model checking (MC) and theorem proving (TP) tools based on Automata and/or Temporal Logic haveproven extremely useful in the context of hardware and software verification. Essentially, all these tools perform various forms of reachability analysis over the resulting state space, the size of which can be exponential in the number of components. Current systems like smv and NuSMV, SyMP, and Kronos provide a frameworkfor many possible developments. For instance, Kronos is used to test Timed Automata specifications — a feature which is of particular interest to us. This class of tools is commonly used as a sort of "debugger" for hardware, software, and communication system models. In the context of biological system modeling, they would provide a way to quickly highlight an incorrect hypothesis, or provide information useful to devise a wet-lab experiment. Tools for checking properties of hybrid systems happen to be more complex. The state-of-the-art systems deal with restricted forms of hybrid systems, the so-called linear or rectangular hybrid systems, using quotient and bisimulation techniques to check for safety and liveness properties. The HyTech system [19] is an example of such a tool from UC Berkeley. Our prior work on collapsing and bisimulation [6] simplifies the application of property checking for hybrid systems within our framework. Of course, such considerations play a very important role when dealing with the issues of compositionality of models; we will also explore these issues in our general framework (cf. [3,10,12,32]). While model checking has been successfully used to prove properties of discrete and hybrid systems, in certain applications the state space explosion problem renders model checking ineffective. In these cases, theorem prover approaches have become the tools of choice [31]. <<<