Verification of behaviourist multi-agent systems by means of formally guided simulations

• Main Author: Salem da silva, Paulo
• Language: ENG
• Published: Université Paris Sud - Paris XI 2011
• Subjects: [INFO:INFO_OH] Computer Science/Other; Systèmes multi-agents; Comportementalisme; Environements; Méthodes formelles; Vérification formelle; Simulation; Test basé sur des modèles
• Online Access: http://tel.archives-ouvertes.fr/tel-00656809; http://tel.archives-ouvertes.fr/docs/00/65/68/09/PDF/VD2_SALEM-DA-SILVA_PAULO_28112011.pdf

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en plusieurs agents qui interagissent et qui existent au sein d'un environnement. En particulier, ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, à savoir, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominante dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. De cette manière, non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Plus précisément, dans cette thèse, nous introduisons une architecture formelle d'agent (spécifiée avec la Notation Z) basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement (basée sur l'algèbre de processus pi-calculus) pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisés d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Dans cette thèse nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables (e.g., "chaque fois que l'agent fait X, il fera Y plus tard"). Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, donc, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator). Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche.