Verifying Pushdown Multi-Agent Systems against Strategy Logics

Chen, Taolue; Song, Fu; Wu, Zhilin

Verifying Pushdown Multi-Agent Systems against Strategy Logics

Download BibTeX Cite

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 180-185.

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.

Taolue Chen, Fu Song, and Zhilin Wu. 2016. Verifying Pushdown Multi-Agent Systems against Strategy Logics. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16. IJCAI, 180–185. https://ijcai.org/proceedings/2016/33

@inproceedings{ijcai2016p33,
  title     = {Verifying Pushdown Multi-Agent Systems against Strategy Logics},
  author    = {Chen, Taolue and Song, Fu and Wu, Zhilin},
  booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-16}},
  publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
  editor    = {Subbarao Kambhampati},
  pages     = {180--185},
  year      = {2016},
  month     = {7},
  url       = {https://ijcai.org/proceedings/2016/33},
}

TY  - CPAPER
TI  - Verifying Pushdown Multi-Agent Systems against Strategy Logics
AU  - Chen, Taolue
AU  - Song, Fu
AU  - Wu, Zhilin
T2  - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16
PB  - AAAI Press / International Joint Conferences on Artificial Intelligence
PY  - 2016
SP  - 180
EP  - 185
UR  - https://ijcai.org/proceedings/2016/33
ER  -