Séminaires
Séminaire du 8 avril 2016
Lieu
LRDE : comment y aller
Programme
14h00-14h45: Alexandre Duret-Lutz (LRDE/EPITA), "Spot 2.0"
Abstract : 
Spot, 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 : Je 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.