13h00 - 13h30 – Déborah Boyenval (I3S/Sparks)
Étude des checkpoints du cycle cellulaire : spécification et vérification
Le cycle cellulaire est par définition une succession d'évènements conduisant à la duplication sans erreur de l'ADN (phase S) et l'équitable division d'une cellule mère en deux cellules filles (phase M). Au cours de la progression du cycle cellulaire (G1-S-G2-M), l'intégrité de l'ADN est garantie notamment par les checkpoints. Nos travaux montrent que la modélisation discrète du cycle cellulaire permet de modéliser proprement la notion fondamentale de checkpoint. Un nouveau modèle multivalué du cycle cellulaire est présenté en suivant le formalisme de René Thomas. Le modèle se focalise sur la succession des évènements de régulation qui représente le cycle cellulaire. On y montre que plusieurs permutations de ces évènements sont admissibles, tout en permettant néanmoins de dégager des évènements clefs non permutables qui caractérisent les checkpoints. Cette étude a été rendue possible grâce à l'usage de deux types de méthodes formelles dédiées aux réseaux de régulation multivalués: la logique de Hoare "génétiquement modifiée" et le model-checking pour CTL. L'outil TotemBioNet combine efficacement ces deux approches formelles pour identifier exhaustivement les paramètres dynamiques des modèles compatibles avec nos définitions du cycle cellulaire et de ses checkpoints.
13h30 - 14h00 – Loïc Paulevé (CNRS/LaBRI/Formal Methods)
Most Permissive Boolean Networks in practice
Logical modeling, notably with Boolean Networks (BNs), is a
well-established approach that enables reasoning on the qualitative
dynamics of networks. However, (a)synchronous Boolean network, besides
being costly to analyze, can preclude the prediction of certain
behaviors observed in quantitative systems.
Most Permissive Boolean Networks offer the formal guarantee not to miss
any behavior achievable by a quantitative model following the same
logic. Moreover, MPBNs significantly reduce the complexity of dynamical
analysis, enabling to model genome-scale networks.
In this talk, after an overview of the motivation and properties of
MPBNs, I'll focus on their practical usage for the analysis of models
of biological networks.
Related material:
Dernière modification le 06/11/2020