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.