Comment les échecs de preuve peuvent aider à la correction de spécifications erronées de Systèmes Multi-Agents

Depuis plusieurs années, nous avons défini le modèle GDT4MAS (dont la sémantique repose sur la LTL) afin de spécifier formellement les systèmes multi-agents dans l’objectif de permettre leur validation par la preuve. A cet effet, nous avons effectué des travaux sur l’utilisation des techniques de preuve de théorèmes dans ce contexte. Nous avons pour cela défini un système de génération d’obligations de preuve à partir de la spécification GDT4MAS, obligations de preuve qui peuvent ensuite être confiées à un prouveur de théorèmes.