Contact
Largouët Christine, clargoue@irisa.fr
Mots-clés
Intelligence artificielle, Model-checking, Aide à la décision, Ecosystèmes, Synthèse de contrôleur, Stratégies
Description
La modélisation dans le domaine agro-écologique est importante car elle permet de mieux comprendre les interactions entre l’environnement et les activités humaines. Les travaux basés sur la simulation restent difficiles à utiliser dans un contexte d’aide à la décision. En particulier la recherche de stratégies optimales restent un grand défi.
Une nouvelle approche consiste à représenter le système étudié dans un formalisme de systèmes à événements discrets. Ceci permet de profiter de l’efficacité du model-checking et d’utiliser la synthèse de contrôleur pour générer automatiquement des stratégies optimales. Des premiers travaux ont montré des limites de performance dans l’application des outils “classiques” de synthèse de contrôleur (Uppaal Tiga). Ces outils ne peuvent traiter que des modèles de taille limitée alors que les écosystèmes qui nous intéressent se caractérisent par leur grande taille (nombreux composants en interaction).
L’objectif de ce stage consiste à proposer des outils permettant d’effectuer la synthèse de contrôleur sur des applications réelles telles que les écosystèmes. Un premier travail consiste à explorer les nouvelles techniques de model-checking et de synthèse de contrôleur (vérification de systèmes multi-agents, model-checking robuste, etc.) afin de verifier leur adéquation au problème. Le modèle de l’écosystème est généralement construit de manière automatique après une description dans un langage de haut niveau des caractéristiques du système. Le modèle obtenu est généralement de grande taille et présente de nombreuses redondances. Afin de diminuer la complexité du modèle, une méthode de réduction du modèle, obtenue de manière automatique, sera proposée ; les propriétés du modèle devront cependant être respectées. Sur ce modèle réduit, les nouvelles techniques de model-checking et de synthèse de contrôleur permettant la recherche de stratégies seront testées et comparées.
