Vérification formelle du respect de valeurs morales dans les SMA

L’utilisation croissante d’agents autonomes artificiels dans des secteurs comme le milieu hospitalier ou les transports amene a reflechir au respect de regles morales partagees par tous. Le probleme est d’autant plus crucial que les regles morales informellement validees par tous sont souvent incompatibles les unes avec les autres, et que ce sont souvent des regles ethiques qui amenent l’humain, suivant les circonstances, a privilegier telle ou telle regle morale. Utiliser la preuve pour verifier qu’un agent respecte bien des regles morales et ethiques pourraient aider a accroitre la confiance que nous pouvons avoir en de telles unites logicielles. Dans cet article, nous montrons, en nous appuyant sur une etude de cas, comment, a partir de regles morales a priori contradictoires mais ordonnees par des regles ethiques exprimant un systeme de valeurs, nous parvenons a definir un ensemble de proprietes formelles qui, lorsqu’elles sont etablies par un agent, permettent d’assurer que l’agent en question respecte bien la regle ethique souhaitee.