Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Kouvaros, P and Lomuscio, A},
pages = {1200--1208},
publisher = {ACM},
title = {Formal Verification of Opinion Formation in Swarms},
url = {},
year = {2016}

RIS format (EndNote, RefMan)

AB - We investigate the formal verification of consensus protocols in swarm systems composed of arbitrary many agents. We use templates to define the behaviour of the agents in an opinion dynamics setting and formulate their verification in terms of the associated parameterised model checking problem. We define a finite abstract model that we show to simulate swarms of any size, thereby precisely encoding any concrete instantiation of the swarm. We give an automatic procedure for verifying temporal-epistemic properties of consensus protocols by model checking the associated finite abstract model. We present a toolkit that can be used to generate the abstract model automatically and verify a given protocol by symbolic model checking. We use the toolkit to verify the correctness of majority rule protocols in arbitrary large swarms.
AU - Kouvaros,P
AU - Lomuscio,A
EP - 1208
PY - 2016///
SP - 1200
TI - Formal Verification of Opinion Formation in Swarms
UR -
ER -