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 = {Griesmayer, A and Lomuscio, A},
doi = {10.1007/978-3-642-38592-6_10},
pages = {130--145},
title = {Model checking distributed systems against temporal-epistemic specifications},
url = {},
year = {2013}

RIS format (EndNote, RefMan)

AB - Concurrency and message reordering are two main causes for the state-explosion in distributed systems with asynchronous communication. We study this domain by analysing ABS, an executable modelling language for object-based distributed systems and present a symbolic model checking methodology for verifying ABS programs against temporal-epistemic specifications. Specifically, we show how to map an ABS program into an ISPL program for verification with MCMAS, a model checker for multi-agent systems. We present a compiler implementing the formal map, exemplify the methodology on a mesh network use case and report experimental results. © 2013 IFIP International Federation for Information Processing.
AU - Griesmayer,A
AU - Lomuscio,A
DO - 10.1007/978-3-642-38592-6_10
EP - 145
PY - 2013///
SN - 0302-9743
SP - 130
TI - Model checking distributed systems against temporal-epistemic specifications
UR -
ER -