Thèse Jeux Robustesse et Model Checking pour les Automates de Dimension Supérieure H/F Doctorat.Gouv.Fr

Établissement : Institut Polytechnique de Paris Télécom SudParis École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris Laboratoire de recherche : SAMOVAR - Services répartis, Architectures, Modélisation, Validation, Administration des Réseaux Direction de la thèse : Natalia KUSHIK Début de la thèse : 2026-10-15 Date limite de candidature : 2026-10-02T23:59:59 Cette thèse s'articule autour des thèmes suivants :

- Jeux sur HDA et HDTA : proposer un modèle formel pour les jeux sur HDA. Le premier axe de cette thèse est de formaliser les jeux sur HDA et ses variantes, et d'étudier différents problèmes classiques (jeux à somme nulle, équilibre de Nash, etc.).

- Robustesse de HDA/HDTA : étendre les travaux récents sur la robustesse des automates temporisés aux automates temporisés de dimension supérieure. Pour ce faire, il est nécessaire de formaliser les distances entre les exécutions et leurs étiquettes dans HDTA, comme cela a été fait récemment pour les automates temporisés.

- Application et Implémentation : appliquer ce formalisme à la vérification de la robustesse et à la synthèse pour des systèmes concurrents et des systèmes industriels. Le troisième objective de cette thèse est d'étendre les travaux sur l'utilisation de HDA pour contrôler des systèmes concurrents et industriels. Finalement, implémenter les résultats dans un outil de vérification de modèles pour HDA ou HDTA, par exemple l'outil pn2HDA de Philipp Schlehuber-Caissier. Les jeux sur graphes constituent un modèle puissant pour enrichir les objectifs classiques sur les graphes et, par extension, sur les automates. Ils répartissent les actions ou les positions entre un ensemble de joueurs. Ainsi, chaque joueur contrôle une partie spécifique de l'automate et attend les décisions des autres lorsqu'il n'en a pas le contrôle. Plusieurs travaux ont réussi à étendre ce principe à d'autres variantes telles que les automates temporisés et les réseaux de Petri, et à l'appliquer à la vérification. Cependant, ces modèles n'utilisent que la concurrence entrelacée. Les automates de dimension supérieure (HDA) sont un modèle basé sur les automates qui étend les automates classiques pour permettre une concurrence non entrelacée. Ils sont très expressifs, généralisant à la fois les automates et les réseaux de Petri (ces derniers pour plusieurs versions de leur sémantique de concurrence). - Proposer un modèle formel pour les jeux sur HDA : formaliser les jeux sur HDA et ses variantes, et d'étudier différents problèmes classiques (jeux à somme nulle, équilibre de Nash, etc.);

- étendre les travaux récents sur la robustesse des automates temporisés aux automates temporisés de dimension supérieure : formaliser les distances entre les exécutions et leurs étiquettes dans HDTA, comme cela a été fait récemment pour les automates temporisés;

- appliquer ce formalisme à la vérification de la robustesse et à la synthèse : implémenter les résultats dans un outil de vérification de modèles pour HDA ou HDTA.