Séminaire du 8 avril 2016

Lieu

LRDE : comment y aller

Programme

14h00-14h45: Alexandre Duret-Lutz (LRDE/EPITA), "Spot 2.0"

Abstract : transparentsSpot, une bibliothèque C++ de manipulation d'omega-automates pour le model checking. Les nouveautés sont assez nombreuses: la bibliothèque travaille maintenant avec des automates dont la condition d'acceptation peut être arbitrairement complexe (par exemple une combinaison booléenne de Streett et Rabin généralisé), de nouveaux outils en ligne de commande permettent de manipuler et produire ces automates, et la majeur partie des fonctionnalités est utilisable avec une surcouche de bindings pour Python.

Je montrerai en particulier:

  • des exemples d'utilisation tirés du cours d'initiation au model checking de l'Épita (travail sur la sémantique de LTL, et écriture d'un model checker jouet en quelques lignes de Python).
  • la facilité avec laquelle on peut chaîner les différents outils pour construire un pipeline de manipulation d'automates
  • une technique utilisant un SAT-solver pour synthétiser des automates équivalents mais avec d'autres conditions d'acceptation.

14h45-15h30 : Maximilien Colange(ENS de Cachan), "TiAMo, the Timed Automata Model-checker"

Abstract : transparentsJe présenterai TiAMo, un model-checker pour les systèmes temporisés développé au LSV. Les systèmes temporisés présentent une composante en temps continu, qui font de leurs espaces d'états des graphes infinis à branchement infini. Dans le cadre du model-checking, leur analyse repose essentiellement sur des abstractions permettant de se ramener à des graphes discrets. Nous nous concentrons sur les problèmes d'accessibilité dans les automates temporisés, et d'accessibilité optimale dans les automates temporisés à coûts positifs.

TiAMo est pensé comme une plateforme permettant la comparaison expérimentale des différents algorithmes et abstractions pour la vérification de systèmes temporisés. Je rappellerai les principaux problèmes algorithmiques qui se posent dans ce cadre, et les différentes solutions qui ont été proposées. Je présenterai également l'outil TiAMo, et les algorithmes d'analyse qu'il implémente.

15h30-16h00: pause café

16h00-16h30: vie du groupe