Distributed BDD-based BMC for the verification of multi-agent systems

We present a method of distributed model checking of multiagent 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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification--Model checking General Terms Verification Keywords Verification of MAS, Distribute...

• Type: Conference
• Year: 2010
• Where: ATAL
• Authors: Andrew V. Jones, Alessio Lomuscio
• Keywords: ATAL 2010, Binary Decision Diagrams, Intelligent Agents, Model Checking, Serial Bounded Technique