Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Kouvaros:2016,
author = {Kouvaros, P and Lomuscio, A},
pages = {1200--1208},
publisher = {ACM},
title = {Formal Verification of Opinion Formation in Swarms},
url = {http://hdl.handle.net/10044/1/34131},
year = {2016}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
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
PB - ACM
PY - 2016///
SP - 1200
TI - Formal Verification of Opinion Formation in Swarms
UR - http://hdl.handle.net/10044/1/34131
ER -