Contribution à la modélisation et à la vérification des systèmes multi agents

Petri nets (PN) are currently the most promising approaches to model and to verify complex systems such as Multi Agent Systems (MAS). Several solutions have been proposed to solve the problems of communication, coordination and interaction among Agents. However, to best of our knowledge, none of this solution has able to handle both aspects: structural and behavioral. The thesis focuses on the problem of formal modeling and automatic and semi-automatic verification of properties in Multi Agent Systems. More specifically, the objective is to propose a new original formal model based on Petri nets, Agents Petri nets (APN), which express consistently more accurate a Multi Agent Systems. There is growing interest in the extension of this model for modeling the migration of Agents within the mobile Agent systems. This class of model allows focusing on the formal verification of classical properties such as alertness or absence of deadlock in the context of Multi Agent Systems.Les Réseaux de Petri (RdP) sont actuellement les approches les plus prometteuses pour modéliser et vérifier les systèmes complexes tels que les Systèmes Multi Agents (SMA). De nombreuses solutions ont été proposées pour remédier aux problèmes de communication, de coordination et d’interaction entre les Agents. Cependant, il n’existe aucune en mesure de traiter, à la fois les aspects structurels et comportementaux, du moins à notre connaissance. La thèse s'intéresse à la problématique de modélisation formelle et de vérification automatique et semi-automatique de propriétés pour les Systèmes Multi Agents. Plus précisément, l'objectif consiste à proposer un nouveau modèle formel original basé sur les réseaux de Petri, les Réseaux de Petri à Agents (RdPA), qui permettent d’exprimer de manière consistante et plus précise les systèmes Multi Agents. Il s’intéresse de plus à l’extension de ce modèle aux fins de modéliser la migration des agents dans le cadre des systèmes à agents mobiles. Cette classe de modèle permet de s’intéresser à la vérification formelle de propriétés classiques comme notamment la vivacité ou l’absence d’interblocage dans le cadre des Systèmes Multi-Agent