Scalable Verification of Strategy Logic Through Three-Valued Abstraction

Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga, Vadim Malvone, Aniello Murano

IJCAI 2023 pp. 46-54

doi:10.24963/IJCAI.2023/6 /ijcai/2023/belardinelli2023ijcai-scalable/

Abstract

The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results.

PDF IJCAI Semantic Scholar

Cite

Text

Belardinelli et al. "Scalable Verification of Strategy Logic Through Three-Valued Abstraction." International Joint Conference on Artificial Intelligence, 2023. doi:10.24963/IJCAI.2023/6

Markdown

[Belardinelli et al. "Scalable Verification of Strategy Logic Through Three-Valued Abstraction." International Joint Conference on Artificial Intelligence, 2023.](https://mlanthology.org/ijcai/2023/belardinelli2023ijcai-scalable/) doi:10.24963/IJCAI.2023/6

BibTeX

@inproceedings{belardinelli2023ijcai-scalable,
  title     = {{Scalable Verification of Strategy Logic Through Three-Valued Abstraction}},
  author    = {Belardinelli, Francesco and Ferrando, Angelo and Jamroga, Wojciech and Malvone, Vadim and Murano, Aniello},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2023},
  pages     = {46-54},
  doi       = {10.24963/IJCAI.2023/6},
  url       = {https://mlanthology.org/ijcai/2023/belardinelli2023ijcai-scalable/}
}