Projet ANR-13-BS02-0011 – Stoch-MC : Modèles stochastiques: passage à l’échelle pour le Model Checking
Programme : Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2)
Année de financement : 2013
Coordinateur du projet : Monsieur Blaise GENEST (Inria, Centre de recherche de Rennes - Bretagne Atlantique, equipe SUMO)
Partenaires : Inria Centre Paris - Rocquencourt; Supervision Of Large Modular And Distributed Systems; Laboratoire Bordelais de Recherche en Informatique; Institut de Recherche en Informatique Fondamentale
Montant : 361900.0 euros
Durée : 48 mois
Résumé : STOCH-MCModèles stochastiques: passage à l’échelle pour le Model Checking.
Scalable Model Checking et Applications en Biologie SystémiqueL'objectif de notre projet de recherche STOCH-MC est de développer le model-checking passant a l'échelle de très grand systèmes stochastiques et qui apporte des réponses exactes. Les grands systèmes stochastiques apparaissent naturellement dans de nombreux contextes, des réseaux aux systèmes biologiques. Nous démontrerons les techniques que nous développerons sur deux systèmes biologiques: un modèle de mort chez les cellules Héla et un modèle de réponse au stress chez la levure.
Model-Checking exact à travers des approximationsNotre technique centrale est d'obtenir des résultats exacts à travers des calculs approchés, permettant un passage à l'échelle jusqu'au très grand système. Les résultats sont analysés pour voir si une réponse exacte peut être dérivée (par exemple par suivi de la précision de l'approximation). Si une réponse exacte ne peut être obtenue, l'approximation sera recalculée avec une meilleure précision.Nous considérons deux types de modèles:- Les modèles purement stochastiques (Chaine de Markov, Réseaux Dynamiques (DBNs)). Cela permet de modéliser le comportement de grands systèmes biologiques tels que la voie de signalisation de l'apoptose chez Héla sous traitement de Trail.- Les Processus de Décision Markovien (MDPs, ainsi que différentes sémantiques tel que les automates probabilistes de Rabin), ce qui permet de modéliser du contrôle stochastique, par exemple pour une population de levures sous chocs osmotiques.
Résumé de la soumission : Le model-checking est aujourd'hui un domaine de recherche mature, qui a obtenu le prix Turing en 2007. Il consiste en la description formelle d'un système en un modèle mathématique, la formalisation des propriétés attendues dans une logique, et en la conception d'algorithmes pour décider si le modèle satisfait les propriétés. Le model-checking a commencé avec des systèmes Booléens, des modèles à états finis... Cela est maintenant bien établi. Afin d'appréhender des systèmes réalistes (et donc gros), des techniques d'abstraction comme la méthode CEGAR (pour counter-example guided abstraction [CCKSVW02]), ou l'interprétation abstraite (les travaux de Cousot et al.) ont été développées.Ces techniques sont très efficaces pour vérifier de gros programmes séquentiels, graçe aux prédicats Booléens (la variable x a une valeur plus petite que 2). Cependant, les techniques d'abstraction courantes ne conviennent pas à la vérification de gros systèmes probabilistes. Pour vérifier de gros systèmes probabilistes, le model-checking statistique, basé sur des simulations de Monte Carlo, peut être utilisé. Toutefois il ne permet de donner que des réponses correctes avec forte probabilité, mais pas sures. Il n'existe pas de technique de model-checking exact qui traite des gros systèmes stochastiques (par exemple des chaines de Markov a 10^20 états, obtenues par 20 variables pouvant prendre chacune 10 valeurs différentes). L'outil PRISM et ses concurrents permettent de gérer environ 10^10 états au maximum. Pour cette raison, Clarke et Cousot ont lancé l'initiative CMACS (Computational Modeling and Analysis for Complex Systems) afin de créer MCAI 2.0, la nouvelle génération de model-checking et interprétation abstraite.Le but de notre projet Stoch-MC est de développer des techniques de model-checking pouvant traiter de gros systèmes probabilistes en fournissant des réponses sures. Les gros systèmes probabilistes apparaissent naturellement dans de nombreux contextes, des réseaux aux systèmes biologiques. Nous démontrerons nos techniques sur deux modèles clefs: un modèle de mort de cellules Hela et un modèle de réponse au stress dans la levure.Notre idée de base pour obtenir des algorithmes efficaces repose sur la possibilité d'approcher les probabilités. Une borne sur l'erreur dans l'approximation est calculée a posteriori, en utilisant les caractéristiques du modèle. On obtient donc un intervalle de probabilité ([0.4,0.6]) plutôt qu'une valeur précise comme dans les outils actuels. Si la réponse n'est pas suffisamment précise (la probabilité est-elle supérieure a 0.45 ?), on alloue plus de temps à l'approximation pour affiner l'intervalle, jusqu'à ce qu'une réponse certaine soit donnée. Ceci imite l'approche CEGAR.Notre approche repose sur plusieurs ingrédients. Tout d'abord, on proposera des algorithmes paramétrés permettant une bonne analyse approchée. Le paramètre permet d'augmenter la précision, au prix d'un temps de calcul plus grand. Deuxièmement, on proposera une analyse de l'erreur pour en évaluer une borne, comme nous l'avons fait dans [AAGT12, PALGT12]. Le but à long terme est le model-checking de gros processus de décision markoviens (MDP). En biologie des systèmes, par comparaison aux chaines de Markov, les MDP permettent des modèles avec plusieurs modes (saturé, non saturés…), ou plusieurs possibilités (par exemple sur la quantité de médicaments à injecter). Le model-cheking du MDP revient alors à déterminer les choix optimaux pour une fonction de gain donnée, qui permet par exemple exhiber les comportements corrects.Disposer d’algorithmes efficaces de model-checking général pour de gros MDP n'est pas envisageable dans les 4 prochaines années. Néanmoins, nous développerons des techniques pour les principales facettes du problème et montrerons leur applicabilité aux pathways biologiques, démontrant que le model-checking exact de gros MDP est possible à terme. Ceci sera la base d'une proposition d'ERC dans 4 ans.
Résultats : Les résultats obtenus à T0+17mois sont:
- Nous avons obtenu un premier modèle de DBN (utilisant des tables de probabilités conditionnelles creux) pour la voie de signalisation de l'apoptose. (T5)
- Nous avons un prototype d'inférence approchée pour les DBNs (avec et sans représentation creuse). Les expérimentations  sont en cours pour comprendre sa précision. (T2)
- Nous avons une analyse théorique de l'erreur à chaque étape,  exprimée en terme de la pseudo distance de Kullback-Leibler. (T3)
Perspectives : Ce projet ANR regroupe des chercheurs de Méthodes Formelles, de Biologie Systémique et aussi de théorie de l'information. Cette combinaison unique a déjà porté ces fruits pour la modélisation de système biologique sous forme de DBN et de l'inférence de DBN.
Au-delà des défis importants de ce projet ANR, c'est a dire obtenir des résultats tangibles pour les systèmes biologiques - ce qui est connu comme compliqué, nous voulons démontrer que le Model checking peut être utiliser pour analyser des systèmes complexes. Notre but a long terme est d'être capable de générer automatiquement des contrôleurs pour de grands modèles de populations de cellules. Le projet STOCH-MC est la première étape pour montrer que cela est réalisable.
Publications et brevets : Quelques publications au coeur du projet STOCH-MC.
L. Maruthi, I. Tkachev, A. Carta, E. Cinquemani, P. Hersen, G. Batt. , A. Abate. Towards real-time control of gene expression at the single cell level: a stochastic control approach CMSB 2014, LNCS/LNBI, Springer, 155-172.
François Bertaux, Szymon Stoma, Dirk Drasdo, Gregory Batt. Modeling dynamics of cell-to-cell variability in TRAIL-induced apoptosis explains fractional killing and predicts reversible resistance. PLoS Computational Biology, 10(10):e1003893, 2014.
François Dufour Tomás Prieto-Rumeau. Approximation of average cost Markov decision processes using empirical distributions and concentration inequalities STOCHASTICS, 2015.
Manindra Agrawal, S. Akshay, Blaise Genest, P.S. Thiagarajan. Approximate Verification of the Symbolic Dynamics of Markov Chains. JACM 62(1): 34-65, 2015.