Skip to Main content Skip to Navigation
Conference papers

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].
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 11:35:15 AM
Last modification on : Tuesday, January 18, 2022 - 2:26:06 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Alessio Lomuscio. Advances in Verification of Multi-agent Systems. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.3-4, ⟨10.1007/978-3-319-72044-9_1⟩. ⟨hal-01767478⟩



Record views


Files downloads