2013/01/28 by Kouvaros, Panagiotis, Lomuscio, Alessio
#D.2.4 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA)
paper · doi:10.48550/arxiv.1301.6431
A key problem in verification of multi-agent systems by model checking concerns the fact that the state-space of the system grows exponentially with the number of agents present. This makes practical model checking unfeasible whenever the system contains more than a few agents. In this paper we put forward a technique to establish a cutoff result, thereby showing that all systems of arbitrary number of agents can be verified by model checking a single system containing a number of agents equal to the cutoff of the system. While this problem is undecidable in general, we here define a class of parameterised interpreted systems and a parameterised temporal-epistemic logic for which the result can be shown. We exemplify the theoretical results on a robotic example and present an implementation of the technique on top of mcmas, an open-source model checker for multi-agent systems.