Jeudi 9 Mars


Retour à la vue des calendrier
Jeudi 9 Mars
Heure: 10:30 - 11:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Hybride Modelling, Analysis and Quantitative Verification of Large Biological Regulatory Networks
Description: Louis Fippo Fitime Biological Regulatory Networks (BRNs) are usually used in systems biology for modelling,
understanding and controlling the dynamics of different biological functions (differentiation,
proliferation, proteins synthesis, apoptose) inside cells. Those networks are enhanced with
experimental data that are nowadays more available which give an idea on the dynamics of BRNs components.
Formal analysis of such models fails in front of the combinatorial explosion of generated behaviours
despite the fact that BRNs provide abstract representation of biological systems.

This thesis handles hybrid modelling, the simulation, the formal verification and control of Large
Biological Regulatory Networks. This modelling is done thanks to stochastic automata networks, thereafter
to Process Hitting by integrating time-series data.

Firstly, this thesis proposes a refining of the dynamics by estimation of stochastic and temporal (delay)
parameters from time-series data and integration of those parameters in automata networks models. This
integration allows the parametrisation of the transitions between the states of the system. Then,
a statistical analysis of the traces of the stochastic simulation is proposed to compare the dynamics
of simulations with the experimental data.

Secondly, this thesis develops static analysis by abstract interpretation in the automata networks
allowing efficient under- and over-approximation of quantitative (probability and delay) reachability properties.
This analysis enables to highlight the critical components to satisfy these properties.

Finally, taking advantage from the previous developed static analyses for the reachability properties in the
qualitative point of view, and from the power of logic programming (Answer Set Programming), this thesis addresses the domain
of control of system by proposing the identification of bifurcation transitions. Bifurcations are
transitions after which the system can no longer reach a state that was previously reachable.