17 novembre 2014
Amélie David (IBISC, Université d'Evry-Val-d'Essonne)La logique ATL (Alternating-time Temporal Logic) et ses extensions sont des langages naturels pour la spécification de systèmes ouverts, i.e. de systèmes interagissant avec leur environnement. Les composantes du système ainsi que l’environnement sont représentés par un jeu dans lequel les joueurs ou des coalitions de joueurs doivent trouver une stratégie pour atteindre leur objectif. La logique ATL+ correspond à l’extension permettant la description de plusieurs objectifs à l’intérieur d’un même stratégie. Nous souhaitons répondre de manière automatique et constructive au problème de la satisfiabilité: existe-t-il un modèle d’une formule donnée? Nous présentons donc une méthode de décision pour l’extension ATL+ basée sur les tableaux permettant de résoudre le problème de manière optimale en 2EXPTIME.