# 1st Bioss Workshop: "Systemic Symbolic Biology"

*September 18th, 2015*

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