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 = {Lomuscio, AR and Cermak, P and Murano, A},
pages = {2038--2044},
publisher = {AAAI Press},
title = {Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications},
url = {},

RIS format (EndNote, RefMan)

AB - Strategy Logic (SL) has recently come to the fore as a usefulspecification language to reason about multi-agent systems.Its one-goal fragment, or SL[1G], is of particular interest asit strictly subsumes widely used logics such as ATL, whilemaintaining attractive complexity features. In this paper weput forward an automata-based methodology for verifyingand synthesising multi-agent systems against specificationsgiven in SL[1G]. We show that the algorithm is sound andoptimal from a computational point of view. A key featureof the approach is that all data structures and operations onthem can be performed on BDDs. We report on a BDD-basedmodel checker implementing the algorithm and evaluate itsperformance against a number of scalable scenarios.
AU - Lomuscio,AR
AU - Cermak,P
AU - Murano,A
EP - 2044
PB - AAAI Press
SP - 2038
TI - Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
UR -
UR -
ER -