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{Griesmayer:2013:10.1007/978-3-642-38592-6_10,
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 = {http://dx.doi.org/10.1007/978-3-642-38592-6_10},
year = {2013}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
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 - http://dx.doi.org/10.1007/978-3-642-38592-6_10
ER -