Counterexample-guided Distributed Permissive Supervisor Synthesis for Probabilistic Multi-agent Systems through Learning

Planning and decision making of multi-agent systems (MAS) under uncertainties has been a hot research area for decades as it finds a wide spectrum of applications in communication, control, robotics and so on. In recent years formal methods emerge in MAS problems due to its correct-by-design nature. Previously we considered the permissive supervisor synthesis for a single agent and this paper extends the result to consider multi-agent systems. The extension is not straightforward as the number of agents in the system grows. The state space explosion problem and local supervisor synthesis pose new challenges. We are therefore motivated to propose a novel automatic local supervisor synthesis framework based on learning and compositional model checking. With the recent advance in assume-guarantee reasoning verification for probabilistic systems, building the composed system can be avoided to alleviate the state space explosion and we propose a particular procedure to identify which subsystem is at fault when our system cannot meet the specification. Our approach is guaranteed to terminate in finite steps and to be correct.