Gaële Simon

Vers une aide au débuggage des SMA par l'exploitation d'échecs de preuve

Vérification formelle et éthique dans les SMA

L'utilisation croissante d'agents autonomes artificiels dans des secteurs comme le milieu hospitalier ou les transports amène à réfléchir au respect de règles morales partagées par tous. Le problème est d'autant plus crucial que les règles morales informellement validées par tous sont souvent incompatibles les unes avec les autres, et que ce sont souvent des règles éthiques qui amènent l'humain, suivant les circonstances à privilégier telle ou telle règle morale. Utiliser la preuve pour vérifier qu'un agent respecte bien des règles morales et éthiques pourraient aider à accroître la confiance que nous pouvons avoir en de telles unités logicielles. Dans cet article, nous montrons, en nous appuyant sur une étude de cas, comment, à partir de règles morales a priori contradictoires mais ordonnées par des règles éthiques, nous parvenons à définir un ensemble de propriétés formelles qui, lorsqu'elles sont établies par un agent, permettent d'assurer que l'agent en question respecte bien la règle éthique souhaitée.

Spécifier des agents composés d'agents avec les GDT

Dans cet article, nous spécifions une nouvelle extension du formalisme Goal Decomposition Tree pour décrire des agents composés d'agents. Cette notion correspond à une forme de décomposition particulière de but permettant d'introduire des agents spécifiques qui ont en charge la résolution des sous-buts du but décomposé ainsi. Nous décrivons la sémantique formelle de cette décomposition et nous définissons différents opérateurs pour la mettre en oeuvre. Nous décrivons également des cas d'utilisation typique de ce nouveau type de décomposition. Enfin, afin de préserver l'objectif principal des GDT (prouver des comportements d'agents), nous fournissons les schémas de preuve permettant de prouver la correction de tels agents. In this article, we formalize the notion of an agent made of agents by extending the Goal Decomposition Tree formalism. We not only give a formal semantics to this decomposition but we also define operators to introduce various ways of recursively defining agents. We also present design patterns that show various use cases of meta-agents. Finally, to preserve the essential GDT property that consists in allowing to prove agents behaviours, we give proof schemas that allow to prove the correctness of a meta-agent.