Spécifier et vérifier en GDT4-D-MAS des ensembles dynamiques d’agents

Cet article traite de la preuve formelle de systèmes multi-agents à l’aide du modèle GDT4MAS. Ce modèle aborde la vérification formelle de la spécification jusqu’à la génération d’obligations de preuve en s’appuyant sur la logique du premier ordre. Toutefois, ce modèle ne permet pas de spécifier explicitement des comportements ayant trait au nombre d’agents présents dans le système, ce qui rend difficile l’expression de propriétés liées à l’ouverture du système, i.e. liées à l’apparition ou la disparition d’agents. Nous proposons alors une reformulation du modèle qui intègre explicitement des notions ensemblistes permettant d’exprimer la présence ou non d’agents dans le système, de considérer des actions permettant de créer ou détruire des agents et de spécifier plus simplement  leur initialisation. Nous illustrons l’application de ces concepts sur un exemple de système proie-prédateur.