Objectives

Bioss is a new French working group on the symbolic modelling of biologic systems, combining discrete mathematics and fundamental computer science with molecular biology and medicine. This thematic aims at studying information transmissions in biological systems, by using formal methods from computer science (or new ones) in order to model, analyse and understand the dynamics of complex living systems.
This first workshop aims at bringing together the members of the Bioss working group as well as anyone interested in the Bioss topics, and to discuss the current activities of our research interests. It will concentrate on the young generation, by giving invited PhD students and postdocs the opportunity to present their recent or current work. This will give a panorama, representative of the French activities on Symbolic Systems Biology.

Scope

The program will consist of invited talks, mainly by PhD students and postdocs.
Topics of Symbolic Systems Biology include, but are not limited to:\

• modelling of biological systems,
• discrete or hybrid formalisms,
• semantics (included stochastic),
• model verification,
• model reduction,
• prediction (under uncertainty),
• model inference.

Registration

Registration is free but mandatory through the CMSB registration page, even if you don't attend CMSB.

Programme

14:30 - 14:55
    Marc Bouffard - Extracting logic gates from a metabolic network, why and how ?
14:55 - 15:20
    Pauline Traynard - Logical modeling and model-checking of the mammalian cell cycle
15:20 - 15:45
    Julie Laniau - Metabolic network reconstruction with combinatorial optimization : influence of cross-compartment metabolites
15:45 - 16:00
    Coffee break
16:00 - 16:25
    Alexandre Rocca - Application of Formal Methods to Biological Systems Modelling
16:25 - 16:50
    Alexandre Temperville - Computation of sparse conservation laws and applications
16:50 - 17:15
    Louis Fippo-Fitime - Integrating time-series data on large-scale discrete cell-based models
17:15 - 17:40
    Pierre Boutillier - A new simulator for large Kappa models\

Abstracts

Marc Bouffard (Univ. Paris Sud / LRI) - Extracting logic gates from a metabolic network, why and how ?
Synthetic biology can be used to design artificial bio-devices that can perform successively the samples intake, its analysis and provide an integrated response. This will be performed by a logic function applied to the output of the sensors that respond to the bio-markers of the targeted pathology. This logic function is computed using logic circuits made of interconnected logic gates. For this purpose, a library of basic logic gates that can be wired together so as to function correctly in the same environment, will be automatically extracted from the metabolic networks of living organisms.

Pauline Traynard (Inria Paris-Rocquencourt) - Logical modeling and model-checking of the mammalian cell cycle
The molecular networks controlling cell cycle progression have been predominantly modelled using differential equations, an approach which demands to define complex regulatory terms with poorly characterised kinetic parameters. In contrast, qualitative dynamical models are easier to define, analyse and compose.
We revisit a boolean model for the core network behind the mammalian cell cycle (Fauré et al. Bioinformatics, 2006), taking into account recent advances in the characterisation of the underlying molecular networks to obtain a better qualitative consistency between simulations and documented mutants features. In particular, we refine the model to account for the role of the tumour suppressor protein Rb as a multifunctional protein, involved in independent proliferative control mechanisms. Using a multilevel rather than a boolean variable models the fact that differently phosphorylated forms of Rb result in different effects on other components of the network. We then introduce a crucial regulatory link between Rb and p27, another important cell cycle repressor.
We evaluate the dynamical properties of the resulting model with synchronous and asynchronous simulations using the software GINsim (http://www.ginsim.org). We also have designed temporal logic queries, enabling an efficient and automatic verification of key dynamical properties such as conditions on the activation of components or the order of changes of their levels, with the symbolic model checker NuSMV. Moreover, adding transition probabilities allow a stochastic simulation of the model with the software MaBoSS and provides new insights into the dynamical behavior of the system.

Julie Laniau (Inria Rennes) - Metabolic network reconstruction with combinatorial optimization : influence of cross-compartment metabolites

Alexandre Rocca (Univ. Joseph Fourier / Verimag) - Application of Formal Methods to Biological Systems Modelling
Modelling complex biological systems as differential equations mostly results in non-linear, high-dimensional, and stiff models. The validation of those models according to experimental results is often done with simulation. Moreover, to cope with the uncertainty of real biological systems, and to expand the experimental results to a more general model, uncertain parameters are used.To validate a large set of initial states and parameter values, a large number of simulation runs is needed. However, the result, being non-exhaustive, is not guaranteed. Formal verification techniques allow proving properties, with set-based reachability computation techniques, by replacing simulation runs with conservative sets of trajectories. Applying the Bernstein expansion of polynomials, we developed a reachability tool on polynomial systems with uncertain parameters. This tool takes advantage of the particular forms of the polynomials modelling of biochemical networks to speed up the Bernstein expansion.This allows a faster verification of complex biological systems. The tool is directly applied on a real system (Iron Homeostasis project). It is developed in collaboration with a biological experimentation team (LBFA, Grenoble) to address the needs of biologists.

Alexandre Temperville (Univ. Lille 1 / CRIStAL) - Computation of sparse conservation laws and applications
Conservation laws are a key-tool to study systems of chemical reactions in biology. After discussing about what good conservation laws can be, we propose a greedy algorithm, computing a sparsest set of conservation laws from a given set of conservation laws. Then, we briefly present an improvement of this algorithm, some benchmarks on Maple and Python codes of this algorihtm over a subset of the curated models taken from the BioModels database. At last, we will finish to talk about prospects of practical applications of this algorithm.

Louis Fippo-Fitime (École Centrale de Nantes / IRCCYN) - Integrating time-series data on large-scale discrete cell-based models
In this work we propose an automatic way of generating and verifying formal hybrid models of signaling and transcriptional events, gathered in large-scale regulatory networks.This is done by integrating temporal and stochastic aspects of the expression of some biological com- ponents. The hybrid approach lies in the fact that measurements take into account both times of lengthening phases and discrete switches between them. The model proposed is based on a real case study of keratinocytes differentiation, in which gene time-series data was generated upon Calcium stimulation.
To achieve this we rely on the Process Hitting (PH) formalism that was designed to consider large-scale system analysis. We first propose an automatic way of detecting and translating biological motifs from the PID database to the PH formalism. Then, we propose a way of estimating temporal and stochastic parameters from time-series expression data of action on the PH. Simulations emphasize the interest of synchronizing concurrent events.

Pierre Boutillier (Univ. Paris Diderot / PPS) - A new simulator for large Kappa models
When trying to model biological systems, one can either rely on so called "chemical reaction network" representations and use techniques based on multisets rewriting or ODEs for simulations. An alternative is to use representations that rely on reaction patterns also called rule-based. While the first method is extremely efficient when it applies, it requires somehow to compute the space of reachable species and is subject to combinatorial explosion as the number of simulated reactions grows rapidly. Kappa is a language based on graph pattern rewriting, that attemps to cope with the combinatorics of signalling pathways. A simulation step is based on Gillespie's algorithm and requires to maintain all rule's left hand sides matches at each state of the system. Keeping these matches up-to date is the bottleneck of the simulator. In this talk I will describe how we attempt to minimize the cost of this update operation.\

Dernière modification le 18/09/2015