Formal Verification of Homogeneous Multi-agentReinforcement Learning systems
Xiaoyan Wang, Lan Huang, Yujuan Zhang · Research Square · 2023
Abstract We examine the homogeneous multi-agent reinforcement learning sytems(HMARLs) in which the agents with the same roles have the equal ability of learning, reasoning and goals. We introduce a novel semantics for HMARLs called homogeneous neural concurrent game structure (HNCGS), which extends CGS with neural network and roles where the agents are implemented via feed-forward ReLU neural networks. To formally verify concrete HNCGS systems, we put forward multi-role linear dynamic strategy logic(mrLDSL), which is a variant of the SL and LDL and provides a holistic perspective to describe some properties of the system, such as sequential property, parallel property, regardless of which agent is responsible for the concrete task. We apply parameterized model checking(PMC) to solve the HNCGS verification problem against mrLDSL. The cutoff method is used to reduce the number of agents during the verification process. We present a methodology for the cutoff identification of a given HNCGS system and show the decidability of the HNCGS verification problem. We bring an algorithm for MILP-based verification process, and report the experimental results.