Meriem Taibi and Malika Ioualalen, University of Science and Technology Houari Boumediene, Algeria

Multi-agent systems are asynchronous and distributed computer systems. These characteristics make them also a discrete-event dynamic system. It is, therefore, important to analyze the behavior of such systems to ensure that they terminate correctly and satisfy other important properties. This paper presents a formal modeling and analysis of MAS, based on Well-formed Nets, in order to ensure the absence of any undesired or unexpected behavior. To validate our contribution, we consider the timetable problem, which is a multi-agent resource allocation problem.

Multi-agent system, Well-formed Nets, Model Checking.