December 6, 2010
Catalin Dima (LACL) Salle des thèses
Les travaux de recherche présentés s’inscrivent dans le domaine de la vérification formelle des systèmes multi-agents et/ou temps réel. Une partie des travaux a eu comme point de départ le besoin de spécifier de manière plus fine certaines propriétés de sécurité telles que l’absence de fuite d’information ou l’authenticité, des propriétés de sécurité dans des protocoles de groupe ou le calcul de la capacité des canaux cachés. Nous avons montré que certaines de ces propriétés nécessitent des modèles multi-agents et sont naturellement spécifiables dans des logiques temporelles épistémiques. Par la suite, nous nous sommes intéressés aux problèmes de satisfiabilité et de model-checking dans ces logiques et à l’étude des classes d’automates avec observation partielle. Les résultats obtenus raffinent davantage la séparation entre le décidable et l’indécidable dans le model-checking des logiques temporelles épistémiques et permettent une meilleure compréhension de l’expressivité de ces logiques et/ou leur relation avec des classes d’automates d’arbres. Les recherches sur le calcul de la capacité des canaux cachés impliquent aussi des modèles multi-agents simplifiés et utilisent des résultats de la théorie des relations rationnelles, de la théorie des graphes et de la théorie des matrices nonnégatives.
D’autre part, nos travaux ont aussi porté sur les propriétés algorithmiques des modèles de systèmes temps réel tels que les automates à chronomètres ou à horloges inexactes. Les résultats de décidabilité et d’expressivité obtenus raffinent certaines techniques d’automates temporisés et pourraient s’appliquer à l’étude de l’ordonnançabilité ou de l’implémentabilité des systèmes embarqués.