• Thèse
  • Caen

Site Laboratoire GREYC

Bonjour,

Nous proposons une thèse au laboratoire GREYC (UMR CNRS 6072) dans le domaine de la preuve et des systèmes multi-agents :

  • Sujet : spécification d’un système multi-agents par l’analyse d’échecs de preuve
  • Mots-clés : systèmes multi-agents, vérification, preuve automatique, raisonnement, logique
  • Encadrement : Bruno Zanuttini et Gaële Simon
  • Environnement : Equipe MAD – Laboratoire GREYC (Groupe de Recherche en Informatique, Image et Instrumentation de Caen)
  • Financement :  durée prévue de 3 ans sous réserve de financement par la Région, ou sujette à concours via des allocations établissement
  • Début de thèse : 1er Octobre 2024
  • Profil recherché : Étudiants en Master 2 d’Informatique   ou élèves-ingénieurs en dernière année (BAC+5) intéressés par la logique, la preuve et les systèmes multi-agents.
  • Candidatures : contacter Bruno Zanuttini (bruno.zanuttini@unicaen.fr) et Gaële Simon (gaele.simon@unicaen.fr) en envoyant un CV, une lettre de motivation ainsi que les notes disponibles de l’année en cours. Les candidatures seront étudiées au fil de l’eau.

Pour plus de détails, consulter la description du sujet ci-dessous.

Pour les candidats intéressés et souhaitant plus d’informations, un projet plus détaillé peut être envoyé sur simple demande.

Cordialement,

Bruno Zanuttini et Gaële Simon

____________________________

Equipe MAD – GREYC Université de Caen-Normandie

Proposition de sujet de thèse : Spécification d’un système multi-agents par l’analyse d’échecs de preuve

Mots-clefs : Systèmes multi-agents ; Vérification ; Preuve automatique ; Raisonnement ; Logique

Contexte thématique : Ce sujet de thèse se place dans le cadre de la preuve formelle de systèmes multi-agents (SMA). Un SMA est un système composé d’entités artificielles autonomes en interaction, conçu pour des objectifs divers, notamment de simulation [BN13, DB05, PHDL07]1. Quel que soit l’objectif, la conception d’un tel système consiste essentiellement à spécifier le comportement de chacun des agents ou types d’agents. C’est toutefois un problème extrêmement difficile, en particulier du fait de la grande diversité d’exécutions possibles de tels systèmes. Pour cette raison, la communauté a proposé de nombreux langages de spécification [Rao96, 3APL, GOAL], accompagnés d’outils diversifiés [Jason, Jade, Gama]. Dans ce contexte, l’équipe MAD du laboratoire GREYC mène depuis plusieurs années des travaux visant à développer une approche complète de conception, allant de la spécification logique à l’exécution du système spécifié [MSSZ07, MS13, MS17, MS19]. L’originalité de cette approche nommée GDT4MAS (Goal Decomposition Trees for MultiAgent Systems) est de proposer un langage de spécification accompagné d’un système de preuve automatique. Le langage de spécification intègre à la fois les aspects comportementaux des agents et les propriétés attendues du système. Il permet donc à la fois d’exécuter ce système et, via le système de preuve associé, de vérifier (semi-)automatiquement que toutes les étapes de la conception respectent les propriétés attendues.

Objectif de la thèse : Cette thèse vise à proposer une boite à outils d’exploitation d’échecs de preuve, pour accompagner les concepteurs de SMA dans un processus de conception assisté par la preuve. Ces travaux s ’inscrivent en effet dans une approche mettant l’accent sur un développement incrémental de la spécification. Dans ce cadre, il s’agit donc de proposer des outils permettant au concepteur d’exploiter les échecs de preuve au fur et à mesure de la conception pour corriger et/ou compléter les spécifications du SMA. En effet, si l’échec de preuve est lié à une spécification erronée, incomplète ou imprécise, les outils doivent aider à identifier les parties de la spécification en cause et à déterminer comment les corriger pour résoudre le problème. Toutes ces tâches sont particulièrement difficiles si l’on n’est pas un spécialiste de la preuve et du prouveur utilisé. Travaux connexes À notre connaissance, de tels outils ne sont pas mentionnés dans la littérature sur les SMA. Cependant, l’exploitation d’échecs de preuve a été en partie étudiée dans la littérature sur la preuve de théorèmes et la vérification de programmes. La preuve de programmes est utilisée avec succès depuis plus de vingt ans dans l’industrie, pour la vérification de systèmes dont dépendent des vies humaines. Cependant, elle repose sur des prouveurs automatiques qui ne prouvent pas tous les théorèmes au-delà de la logique propositionnelle. Par ailleurs, l’utilisation de prouveurs interactifs comme PVS [ORS92] ou Isabelle [Pau94] nécessitent une grande expertise de la preuve et du prouveur. C’est pourquoi des travaux visent à aller plus loin en proposant des aides à l’analyse d’échecs de preuve. Par exemple, STADY est un outil permettant, à l’aide de tests ciblés, de catégoriser un échec de preuve d’une spécification prenant la forme d’un programme C annoté [PKBGJ16]. Dans le cadre de l’Atelier B [Abr96], un outil appelé ProB permet de générer un contre-exemple à partir d’un échec de preuve [KBL15] afin notamment d’aider à la détection d’inconsistances dans la spécification. Dans le cadre de la preuve de spécifications de programmes ADA, il est proposé d’exploiter des contre- modèles générés par des SMT-Solvers [HMM16] pour les transformer en contre-exemples proposés à l’utilisateur sous forme de commentaires insérés dans le code à vérifier. Le point commun de ces différents types de travaux est la nécessité de proposer à l’utilisateur un ensemble d’informations lui permettant d’analyser des échecs de preuve, de la façon la plus intelligible possible et avec le moins de connaissances possible sur le prouveur. Cela implique notamment de pouvoir exprimer les contre-exemples en utilisant les variables du programme, et demande également de pouvoir fournir des informations sur la localisation de l’erreur. Dans certains cas, il peut être envisagé d’aller plus loin en proposant éventuellement des solutions de correction de la spécification. . Dans le cas où l’erreur dans le théorème est liée à un manque d’hypothèses, des techniques de type abduction ont été envisagées pour proposer les hypothèses à ajouter afin de corriger le théorème dans le cadre de preuves par induction [Mon03, DMN06]. D’autres travaux plus généraux, comme le système ABC sur la mise à jour des connaissances d’un agent représentées sous la forme d’une théorie logique [LBS18], ou encore le système EXPLAIN [DD13], permettant de mettre en œuvre un algorithme d’inférence abductive, peuvent être étudiés et adaptés à la correction de théorèmes de la spécification. Les travaux menés dans cette thèse pourront ainsi s’appuyer sur ces différentes approches pour les adapter à la conception de SMA. D’un point de vue technique, le caractère innovant, principal verrou scientifique, provient de l’articulation entre les spécifications d’un SMA et les théorèmes que l’on essaie de prouver : les échecs de preuve devront permettre de revenir sur la spécification à partir de laquelle ces théorèmes sont générés. L’approche GDT4MAS, développée dans l’équipe et reposant directement sur la preuve de théorèmes, fournira un cadre particulièrement adapté à ces travaux. Toutefois, la vérification de spécifications formelles par la preuve peut être envisagée sur d’autres langages formels [Rao96, 3APL]. Les outils proposés devront donc, autant que possible, être applicables à un grand nombre de systèmes de conception de SMA aidés par la preuve.
(1 La liste des références bibliographiques se trouve en fin de document)

Originalité de l’approche : La quasi-totalité des travaux existant dans le domaine de la preuve de systèmes multi-agents reposent sur du model-checking [Rai06]. Le principe général du model-cheking est de partir d’une spécification formelle exécutable, et de vérifier que toutes les traces d’exécution possibles du système vérifient bien les propriétés attendues. Le grand atout de cette approche est qu’elle est entièrement automatique, d’où son grand succès dans le domaine de la preuve de SMA. Cependant, cela nécessite d’avoir une spécification suffisamment complète et précise pour être exécutable. De plus, cela implique que le système spécifié puisse se ramener à un nombre fini et raisonnable d’états, ce qui représente l’un des principaux inconvénients de cette approche notamment dans le cas particulier des SMA. De plus, un nombre fini d’états ne permet pas de faire la preuve d’un SMA quel que soit le nombre d’agents présents dans le système. Pour un certain nombre de systèmes néanmoins, le nombre d’agents est connu et figé dès le départ, ce qui rend ces techniques utilisables pour un nombre raisonnable d’agents. L’approche utilisée dans le cadre de GDT4MAS repose sur la preuve de théorèmes en logique du premier ordre, ce qui rend possible des preuves plus générales (nombre infini d’états notamment). Cela permet des preuves indépendantes du nombre d’agents, et sur des spécifications incomplètes, rendant possible un processus incrémental. Cependant, en utilisant cette approche, on peut être confronté à des impossibilités de preuve liées à l’incomplétude de Gödel et à la semi-décidabilité de la logique du 1er ordre à laquelle on adjoint l’arithmétique. Cela rend donc en théorie la preuve de théorèmes non complètement automatisable. Néanmoins, dans les cas réels, peu de théorèmes appartiennent aux deux catégories précédentes. De plus, dans GDT4MAS, une attention particulière a été portée sur le fait de générer des théorèmes essentiellement prouvables par des stratégies généralistes et automatiques des prouveurs. L’enjeu de la thèse est de définir, dans le cadre d’une approche type GDT4MAS, un ensemble d’outils d’analyse d’échecs de preuve permettant d’aboutir à un véritable processus de conception de SMA accompagné par la preuve. Une telle approche n’existe pas actuellement, notamment car les informations fournies par un model-checker en cas d’échec de preuve sont difficiles à exploiter. Le concepteur est donc assez démuni lorsque la preuve échoue, ce qui est un frein énorme à la conception des SMA.

Encadrement : La thèse sera encadrée par deux membres de l’équipe MAD, Bruno Zanuttini (PU) en tant que directeur, et Gaële Simon (MCF), en tant que co-encadrante. L’encadrement de la thèse permettra d’apporter au (à la) doctorant(e) l’expertise nécessaire sur deux aspects : Bruno Zanuttini, sur le processus abductif et la spécification logique d’actions [NZ08, SNZ21], et Gaële Simon, sur la spécification et la preuve de SMA [MSSZ07, MS13, MS19].

Bibliographie
[3APL] https://www.cs.uu.nl/3apl/ [Abr96] J.-R. Abrial. The B Book. Cambridge University Press, 1996.
[BN13] A. Barve, M. J. Nene. Survey of Flocking Algorithms in Multi-agent Systems, IJCSI International Journal of Computer Science Issues, Vol. 10, Issue 6, No 2, November 2013 [DB05] M. Dorigo, C Blum. Ant colony optimization theory: A survey. Theoretical Computer Science, Volume 344, Issues 2–3, 17 November 2005, pages 243-278 [DD13] I. Dillig, T. Dillig. Explain: A Tool for Performing Abductive Inference, 25th International Conference on Computer Aided Verification, 684- 689, 2013.
[DMN06] L.A. Dennis, R Monroy, P Nogueira. Proof directed debugging and repair. Seventh Symposium on Trends in Functional Programming, 131-140, 2006.
[Gama] https://gama-platform.org/ [GOAL] https://goalapl.atlassian.net/wiki/spaces/GOAL/overview [HMM16] D. Hauzar, C. Marché, Y. Moy. Counterexamples from proof failures in the SPARK program verifier. Research Report RR-8854, Inria, 2016.
[Jade] https://jade.tilab.com/ [Jason] https://jason.sourceforge.net/wp/ [KBL15] S. Krings, J. Bendisposto, M. Leuschel. From failure to proof: The PROB disprover for B and Event-B. Proc. Software Engineering and Formal Methods, Lecture Notes in Computer Science, vol. 9276, pp. 199-214, 2015.
[LBS18] X. Li, A. Bundy, A. Smaill. ABC Repair System for Datalog-like Theories, 15th International Conference on Knowledge Engineering and Ontology Development, 333-340, 2018.
[Mon03] R. Monroy. Predicate synthesis for correcting faulty conjectures: The proof planning paradigm. Automated Software Engineering 10 (3), 247-269, 2003.
[MS09] B. Mermet et G.simon. Modélisation, Implantation et Vérification d’agents avec les GDT, https://mermet.users.greyc.fr/Enseignement/CoursPDF/gdts.pdf, 2009.
[MS13] B. Mermet, G. Simon. A new proof system to verify GDT agents, International Symposium on Intelligent Distributed Computing, Prague, Czech Republic. pp.181-187, Sep 2013.
[MS17] B. Mermet, G. Simon. Vers une aide au débuggage des SMA par l’exploitation d’échecs de preuve, Journées Francophones sur les Systèmes Multi-Agents (JFSMA 2017), Caen, France, Jul 2017.
[MS19] B. Mermet, G. Simon. Using proof failures to help debugging MAS. International Conference on Agents and Artificial Intelligence (ICAART 2019), Feb 2019, Prague, France. pp.523-530.
[MS22] B.Mermet et G.Simon. Comment les échecs de preuve peuvent aider à la correction de spécifications erronées de Systèmes Multi-Agents (poster). JFSMA 2022: 145 [MSSZ07] B. Mermet, G. Simon, Arnaud Saval, Bruno Zanuttini. Specifying, Verifying and Implementing a MAS : A Case study. 5th International Workshop on Programing Multi-Agent Systems (ProMAS 2007), 2007, pp.15.
[NZ08] G. Nordh, B. Zanuttini. What Makes Propositional Abduction Tractable. Artificial Intelligence, 2008, pp.1245-1284.
[ORS92] S. Owre, J.M. Rushby, N. Shankar. PVS: A prototype Verification System. 11th International Conference on Automated Deduction (CADE), Vol. 607 in Springer Verlag Lecture Notes in Artificial Intelligence; pp 748-752,1992.
[Pau94] L. C. Paulson . Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828, 1994. Equipe MAD – GREYC Université de Caen-Normandie [PHDL07] X. Pan, C. S. Han, K. Dauber, K. H. Law, « A multi-agent based framework for the simulation of human and social behaviors during emergency evacuations », AI & Society, vol. 22, n°2, p. 113-132, 2007 [PKBGJ16] G. Petiot, N. Kosmatov, B. Botella, Alain Giorgetti, J. Julliand. Your proof fails? Testing helps to find the reason, Lecture Notes in Computer Science, Springer, pp.130-150, 2016.
[Rai06] F. Raimondi. Model checking multi-agent systems. Doctoral thesis, University of London. 2006.
[Rao96] A. S. Rao, AgentSpeak(L): BDI Agents Speak Out in a Logical Computable Language, Proceedings of Seventh European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW-96).
[SNZ21] S. Scheck, A. Niveau, B. Zanuttini. Knowledge Compilation for Nondeterministic Action Languages. International Conference on Automated Planning and Scheduling, Aug 2021, Guangzhou, China.

Pour postuler, envoyez votre CV et votre lettre de motivation par e-mail à bruno.zanuttini@unicaen.fr