Résumé : L’utilisation croissante d’agents autonomes artificiels dans des secteurs comme le milieu hospitalier ou les transports amène à réfléchir aurespect de règles morales partagées par tous. Leproblème est d’autant plus crucial que les règlesmorales informellement validées par tous sontsouvent incompatibles les unes avec les autres,et que ce sont souvent des règles éthiques quiamènent l’humain, suivant les circonstances àprivilégier telle ou telle règle morale. Utiliser lapreuve pour vérifier qu’un agent respecte biendes règles morales et éthiques pourraient aiderà accroître la confiance que nous pouvons avoiren de telles unités logicielles. Dans cet article,nous montrons, en nous appuyant sur une étudede cas, comment, à partir de règles morales apriori contradictoires mais ordonnées par desrègles éthiques, nous parvenons à définir un ensemble de propriétés formelles qui, lorsqu’ellessont établies par un agent, permettent d’assurerque l’agent en question respecte bien la règleéthique souhaitée.

Résumé : Cet article se place dans le contexte de la validation de SMA grâce à la preuve de théorèmes.Il présente une étude de cas préliminaire faisantpartie d’un travail plus vaste dont l’objectif àlong terme est d’analyser dans quelle mesure detels outils de preuve peuvent être utilisés, pouraider à mettre au point un SMA. L’article décrit comment une erreur liée à un problème desynchronisation entre agents peut être caractérisée grâce à un échec de preuve. L’exploitationdes échecs de preuve permet ainsi de mettre enévidence un bug qui ne survient que dans uncontexte particulier d’exécution et qui n’auraitdonc pas été évident à détecter avec des techniques de debuggage classiques.

Résumé : 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 eectué 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.