Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



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




569Huxley BuildingSouth Kensington Campus






BibTex format

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)

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 ( 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 -