Plan de l'exposé : - Modèles & logiques formels, cohérence, validation - Formalisation des réseaux de régulation biologique - Logique temporelle et Model Checking - Exemple (J.Guespin)~: Pseudomonas aeruginosa . Cohérence par Model Checking . Extraction automatique de plans d'expériences . Propriétés expérimentalement observables - Questions d'actualité