Combining Strategy and Roles to Formally Analyze Multi-Agent Reinforcement Learning

A novel semantics for MARL called neural concurrent game structure (NCGS) is introduced, which extends CGS with neural network and roles where the agents are implemented via feed-forward ReLU neural networks. To formally verify concrete NCGS systems and reduce the complexity, multi-role strategy logic(mrSL) was put forward. mrSL is suitable for the properties of the NCGS, regardless of which agent is responsible for the specific task. Parameterized model checking(PMC) is used to solve the NCGS verification problem against mrSL. Finally an algorithm for MILP-based verification process is introduced, and report the experimental results.