%0 Conference Proceedings
%T Advances in Verification of Multi-agent Systems
%+ Imperial College London
%A Lomuscio, Alessio
%Z Part 1: Abstracts of Invited Talks
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 23th International Workshop on Algebraic Development Techniques (WADT)
%C Gregynog, United Kingdom
%Y Phillip James
%Y Markus Roggenbach
%I Springer International Publishing
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-10644
%P 3-4
%8 2016-09-21
%D 2016
%R 10.1007/978-3-319-72044-9_1
%Z Computer Science [cs]Conference papers
%X 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].
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01767478/document
%2 https://inria.hal.science/hal-01767478/file/433330_1_En_1_Chapter.pdf
%L hal-01767478
%U https://inria.hal.science/hal-01767478
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-WADT
%~ IFIP-LNCS-10644