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