**18 septembre 2015**à Nantes

### 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