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 = {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 = {},
volume = {261},
year = {2018}

RIS format (EndNote, RefMan)

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 -
UR -
VL - 261
ER -