Advances in verification of multi-agent systems

Abstract

I was honoured by the opportunity to share with the WADT 2016 attendees some of the recent work in our lab on verifying multi-agent systems (MAS) against agent-based specifications. MAS are distributed autonomous systems in which the components, or agents, act autonomously in order to reach private or common goals. MAS have been used as a paradigm to realise a wide number of applications ranging from autonomous systems and robotics to services, electronic assistants, and beyond. Logic-based specifications for MAS typically do not refer only to the agents’ temporal evolution, but also to their knowledge, strategic abilities, and other AI-inspired primitives. I began by reporting algorithms for symbolic model checking against epistemic and strategic specifications [1, 2]. I highlighted potential speedups of these techniques via a number of techniques including symmetry reduction [3], parallel approaches [4], and SAT-based methods [5]. I then demonstrated MCMAS [6, 7], an open-source BDD-based model checker supporting these specification languages. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicle was discussed [8, 9] as well applications to the verification of artifact-based services [10, 11]. I concluded by considering the case of MAS where the number of agents is unbounded and cannot be determined at design time. This is a typical assumption in robotic swarms and recent internet of things applications. In view of solving this, I reported our approach to the parameterised model checking problem. While this is generally undecidable, I presented results that establish sufficient conditions for determining a cut-off of a MAS [12–14], i.e., the number of agents that need to analysed for verifying a MAS composed of any number of components. I concluded by presenting applications to the verification of related notions, such as emergence [15–17].