RICERCA ITALIANA     

Bio-Inspired Systems and Calculi with Applications -- BISCA

Università di Pisa

Abstract

Abstract

We plan to develop and use methods typical of computer science for describing, analysing and implementing in silico biological systems.
Besides offering such a modelization, we expect that the interaction and organization mechanisms of living matter will suggest us new paradigms of computation and new formalisms beneficial to information technology in general.
In particular, the project will focus on languages and models for specifying biological systems, for simulating their behaviour and for verifying formally their properties.

We will mainly concentrate on the specification and analysis of intra- and inter-cellular interactions.
The description of these phenomena will include both qualitative aspects, e.g. cause-effect relationships, and quantitative aspects, e.g. those depending on time and probabilistic distributions typical of biological systems.
Quantitative and qualitative aspects require new enhancements of existing computer-based analysis techniques and the development of new ones.

We plan to use linguistic mechanisms and models, specifically tailored for describing and manipulating such aspects of living matter as biochemical reactions, metabolic pathways and membranes.
Therefore we may be required to adapt existing linguistic instruments and models and to develop new ones.

Our ideas and proposals will be tuned, tested and validated over case studies coming from the relevant literature and selected together with the biologists present in all the research groups involved in this project, as well as with biologists and computer scientists working in similar topics worldwide, the results of which we envisage to compare with ours.
The feasibility of our approach will be further validated by designing and implementing proof-of-concept prototypical software tools, based on the theoretical framework developed in the first phase of the investigation.

Our long term goal is twofold.
From the one side, we aim at producing tools and techniques inspired by the biological world, and able to deal with much more complex Information Technology problems than were addressable with current technology, for example being able to do knowledge discovery in structurally and behaviourally complex systems functioning in probabilistic environments, or modelling and simulation tools for handling (partial) knowledge at different levels of detail.
On the other hand, we would like to offer biologists with an environment for attacking problems at a system level that cannot be addressed without using Information Technology, because biology is a knowledge-intensive domain, involving huge amounts of data, showing emerging properties.

If successful, this project will confirm a general understanding in the scientific community, that Information Technology will be as indispensable for biology, and viceversa, as mathematics has been for physics.
In any case, there will certainly be a fruitful cross-fertilization between biology and computer science. <<<

Principal Investigator

Pierpaolo Degano Università degli Studi di PISA

Research Objectives

Our long term goal is twofold. First, we aim at discovering new models and theories within Computer Science inspired by the biological world, and at producing techniques and tools to deal with much more complex Information Technology problems than those addressable with current technology. Second, we plan to provide biologists with an environment for attacking problems at a system level, not addressable without using Information Technology. This environment will provide biologists with modelling, analysis and simulation tools capable of handling complex behaviour and of representing emerging properties.
We advocate thus a convergence between computer and life sciences, placing ourselves in the computational side of Systems Biology. This emerging paradigm of biology moves from the classical reductionist approach to a system level understanding of life, where unpredictable, complex behaviour show up. Essential to that shift is the ongoing change of focus in biology from structure to functionality. We claim that computer science will greatly contribute to a better understanding of the behaviour of bio-systems, as computer science deals with the “process of functioning” whereas, e.g. mathematics or physics deal with the “result of these functioning”. In our terminology, passing from structure to functions amounts to equipping syntax with a behavioural semantics. We thus call for a paradigm shift also on the bio-informatics side: we plan to develop models, languages and tools for describing, analysing and implementing in silico bio-systems, as an additional contribution of information technology to those typical research areas in current bio-informatics, such as storing, organising and retrieving large amounts of biological data or searching and matching DNA sequences, just to mention two well-known topics.

More in detail, we shall develop and use formal methods for modelling and studying the behaviour of living matter. Our starting point is that bio-systems are conveniently described as entities that change their state because of the occurrence of bio-chemical interactions, giving rise to some observable behaviour. Just in the same way, computer systems are often presented as abstract machines, and their behaviour specified by the transitions that may occur, changing the abstract machine internal state. We thus adhere to the view of living matter as a biological computing unit.We shall follow three main lines of research, each tackling complementary aspects of abstract machines.

The first line is on the development of new process calculi, endowed with bio-mimetic primitives, with particular attention to inter-process interaction and stochastic and probabilistic aspects. These primitives will reflect the way living organisms act while interacting with other entities or with the environment. Our tailored calculi will share with the existing ones their formal, executable semantics, thus allowing for re-use of established theory, methods and tools. Particularly relevant are the interpreters, that run the specification of a biological organism: each run can be seen as an experiment in silico. Of course, stochastic parameters are of paramount importance to that simulation, as well as any statistical tool for further analysis of the simulated behaviour. We plan to validate our approach by simulating various biological organisms, to be selected in tight cooperation with the biologists involved in the project. Among the entities to model and analyse, there will be a simplified “virtual” prokaryote, and a partial view of protein synthesis at cellular level.

The second line of research is on mixed approaches for systems biology, among which a compositional theory of hybrid automata, an algebraic approach to model checking, and the development of a meta-tool for that. We plan to study the links between formalisms based on process calculi and hybrid automata, clarifying the relations between internal (based on communication) and external descriptions (based on observable quantities described mainly by systems of differential equations) of bio-systems. The compositional theory of hybrid automata is interesting because usually real systems are built by many components which can interact with each other. Unfortunately, these models have a number of discrete states exponential w.r.t the number of the components. This is the state explosion problem. All the proposed techniques use a top-down approach: starting from the whole system they aim at reducing the state space. We look for a bottom-up approach that verifies each component and combines the results to obtain the overall behaviour. We will investigate conditions on the automata to achieve such a goal. We shall exploit Tarski’s result and quantifier elimination to study hybrid automata, that has begun to be widely studied in the last few years. We wish investigating the biological domain algebraically for finding decidable classes of hybrid automaton and approximated model checking techniques based on system physical constraints and partial cylindrical algebraic decomposition.

The third line of research is inspired from the functioning of the cell. We are particularly interested in the processes which regulate the communication of biochemical substances through membranes. Through Membrane Systems framework we will model and simulate the activity of the various transmembrane protein channels of cells. A main motivation of this research line is to examine the capabilities of P systems for modelling the functioning of specific cellular phenomena. Our general aim is broadening the prospects of Membrane Computing and motivating further cooperations between scientists working in the areas of P systems and Microbiology. We will design appropriate software simulators. These will help us to check the effectiveness and the correctness of our models. The parameters and behaviour of complex systems are directly affect by even little changes of the many different operating conditions. To model complex behaviour, we shall then consider models where probabilities, possibly changing over time, are associated with evolution rules. The stochastic approach we are proposing results more adequate than the one based on differential equation, when low concentrated reactants are involved in many processes active at the same time.

Our ideas and proposals will be tuned, tested and validated over case studies coming from the literature and selected together with the biologists present in all the research groups involved in the project, as well as with biologists and computer scientists working in similar topics worldwide, the results of which we will compare with ours.
The feasibility of our approach will be further validated by designing and implementing proof-of-concept prototypical software tools, based on the theoretical framework developed in the first phase of the investigation.

If successful, this project will confirm a general understanding in the scientific community, that information technology will be as indispensable for biology, and viceversa, as mathematics has been for physics.
In any case, there will certainly be a fruitful cross-fertilization between biology and computer science.
Biologists can perform experiments in silico to better understand the functioning of cells at the wanted levels of abstraction, and ultimately to predict unknown behaviour of living matter.
As for computer scientists, we certainly push further our previous knowledge on formal methods to describe and analyse complex computing systems. Indeed, the bio-systems are much alike global computing systems, like those we see everyday on the web. Both kinds are made of a great number of independent, geographically dispersed, mobile computing agents, that exchange information and proceed with autonomously processing it. Results from our project will therefore find an almost immediate fall-out over the hot field of web services and applications. <<<

Timescale

24 months

National and international background

Base di Partenza – Modello A


The recent, often astonishing developments in biology have produced a huge amount of data on the structure of living matter; consider e.g. the success of the human genome project.
Less instead is known on the versatile biological functions that cells and their components display. Consequently, in the last years we have seen a shift from structure to functionality, and the growth of a new paradigm, that moves from the classical reductionist approach to a system level understanding of life. It is called systems biology [Kit02].

There is a general understanding in the scientific community that computer science will be as indispensable for biology as mathematics has been for physics. E.g., mapping the human genome would be impossible without computers, algorithms and syntax to model structures: it has been crucial representing DNA as a formal language over a four character alphabet and using search and matching algorithms over strings. Much in the same way, computer science appears to be essential for understanding the behaviour of living organisms: passing from structure to functions amounts to equipping syntax with semantics. Computational sciences use to deal with the “process of functioning” whereas mathematics deals with the “result of these functioning”. Therefore, computational sciences may be of great help to theorise the functioning of biological systems as a tangle of processes. Moreover, biological systems modelling is not only an important application area for computer science: it also is a paradigmatic environment for the design and testing of innovative ideas on computing.
Indeed, information technology is playing more and more as both enabler and enabled
by other areas, notably life science. In this domain, the general approach aims to produce tools, techniques and tools to describe and discovery knowledge in structurally and behaviourally complex biological systems.

We advocate then a convergence between computer science and life science, calling for a paradigm shift also on the computer science side, or at least for a fruitful cross-fertilization between the two disciplines. The literature supports our feeling, by recognising some tight connections between biological and computer systems, in particular reporting that programming language techniques and tools can be used to model, analyse and simulate the dynamic behaviour of biological systems. Indeed, biological systems are often described as entities that change their state because of the occurrence of (bio-chemical) interactions, giving rise to some observable behaviour. Just in the same way, computer systems are frequently presented as abstract machines, and their behaviour specified by the transitions that may occur, changing the internal state of the abstract machine. Another similarity is that both kinds of systems result from the combination of smaller parts. Usually, the behaviour of the components is well understood, while that of their composition remains largely unexpected, exhibiting so-called emerging properties. The advantage of computer systems is that their abstract machines can be easily run, and their behaviour inspected. Emerging properties are explicitly made visible and available for analysis and, if unwanted, the designer of the computer system can modify the associated abstract machine until the required behaviour is got.

Below, we address in a little more detail three complementary approaches to the specification of abstract machines, with particular attention to their connections with systems biology. They are very central to those research areas of computer science devoted to computational models, programming languages and tools. Roughly, the linguistic approach offers a clean, logical way of describing the elementary computational steps; from these, the transitions of the abstract machine are then obtained in a purely compositional manner. A different point of view considers directly the abstract machine as an automaton and concentrates on rather efficient methods and tools for validating system behaviour. The third, classical way is dual to the previous one: the abstract machine is represented as a grammar, or more generally as a rewriting system, offering a wide repertoire of results and of proof techniques.

We start from the linguistic approach. Its initiators are Fontana and Buss [FB96] who use a version of the lambda-calculus for modelling biochemical systems. The pioneering work by Regev, Silverman and Shapiro [RSS01] brought out the similarities between distributed, concurrent, mobile computer systems and biological systems, e.g. metabolic and gene regulatory networks, signalling pathways. Biological systems are made up of millions of biological components that are active simultaneously and that can interact to cooperate towards a common goal. Furthermore, the interactions between components are mainly binary and can occur only if the partners are correctly located (e.g. they are near enough, no membrane is dividing them, the affinity or propensity to interaction is sufficiently high).
Finally, the actual interactions may change the future behaviour of the whole system even if they occur locally. All these features describe distributed, concurrent, mobile computer systems as well, except maybe for these artificial systems have a smaller number of components. There are various process calculi, e.g. [Mil89,Hoa85,MPW92,CG98] that specify the form and the dynamic behaviour of systems, and that allow for analysing them.
Some of them have already been used and extended to a better use in the biological applicative domain. Particularly relevant in Systems Biology is the proposal by Priami, Regev, Silverman and Shapiro, who 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. 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 et al. proposed Bio-ambients [RPSCS04], a variant of 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, e. g. parent-child communications can be used to represent the interactions between compounds that reside in the cytosol and in the nucleus. Cardelli's Brane calculi [Car05] are a family of calculi for modeling the intreractions of dynamically nested membranes. The main difference w.r.t. previous approaches is that the active entities reside on membranes, and not inside them. The interaction primitives are classified into two groups: endocytosis/exocytosis and fusion/fission. The expressivity of these groups is investigated in [BG05, Bus05]. Projective Brane calculus [DP04] is a refinement of Brane Calculi where membrane actions are directed, and partitioned in two sets: the actions residing on the external layer of the membrane and the actions residing on the internal layer. In Beta-binders [PQ04,PQ05], pi-calculus like processes are encapsulated into boxes that interact with each other through typed interaction sites. Differently from BioAmbients and Brane calculi, in Beta-binders nesting of boxes is disallowed, but can be emulated. Process primitives include adding, hiding and unhiding a binder; two further operations, split and join, change the structure of boxes. A stochastic extension of Beta-binders has recently been defined [DPPQ06] to allow the quantitative modelling of biological phenomena. Danos and Laneve [DL03,DL04] and Chiaverini and Danos [CD03] proposed the Core Formal Molecular Biology, building up on the basic primitives of the pi-calculus. The behaviour of processes (compounds) and of set of processes (solutions) is given by a set of rewriting rules which account for, e.g. activation, synthesis, complexation. Cardelli and Pradalier [CP05] recently proposed a calculus combining the complexation/decomplexation operations on molecules with membrane interaction operations, à la Projective Brane Calculus.

Tightly related with this approach is the the great deal of work made using Petri nets and related models to represent biological systems. Although relevant, lack of space prevents us from surveying this important stream of research.

As mentioned above, there is a variety of semantically-based tools for the analysis of the behaviour of concurrent processes, e.g. for searching the state space or checking various semantic equivalences and preorders. Among these, we only mention the concurrency (e.g. www.dcs.ad.ac.uk/home/cwb) and mobility workbenches (e.g. www.it.uu.se/research/group/mobility/mwb), as well as tools that explicitly manage stochastic aspects, like the PEPA workbench (www.dcs.ed.ac.uk/pepa/), TwoTowers (www.uniurb.it/bernardo/twotowers/), and simulators that implement the Gillespie's algorithm [Gil77] over executions of terms of the stochastic pi-calculus: BioSpi (www.wisdom.weizmann.ac.il/~biopsi/) and SPiM (www.doc.ic.ac.uk/~anp/spim/). Due to the intrinsic complexity of biological systems also static analysis techniques (e.g. Abstract Interpretation [CC79]) appear particularly interesting to efficiently infer approximate information on the behaviour of biological systems. Indeed, simulation tools or automatic verification techniques have often an unacceptable complexity. In [GL05] a new abstract interpretation of BioAmbients have been proposed which is able to address both the quantitative and causal aspects of biological systems.

In the approach based on rewriting systems, the biological system is represented by a term and its behaviour is defined by rewrite rules. This approach has been used for modelling biochemical reactions in [Gil77,Gil01,Nak72,BCMMT05]. A single reaction is represented by a rewrite rule, and the choice which rule to apply among those applicable, is done according to a probability associated with the rule. The probability represents reaction speed. This approach can be merged with the linguistic one. A biological system is represented by using operators on terms, that have a clear biological meaning (e.g., the fact that an element is inside another or that two elements are adjacent). A term representing a system can be rearranged by using structural congruences. The behaviour of the system is described by a set or rewrite rules, that can easily lead to simulators.
Paun ([Pau02]) has introduced a new computational model based on the idea 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, which keep components apart and act as semi-permeable barriers, ensuring that certain substances always stay into the compartment while other substances stay out of it. Objects (DNA strands, molecules, etc.) and evolution rules (chemical reactions) are associated with each membrane. 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 by passing through the membranes. These systems have been used to model energy aspects connected to cellular reactions [FJ02a,FJ02b]; simulation of photosynthesis [Nis02]; communication processes within the cell [BAM03,BMPZ03,SOT03]; other biological aspects of organisms and systems have been considered [Ard02,Ard03,BFMZ03,FM03,HHGT01,Mar03,SFTT01,STT00,ST00,VPCD03]. In [BMMT06a] a new calculus, called Calculus of Looping Sequences (CLS for short), has been defined. The terms of the calculus are constructed by starting from basic constituent elements, while the behavior of a system is described by a set of rewrite rules to be applied to terms.

Many biological systems have a mixed discrete-continuous behaviour which cannot be characterized in a proper way using either discrete or continuous models. On one hand, their evolution is ruled by a continuous dynamical law concerning substance concentrations and gradients, and, on the other hand, the dynamical law changes depending on the system status. To model this kind of systems, called hybrid, Alur et al. introduced in [ACH95] the notion of hybrid automata. Intuitively a hybrid automaton is a “finite-state” automaton with continuous variables which change according to a set of continuous laws characterizing each discrete node of the automaton itself. The use of hybrid automata for modeling biomolecular networks has been described by Alur et al. [ABI01] and Mishra [Mis02]. Amonlirdviman et al. [AGAT02] demonstrated the utility of hybrid systems by modeling Drosophila planar cell polarity. Starting with the S-System formulation of Savageau and Voit, Antoniotti et al. [AMPPS03] used an additional automaton to broaden the set of representable systems, subsequently using full-fledged hybrid automata [APUM02]. Ghosh and Tomlin presented both a delta-notch [GT01,GT04] and a protein signaling networks [GT05] models based on the hybrid automaton formalism. Casagrande et al. [CMPM05] suggested a simple hybrid automaton model for the E. coli chemotaxis. Once the biochemical system has been formally specified, one needs to verify properties on such a description. Temporal logics [Pnu81] and model checking [CE82,QS82,CES86] are largely used to express hybrid system properties and to prove them over hybrid automata respectively. Temporal logics extend the propositional logic and express properties of transition sequences. In particular, besides using atomic propositions and traditional boolean connectives, temporal logics may specify time properties like either “eventually property P will hold”, “from now on property Q holds” or “property R will never hold”. Model checking is an automatic technique for verifying model’s properties. This technique has many advantages over traditional approaches like simulation or testing. In particular, model checking guarantees the correct and complete verification of a property dealing with all the behaviour of the system, whereas simulation and testing consider only some of the possible trajectories. In general the model checking problem for hybrid automata is not decidable [ACH95], but there are two different ways of handling this problem. The first is to identify hybrid automaton classes for which the problem is decidable and to use them. Many decidable classes have been discovered [ACH95,AD94,PV94,Kop96,LPS00,CMPM05, CPM05], but the restrictions on them make it difficult their use in analysing real systems. The second way makes use of approximated analysis, like bounded model checking [GPB05,FH05], abstract interpretation [ADI02,ADI03a,ADI03b], or quotient reduction [GP05a,GP05b,GP06], to get a partial result for the model checking problem, e.g. the property holds for at least 10’ from the initial conditions. <<<