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{Lomuscio:2010,
author = {Lomuscio, A and Penczek, W and Qu, H},
pages = {659--666},
title = {Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems},
year = {2010}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - We investigate partial order reduction Tor model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing the experimental results obtained against well-known examples in the MAS literature. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
AU - Lomuscio,A
AU - Penczek,W
AU - Qu,H
EP - 666
PY - 2010///
SN - 1548-8403
SP - 659
TI - Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems
ER -