Research interests:
Keyword
Formal Methods for in-silico biology, Computational models in systems biology, simulation, model checking, workflow management systems, Hybrid Automata, Agent-based technology.
In-silico analysis using workflow management systems
An in-silico experiment can be naturally specified as a workflow of activities implementing, in a standardized environment, the process of data and control analysis. A workflow has the advantage to be reproducible, traceable and compositional by reusing other workflows. In order to support the daily work of a bioscientist, several Workflow Management Systems (WMSs) have been proposed in bioinformatics. Generally, these systems centralize the workflow enactment and do not exploit standard process definition languages to describe, in order to be reusable, workflows. While almost all WMSs require heavy stand-alone applications to specify new workflows, only few of them provide a web-based process definition tool.
We have developed BioWMS, a Workflow Management System to support the definition, the execution and the results management of an in-silico experiment through a web-based interface. BioWMS, implemented on BioAgent/Hermes architecture, generates dynamically domain-specific, agent-based workflow engines from a user workflow specification. Our approach exploits the proactiveness and mobility of agent-based technology to embed the application domain features inside agents behaviour. The resulting workflow engine is a multiagent system -a distributed, concurrent system- typically open, flexible, and adaptative.
Click here to watch the video of BioWMS
Computational models in systems biology
Systems biology is a multidisciplinary field whose goal is to provide a
systems-level understanding of biological phenomena by uncovering their
structure, dynamics and control methods. A main focus of
systems biology is to devise mathematical or formal models that capture
significant aspects of in vitro or in vivo experimental data, while remaining
amenable to both quantitative and qualitative analysis. Currently, the most
popular modeling approach is to use complex systems of nonlinear
differential equations, describing in great detail the underlying biological
phenomena. These models, however, are not particularly suitable for
formal analysis, and impose high computational demands on simulation,
especially in large-scale 2D and 3D networks. Simulation at the organ
or even the cell level is thus rendered impractical.
Considering this state of affairs, systems biology could greatly benefit from
the development of techniques that given a system of nonlinear differential
equations, (semi-automatically) constructs a more abstract model that preserves
the properties of interest. One promising approach is based on the use of
Hybrid Automata (HA) as a modeling formalism for
complex biological processes. HA are an extension of finite
automata that allows one to associate a continuous behavior with each state.
Simulation
I'm interested on efficent simulation techniques for biological systems. In particular we are developing a simulator, CellExcite, in order to reproduce in silico the emergent behavior of excitable tissues such as cardiac tissue. We can reproduce several phenomena such as fibrillation and defibrillation using a strong electric shock as the the following movies show.
Ventricolar Fibrillation
(Tissue of 400x400 cells)
|
Defibrillation
(Tissue of 400x400 cells)
|
|
|
|
 |
Spatial Model Checking
One of the most important and intriguing questions in systems biology is how to formally specify emergent behavior in biological tissue, and how to efficientlypredict and detect its onset. A prominent example of such behavior is electricalspiral waves in spatial networks of cardiac myocytes (heart cells). Spiral waves of this kind are a precursor to a variety of cardiac disturbances, including atrial
fibrillation (AF), an abnormal rhythm originating in the upper chambers of the heart. Moreover, the likelihood of developing AF increases with age.
In the paper [1], we addressed this question by proposing a simple and efficient method for learning and automatically detecting the onset of spiral waves in cardiac tissue. Underlying our method is a linear spatial-superposition logic (LSSL), which we have developed for specifying properties of spatial networks. Our method also builds upon hybrid-automata, image-processing, machine-learning and model-checking techniques to first learn an LSSL formula that characterizes such spirals. The resulting formula is then automatically checked against a quadtree (SQT) representation of the scalar electric field, produced by simulating a hybrid automata network modeling the myocytes, at each discrete time step. The SQT representation is obtained via hybrid abstraction and hierarchical superposition of the elementary units within the field.
[1] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S.A. Smolka and A. Wasilewska. Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes. In Proc. of HSCC'08, the 11th International Conference on Hybrid Systems: Computation and Control, St. Louis, USA, April, 2008, pp. 229-243, Springer, LNCS 4981.
Oscillators Model Checking and Control
Synchronization phenomena in large populations of interacting components arewidely represented in nature and intensively studied as physical, biological, chemical, and social systems. In Biology, examples include networks of pacemaker cellsin heart, nervous system, group of synchronously flashing fireflies, just to mention some of those analyzed by Strogatz in his exciting book [2]. Understanding a synchronized collective behavior is essential in Systems Biology especially for developing methods to control the dynamics of systems with desired properties.The distributed synchronization of biological systems is commonly modeled using the theory of coupled oscillators proposed by several authors Art Winfree, Charles S. Peskin and Yoshiki Kuramoto. In this theory, each member of the population is modeled as a phase oscillator running independently at its own frequency. The synchronization could be achieved coupling each oscillator to all the others and making them to interact with a certain strength. Whereas, the control is achieved either by introducing articifial oscillators or a new impulse, by changing the parameters of individual oscillators.
In the paper [3], we defined a subclass of timed automata, called oscillator timed automata, suitable to model oscillators. Then, we have introduced an interaction semantics which is parametric w.r.t. a model of synchronization. The main advantage of our approach is that although the timed automata show different behaviours, w.r.t. the original ones, when interacting, we do not need to change their structure. This is obtained by using a global time measure, which is the one of the observer, and several internal relative time measures, one for each oscillator, which are then re-scaled to the gloabal time.
We also provide a Kuromoto Synchronization Logic (KSL) in order to specifyproperties on synchronization, during a simulation, of Kuramoto based oscillators.Moreover, we propose a model checking algorithm for the logic. We test it byverifying some properties with a prototype simulator and model checker that wehave implemented.
[2] Strogatz, Steven (2003). Sync: The Emerging Science of Spontaneous Order.
[3] Model Checking Biological Oscillators. Ezio Bartocci, Flavio Corradini, Emanuela Merelli, Luca Tesei. In the proceedings of the 2th From Biology To Concurrency International Workshop (FBTC'08), Reykjavik, Island, July, 2008. Electronic Notes in Theoretical Computer Science. 2008.
