A model checking tool for dynamic multi-agent systems

A multi-agent system (MAS) is a system composed of multiple interacting agents which can perform actions in a competitive environment. Among the theoretical framework which model MAS, we focus on named homogeneous and dynamic multi-agent system (HDMAS) first presented in [1]. HDMAS has two significant features: 1. all the agents in the system have the same possible actions (homogeneity) and, 2. the status of each agent may change as the state changes (dynamic). We are interested in studying strategic properties of HDMAS, which express the capabilities of agents to achieve their objectives when competing with the other agents in the system. The thesis project aims to implement a model checking tool for HDMAS. Model checking is a method for checking whether a finite-state model of a system meets agiven formal specification. This tool can be used to build HDMAS models and formulae, and to perform global model checking of HDMAS by finding fixed points. The compiled language for this tool is Scala