Formal Verification of Parameterised Neural-symbolic Multi-agent Systems

Formal Verification of Parameterised Neural-symbolic Multi-agent Systems

Panagiotis Kouvaros, Elena Botoeva, Cosmo De Bonis-Campbell

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Main Track. Pages 103-110. https://doi.org/10.24963/ijcai.2024/12

We study the problem of verifying multi-agent systems composed of arbitrarily many neural-symbolic agents. We introduce a novel parameterised model, where the parameter denotes the number of agents in the system, each homogeneously constructed from an agent template equipped with a neural network-based perception unit and a traditionally programmed action selection mechanism. We define the verification and emergence identification problems for these models against a bounded fragment of CTL. We put forward an abstraction methodology that enables us to recast both problems to the problem of checking Neural Interpreted Systems with a bounded number of agents. We present an implementation and discuss experimental results obtained on a social dilemma game based on guarding.
Keywords:
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis