Verifying and Synthesising Multi-Agent Systems Against One-Goal Strategy Logic Specifications
Abstract
Strategy Logic (SL) has recently come to the fore as a useful specification language to reason about multi-agent systems. Its one-goal fragment, or SL[1G], is of particular interest as it strictly subsumes widely used logics such as ATL*, while maintaining attractive complexity features. In this paper we put forward an automata-based methodology for verifying and synthesising multi-agent systems against specifications given in SL[1G]. We show that the algorithm is sound and optimal from a computational point of view. A key feature of the approach is that all data structures and operations on them can be performed on BDDs. We report on a BDD-based model checker implementing the algorithm and evaluate its performance on the fair process scheduler synthesis.
Cite
Text
Cermák et al. "Verifying and Synthesising Multi-Agent Systems Against One-Goal Strategy Logic Specifications." AAAI Conference on Artificial Intelligence, 2015. doi:10.1609/AAAI.V29I1.9444Markdown
[Cermák et al. "Verifying and Synthesising Multi-Agent Systems Against One-Goal Strategy Logic Specifications." AAAI Conference on Artificial Intelligence, 2015.](https://mlanthology.org/aaai/2015/cermak2015aaai-verifying/) doi:10.1609/AAAI.V29I1.9444BibTeX
@inproceedings{cermak2015aaai-verifying,
title = {{Verifying and Synthesising Multi-Agent Systems Against One-Goal Strategy Logic Specifications}},
author = {Cermák, Petr and Lomuscio, Alessio and Murano, Aniello},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2015},
pages = {2038-2044},
doi = {10.1609/AAAI.V29I1.9444},
url = {https://mlanthology.org/aaai/2015/cermak2015aaai-verifying/}
}