Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

569Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Jones:2010,
author = {Jones, AV and Lomuscio, A},
pages = {675--682},
title = {Distributed BDD-based BMC for the verification of multi-agent systems},
year = {2010}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - We present a method of distributed model checking of multi-agent systems specified by a branching-time temporal-epistemic logic. We introduce a serial algorithm, central to the distributed approach, for combining binary decision diagrams with bounded model checking. The algorithm is based on a notion of "seed states" to allow for state-space partitioning. Exploring individual partitions displays benefits arising from the verification of partial state-spaces. When verifying both an industrial model and a scalable benchmark scenario the serial bounded technique was found to be effective. Results for the distributed technique demonstrate that it out-performs the sequential approach for falsifiable formulae. Experimental data indicates that increasing the number of hosts improves verification efficiency. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
AU - Jones,AV
AU - Lomuscio,A
EP - 682
PY - 2010///
SN - 1548-8403
SP - 675
TI - Distributed BDD-based BMC for the verification of multi-agent systems
ER -