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

@article{Čermák:2018:10.1016/j.ic.2017.09.011,
author = {ermák, P and Lomuscio, A and Mogavero, F and Murano, A},
doi = {10.1016/j.ic.2017.09.011},
journal = {Information and Computation},
pages = {588--614},
title = {Practical verification of multi-agent systems against Slk specifications},
url = {http://dx.doi.org/10.1016/j.ic.2017.09.011},
volume = {261},
year = {2018}
}

RIS format (EndNote, RefMan)

TY  - JOUR
AB - We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSpace-complete. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce Image 1, an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol.
AU - ermák,P
AU - Lomuscio,A
AU - Mogavero,F
AU - Murano,A
DO - 10.1016/j.ic.2017.09.011
EP - 614
PY - 2018///
SN - 0890-5401
SP - 588
TI - Practical verification of multi-agent systems against Slk specifications
T2 - Information and Computation
UR - http://dx.doi.org/10.1016/j.ic.2017.09.011
UR - http://hdl.handle.net/10044/1/68162
VL - 261
ER -