Sujet : Un cadre général pour la vérification de systèmes infinis probabilistes

Responsable : André Arnold
Encadrants : Jean-Michel Couvreur & Grégoire Sutre
Téléphone : 01 47 40 75 38, 05 40 00 33 36
e-mail : couvreur@labri.fr, sutre@labri.fr
Site Web : http://www.labri.fr/~couvreur, http://www.labri.fr/~sutre
Equipe : Modélisation, Vérification et Test de Systèmes Informatisés (MVTsi)

Présentation du sujet :

La modélisation de systèmes complexes fait intervenir à la fois des aspects probabilistes et des aspects infinis. Elle concerne non seulement l'étude de systèmes informatisés ou automatiques mais aussi le domaine en plein essor des modèles du vivant. Développer des techniques et des outils de vérification et d'analyse pour ces modèles est d'un intérêt fondamental.

Les systèmes probabilistes et les systèmes infinis font l'objet de recherches intensives dans le domaine de la vérification, mais peu de travaux traitent des deux aspects. L'objectif de cette thèse est la conception de techniques générales pour la vérification de systèmes infinis probabilistes. Dans un premier temps, il s'agira d'identifier des classes de modèles et de propriétés comportementales sur lesquelles le problème de la vérification est décidable. Un point de départ pourrait être l'étude des systèmes infinis "équivalents" à des systèmes finis, comme les systèmes temporisés. Au delà, il faudra s'intéresser aux systèmes ayant des comportements stationnaires ; cette propriété semble un préambule à la mise en oeuvre de méthodes de vérification pour les systèmes infinis. Dans un deuxième temps, il s'agira de développer des algorithmes et des outils de vérification, et de les confronter à des problèmes complexes issus du monde de l'informatique et des systèmes biologiques.

Mot-clés : vérification formelle, systèmes infinis, systèmes probabilistes, techniques symboliques, logique temporelle, sûreté de fonctionnement.

Commentaires :
Pour des références ou pour une description plus détaillée de ce sujet, n'hésitez pas à prendre contact avec les encadrants.