Verifying Pushdown Multi-Agent Systems Against Strategy Logics
Abstract
In this paper, we investigate model checking algorithms for variants of strategy logic over pushdown multi-agent systems, modeled by pushdown game structures (PGSs). We consider various fragments of strategy logic, i.e., SL[CG], SL[DG], SL[1G] and BSIL. We show that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, which are not harder than the problem for the subsumed logic ATL*. When BSIL is concerned, the model checking problem becomes 2EXPTIME-complete. Our algorithms are automata-theoretic and based on the saturation technique, which are amenable to implementations. PDF
Cite
Text
Chen et al. "Verifying Pushdown Multi-Agent Systems Against Strategy Logics." International Joint Conference on Artificial Intelligence, 2016.Markdown
[Chen et al. "Verifying Pushdown Multi-Agent Systems Against Strategy Logics." International Joint Conference on Artificial Intelligence, 2016.](https://mlanthology.org/ijcai/2016/chen2016ijcai-verifying/)BibTeX
@inproceedings{chen2016ijcai-verifying,
title = {{Verifying Pushdown Multi-Agent Systems Against Strategy Logics}},
author = {Chen, Taolue and Song, Fu and Wu, Zhilin},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2016},
pages = {180-186},
url = {https://mlanthology.org/ijcai/2016/chen2016ijcai-verifying/}
}