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 …