A Compositional Automata-based Approach for Model Checking Multi-Agent Systems

This paper addresses the issue of model checking knowledge in concurrent systems. The work benefits from many recent results on model checking and combined logics for time and knowledge, and focus on the way knowledge relations can be captured from automata-based system specifications. We present a formal language with compositional semantics and the corresponding Model Checking algorithms to model and verify Multi-Agent Systems (MAS) at the knowledge level, and a process for obtaining the global automaton for the concurrent system and the knowledge relations for each agent from a set of local automata that represents the behavior of each agent. Our aim is to describe a model suitable for model checking knowledge in a pre-defined way, but with the advantage that the knowledge relations for this would be extracted directly from the automata-based model.