Verifying pushdown multi-agent systems against strategy logics

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.

Copyright © 2016 International Joint Conferences on Artificial Intelligence. All rights reserved. the published paper is reproduced in the Middlesex University Research Repository with permission from International Joint Conferences on Artificial Intelligence

Published as: 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), Gerhard Brewka (Ed.). AAAI Press 180-186.