---
title: "Verifying Pushdown Multi-Agent Systems against Strategy Logics"
authors:
  - "Taolue Chen"
  - "Fu Song"
  - "Zhilin Wu"
doi: ""
url: "https://ijcai.org/proceedings/2016/33"
pdf: "https://ijcai.org/proceedings/2016/0033.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "180-185"
track: ""
keywords:
---

# Verifying Pushdown Multi-Agent Systems against Strategy Logics

Taolue Chen, Fu Song, Zhilin Wu

*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.