Global Model Checking on Pushdown Multi-Agent Systems

Authors

  • Taolue Chen Middlesex University
  • Fu Song East China Normal University
  • Zhilin Wu Chinese Academy of Sciences

DOI:

https://doi.org/10.1609/aaai.v30i1.10124

Abstract

Pushdown multi-agent systems, modeled by pushdown game structures (PGSs), are an important paradigm of infinite-state multi-agent systems. Alternating-time temporal logics are well-known specification formalisms for multi-agent systems, where the selective path quantifier is introduced to reason about strategies of agents. In this paper, we investigate model checking algorithms for variants of alternating-time temporal logics over PGSs, initiated by Murano and Perelli at IJCAI'15. We first give a triply exponential-time model checking algorithm for ATL* over PGSs. The algorithm is based on the saturation method, and is the first global model checking algorithm with a matching lower bound. Next, we study the model checking problem for the alternating-time mu-calculus. We propose an exponential-time global model checking algorithm which extends similar algorithms for pushdown systems and modal mu-calculus. The algorithm admits a matching lower bound, which holds even for the alternation-free fragment and ATL.

Downloads

Published

2016-03-03

How to Cite

Chen, T., Song, F., & Wu, Z. (2016). Global Model Checking on Pushdown Multi-Agent Systems. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.10124

Issue

Section

Technical Papers: Multiagent Systems