Seminar Room, ground floor (Building IMAG)
8 juin 2017 - 14h00
Itérations sur les politiques pour la vérification de systèmes dynamiques en temps discret.
par Assalé ADJE de Université de Perpignan
Résumé : Dans cet exposé, nous nous intéressons à la vérification formelle de propriétés numériques sur des systèmes dynamiques en temps discret par
analyse statique. Pour valider ces propriétés et garantir la sureté de la vérification, nous cherchons à calculer une sur-approximation précise des
états atteignables. Ce calcul est équivalent à résoudre un problème de plus petit point fixe pour une fonction similaire à un opérateur de
programmation dynamique de la théorie des jeux. En analyse statique, l'algorithme classique pour calculer ce point fixe est l'itération de Kleene
(appelée itérations sur les valeurs en théorie des jeux). Cette méthode est, en général, lente et nécessite des techniques d'accélération
qui dégrade la précision théorique de l'algorithme. Dans cette présentation, nous considérons donc une méthode alternative issue de
la théorie des jeux appelée itérations sur les politiques afin de résoudre les problèmes de point fixe apparaissant dans le calcul
de la sur-approximation des états atteignables.
