# global_model_checking_on_pushdown_multiagent_systems__9d81f2a1.pdf

Global Model Checking on Pushdown Multi-Agent Systems

Taolue Chen Department of Computer Science Middlesex University London, United Kingdom t.chen@mdx.ac.uk

Fu Song Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai, P.R.China fsong@sei.ecnu.edu.cn

Zhilin Wu State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing, P.R.China wuzl@ios.ac.cn

Pushdown multi-agent systems, modeled by pushdown game structures (PGSs), are an important paradigm of infinite-state multi-agent systems. Alternatingtime 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 μ-calculus. We propose an exponential-time global model checking algorithm which extends similar algorithms for pushdown systems and modal μ-calculus. The algorithm admits a matching lower bound, which holds even for the alternation-free fragment and ATL.

1 Introduction Over the last two decades, model checking has become an attractive approach for verifying correctness of systems. Given a model of a system, model checking exhaustively and automatically checks whether this model meets a given specification. It is widely used to verify protocol, hardware design and software (Baier and Katoen 2008). Classical model checking usually focuses on (finite) Kripke structures against properties specified in logical formulae such as Linear Temporal Logic (LTL) (Pnueli 1977) and Computational Tree Logic (CTL) (Clarke and Emerson 1981). Model checking has been extended to multi-agent systems which have been successfully employed as a modeling paradigm in a number of scenarios such as autonomous spacecraft control (Muscettola et al. 1998). A multi-agent system is a complex decentralized computing system composed of multiple interacting intelligent agents within an environment, in which the behavior of each agent is determined by its observed information of the system. To spec-

Authors are alphabetically ordered. Copyright c 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

ify the behavior of multi-agent systems, a well-known logical formalism is Alternating-Time Temporal Logics (Alur, Henzinger, and Kupferman 2002) for which a model checking algorithm for finite-state concurrent game structures is also given therein. Model checking algorithms for various other temporal logics on finite multi-agent systems have been proposed in several works, e.g. (Bourahla and Benmohamed 2005; Bulling and Jamroga 2011; Jamroga and Murano 2015). More recently, on a different dimension, model checking for ATL on a class of infinite-state multi-agent systems, i.e., pushdown multi-agent systems, was also studied in (Murano and Perelli 2015). The authors introduced pushdown game structures (PGSs) as the model, showed that the model checking problem is 2EXPSPACE-hard, and proposed a model checking algorithm in 3EXPTIME. Our work follows the direction of (Murano and Perelli 2015). We note that in the literature there is a distinction between local and global model checking. In the former setting one is given a specific state of the system and determines whether it satisfies a given property. In the latter setting one computes (a finite representation of) the set of states that satisfy a given property. The importance of global model checking has been discussed in (Piterman and Vardi 2004). In a nutshell, it is crucial when repeated checks are required, or where the model checking is only a component of the verification process. As a matter of fact, for many years global model checking algorithms were the standard. Moreover, obviously one can reduce local model checking to the global counterpart, but not vice versa when an infinite state space is concerned, as in the current setting. The algorithm of (Murano and Perelli 2015), which is based on (a variant of) tree automata, is local. (Technically the algorithm works on the product of PGSs and tree automata in a top-down fashion, and it is open whether this can be done in a bottom-up way, as mentioned by the authors.) In contrast, we investigate the global model checking problem for alternating-time temporal logics on PGSs. Namely we aim to compute the set of all of the configurations satisfying the formula in some alternating-time temporal logics. In this work, we consider two variants of alternating-time temporal logics: ATL and alternating-time μ-calculus. Concerning the global model checking for ATL on PGSs, as one of the main contributions, we present a re-

Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16)

duction from the problem to checking non-emptiness of alternating parity pushdown systems which can be solved using approaches given in (Hague and Ong 2009). Our global model checking approach has the same complexity upper bound as the local model checking algorithm proposed in (Murano and Perelli 2015). We also show that the model checking problem for ATL is 3EXPTIME-complete which improves the 2EXPSPACE lower bound of (Murano and Perelli 2015). One of the features of our algorithm is that it can deal with regular valuations rather than simple valuations of atomic propositions. By regular valuations one atomic proposition can denote an infinite (but regular) set of configurations. This turns out be a very handy specification approach (see examples in (Esparza, Kucera, and Schwoon 2003)). As we use alternating multi-automata as the data structure for configurations of PGSs, this comes almost for free, while it is unclear to us how the algorithm of (Murano and Perelli 2015) can support this in an immediate way. In verification, modal μ-calculus is generally considered to be the assembly language of various specifications in the sense that most temporal logics can be translated into μ-calculus to obtain a uniform model checking algorithm. In the multi-agent system setting, an alternating-time extension of μ-calculus has been considered in the original paper (Alur, Henzinger, and Kupferman 2002) already. As another contribution, we study model checking algorithms for alternating-time μ-calculus (AMC) over PGSs. We extend the saturation method of (Hague and Ong 2011) for modal μ-calculus over pushdown systems to the multi-agent system setting, obtaining an EXPTIME-time algorithm. Thanks to the alternating multi-automata as the data structure again, we can cope with the selective path quantifier of the alternatingtime logic directly while keeping constructions for other μcalculus operators untouched. The algorithm inherits the advantages of its counterpart in (Hague and Ong 2011), i.e., simple, amenable to implementation (in practice it is the implementation technique for pushdown model checkers), and efficient. For the lower bound, we show that the global model checking problem for alternation-free AMC on PGSs is already EXPTIME-hard. In fact, we prove that a simple formula A Fq (which is equivalent to μZ. A XZ q) is sufficient to obtain the EXPTIME hardness. From this, we also deduce that model checking of ATL (the alternatingtime counterpart of CTL) on PGSs is EXPTIME-complete. To the best of our knowledge, this result is also new. We remark that it is known that AMC is more expressive than ATL (Alur, Henzinger, and Kupferman 2002). However, this does not contradict the complexity bounds we obtained here, as translating an ATL formula into an equivalent AMC formula involves a doubly exponential blow-up in the size of the formula (de Alfaro, Henzinger, and Majumdar 2001; Alur, Henzinger, and Kupferman 2002), and model checking AMC over PGSs is exponential with respect to sizes of formulae.

2 Preliminaries We fix the following notations. Let AP be a finite set of atomic propositions, Ag be a finite set of agents, Ac be a finite set of actions that can be made by agents, Dc = Ac Ag

be the set of decisions of the agents in Ag. For each agent a Ag and decision d Dc, let d(a) denote the action made by the agent a in d. Given a set X, an X-labeled tree is a pair (Tr, r), where Tr is a prefix closed subset of N , and r : Tr X is a labeling function that assigns to each node an element from X. The root of a tree is ϵ, and for each node t Tr, if there is i N s.t. ti Tr, then ti is called a child of t, otherwise, t is called a leaf. A path π of (Tr, r) is a least subset of Tr such that ϵ π, and for every t π, either t is a leaf in (Tr, r) or there is exactly one i N s.t. ti π. Given a path π, let r(π) = x0x1... denote the sequence of labeled elements of the path π (in the order of the lengths |t| of the nodes t π).

Pushdown Game Structures

Definition 1. (Murano and Perelli 2015) A Pushdown Game Structure (PGS) is a tuple P = (P, Γ, Δ, λ), where P is a finite set of control states, Γ is a finite stack alphabet, Δ : P Γ Dc P Γ is a transition function, λ : P Γ 2AP is a labeling function that assigns to each p, ω P Γ a set of atomic propositions. W.l.o.g., we assume that Γ is a special bottom stack symbol never popped up from the stack.

A configuration of the PGS P is a pair p, ω , where p P is the control state, ω Γ is the stack content. Let CP denote the set P Γ of all the configurations of the PGS P. For every (p, γ, d) P Γ Dc such that Δ( p, γ , d) =

(p , ω), we sometimes write p, γ d P p , ω instead. The transition relation = P: CP Dc CP of the PGS P is defined as follows: for every ω Γ , if

p, γ d P p , ω , then p, γω d = P p , ωω . Given a pair p, γ P Γ and a function f : A Ac such that A Ag, let succf(p, γ) denote the set of tuples

{ p , ω | p, γ d P p , ω Δ and a A : d(a) = f(a)}, and succf(p, γω ) denote the set of configurations { p , ωω | p , ω succf(p, γ)} for every ω Γ which is the set of all the possible successors of p, γω on the actions f(a) for a A (agents Ag \ A can make any action). A track in a PGS P is a finite sequence π of configurations c0...cn such that for every i : 0 i < n, ci d = P ci+1. A path in a PGS P is an infinite sequence π of configurations c0c1... such that for every i 0, ci d = P ci+1. Given a track π = c0...cn (resp. path π = c0c1...), for every i : 0 i n (resp. i 0), let πi denote the configuration ci, π i denote the suffix sequence ci...cn (resp. cici+1...) of π, π<i denote the prefix sequence c0...ci 1 of π. Let TP C+ P denote the set of all the tracks in P,

P Cω P denote the set of all the paths in P. Given a configuration c, let TP(c) = {π TP | π0 = c} denote the set of all the tracks starting from c, P(c) = {π P | π0 = c} denote the set of all the paths starting from c. A strategy for an agent in a PGS P is a function θ : TP Ac that contains all the possible choices of actions depending upon the tracks (i.e., the history the agent saw so far). Let Θ denote the set of all the possible strategies. Given a set of

agents A Ag, an assignment over A is a function υA : A Θ that assigns to each agent a strategy. Let V denote the set of all the possible assignments. A path π is compatible with an assignment υA over the set A of agents, if for every i 0, there is a decision d Dc such that πi d = P πi+1 and d(a) = υA(a)(π<i) for all a A. Given a configuration c CP and an assignment υA over the set A of agents, let

P(c, υA) denote the set of paths starting from c that are compatible with respect to the assignment υA. Formally,

P(c, υA) = {π | π

P(c) π is compatible with υA}.

Alternating-Time Temporal Logics

In this subsection, we recall the definitions of two alternating-time temporal logics: ATL and alternating-time μ-calculus (AMC). ATL and AMC were proposed by Alur et al. in (Alur, Henzinger, and Kupferman 2002) as extensions of CTL and modal μ-calculus (Kozen 1983), where the universal and existential path quantifiers are replaced by more general quantifiers, called path selective quantifiers, each of which is parameterized by a set of agents. Alternating-time temporal logics are defined with respect to a set of atomic propositions AP and a set of agents Ag.

Definition 2. ATL formulae are defined by the following grammar:

φ ::= q | φ | φ φ | Xφ | φUφ | A φ

where q AP, A Ag.

We let φ1 φ2 = ( φ1 φ2), Fφ = true U φ,

Gφ = F φ, and [[A]]φ = A φ. Given an ATL formula φ and an atomic proposition q which is not used in φ, let φ[q/ϕ] denote the ATL obtained by replacing every occurrence of the subformula ϕ in φ by q. Let cl(φ) be the set of all subformulae of the ATL formulae φ. Formally,

if ψ cl(φ) or Xψ cl(φ) or A ψ cl(φ), then ψ cl(φ)

if ψ1Uψ2 cl(φ), then ψ1, ψ2, X(ψ1Uψ2) cl(φ).

The size |φ| of φ is defined as the size of the set cl(φ). In this paper, the semantics of ATL is defined over PGSs. Let P = (P, Γ, Δ, λ) be a PGS, ψ be an ATL formula, π be a path of P, the satisfiability relation P, π |= ψ is defined inductively as follows:

P, π |= q iff q λ(π0);

P, π |= φ iff P, π |= φ

P, π |= φ1 φ2 iff P, π |= φ1 and P, π |= φ2;

P, π |= Xφ iff P, π 1 |= φ;

P, π |= φ1Uφ2 iff there exists i 0 such that P, π i |= φ2 and for every j : 0 j < i, P, π j |= φ1;

P, π |= A φ iff there is an assignment υA V over the set A of agents such that for every π

P(π0, υA), P, π |= φ.

Given a PGS P, a configuration c CP and an ATL formula φ, c satisfies φ, denoted by P, c |= φ, iff there exists a path π

P(c) such that P, π |= φ. ATL is a sub-logic of ATL such that each occurrence of A is followed immediately by an occurrence of X, or U, or G. More precisely, ATL formulae are defined by the following grammar,

φ ::= q | φ | φ φ | A Xφ | A φUφ | A Gφ

where q AP and A Ag. On the other hand, Linear Temporal Logic (LTL) is a sublogic of ATL such that the selective path quantifiers A for A Ag are disallowed. Formally, LTL formulae are defined by the following grammar,

φ ::= q | φ | φ φ | Xφ | φUφ

where q AP.

Definition 3. A parity automaton PA is a tuple (G, Σ, θ, g0, F) where G is a finite set of states, Σ is the input alphabet, θ : G Σ 2G is a transition function, g0 G is the initial state and F : G {0, ..., k} is a rank function assigning each state g G a priority F(g), where k is some natural number called index.

A run of PA over an ω-word α0α1... from Σω is a sequence of states π = g0g1... such that g0 = g0, and for every i 0, gi+1 θ(gi, αi). Let inf(π) be the set of states visited infinitely often in π. A run π is accepting iff the smallest number of {F(g) | g inf(π)} is even. PA is called deterministic if for every (g, α) G Σ, |θ(g, α)| 1. The transition function θ in a deterministic parity automaton (DPA) is written as θ : G Σ G.

Theorem 1. (Kupferman and Vardi 2001; Piterman 2007) For every LTL formula φ, we can construct a DPA with 22O(|φ|) states and 2O(|φ|) indices such that the DPA recognizes all of the ω-words satisfying φ.

According to the definition of ATL , it is easy to see the following proposition.

Proposition 1. Given a PGS P and an ATL formula φ, for every subformula A ψ such that ψ is an LTL formula, if C CP is the set of configurations that satisfy A ψ and λ is extended as q λ(c) for every c C where q is a fresh atomic proposition, then for every configuration c CP, P, c |= φ iff P, c |= φ[q/ A ψ].

The syntax of AMC is given as follows.

Definition 4. Given a set Z of propositional variables, AMC formulae are given by the following grammar:

φ ::= q | q | Z | φ φ | φ φ | A Xφ | [[A]]Xφ | μZ.φ | νZ.φ

where q AP, Z Z, A Ag.

Fix a PGS P = (P, Γ, Δ, λ), a propositional valuation is a function Ω : Z 2CP. The semantics of AMC is given by the denotation function P Ω that maps an AMC formula to a set of configurations of P. Due to space restriction, its detailed definition is omitted here and we refer to, e.g., (Alur,

Henzinger, and Kupferman 2002). An AMC formula φ is alternation-free if for every subformula μZ.ψ (resp. νZ.ψ) of φ, there is no subformula νZ .ϕ (resp. μZ .ϕ) in ψ such that Z is a free variable of ϕ.

Definition 5 (Global Model Checking on PGSs). Given a PGS P and an ATL or AMC formula φ, the global model checking problem is to compute the set of all the configurations C CP such that for every c CP, c C iff P, c |= φ.

In this work, we consider the model checking problem with the labeling function l : AP 2CP such that for every q AP, l(q) is a regular set (technically, it is represented by an alternating multi-automaton; see below for definition). This is usually referred to as a regular valuation (Esparza, Kucera, and Schwoon 2003). l can be lifted to the function λl : P Γ 2AP : for every c CP, λl(c) = {q AP | c l(q)}.

Remark 1. (Murano and Perelli 2015) already presented an example which is modeled as a PGS, as well as some properties that can be expressed in ATL . We will not give examples here for the sake of space.

Below we introduce some machinery which will be used in our model checking algorithms. In particular, model checking ATL will be reduced to checking non-emptiness of alternating parity pushdown systems. Moreover, to finitely represent generally infinite sets of configurations of (alternating) pushdown systems, we use alternating multiautomata which are the data structure of the algorithm and play an essential role in algorithms for both ATL and AMC. Given a set X, let B+(X) be the set of positive Boolean formulae over X. For a set Y X and a formula ψ B+(X), Y satisfies ψ if assigning true to elements of Y and assigning false to elements of X \ Y make ψ true.

Alternating Pushdown Systems Definition 6. An Alternating Pushdown System (APDS) is a tuple P = (P, Γ, Δ), where P is a finite set of control states, Γ is a finite stack alphabet, and Δ : P Γ B+(P Γ ) is a transition function that assigns to each element of P Γ a positive Boolean formula over P Γ .

For every set { p1, ω1 , ..., pn, ωn } P Γ and every pair p, γ P Γ, if { p1, ω1 , ..., pn, ωn } satisfies the positive Boolean formula Δ( p, γ ), we sometimes write p, γ P { p1, ω1 , ..., pn, ωn }. If p, γ P { p1, ω1 , ..., pn, ωn }, then p, γω = P { p1, ω1ω , ..., pn, ωnω } for every ω Γ . For every pair p, γ P Γ, we suppose in this work that the Boolean formula Δ( p, γ ) is in the disjunctive normal form. The size |Δ| of Δ is defined as (p,γ) P Γ |Δ(p, γ)|, where |Δ(p, γ)| denotes the number of satisfying sets of the Boolean formula Δ(p, γ). A run ρ of the APDS P from a configuration p, ω is a CP-labeled tree (Tr, r) such that r(ϵ) = p, ω , and for every node t Tr with r(t) = p , ω and its children t0, ..., tn, it must be the case that p , ω = P { p 0, ω 0 , ..., p n, ω n } where r(ti) = p i, ω i for every i : 0 i n. W.l.o.g., we assume that all of the runs of APDSs are infinite. Given

a path π of the run ρ, let inf(π) denote the set of control states appearing infinitely often in r(π).

Alternating Multi-Automata Definition 7. (Bouajjani, Esparza, and Maler 1997) Let P = (P, Γ, Δ, F) be an APDS. An Alternating Multi Automaton (AMA) is a tuple M = (S, Γ, δ, I, Sf), where S is a finite set of states with S P, Γ is the input alphabet, δ : (S Γ) B+(S) is a transition function, I P is a finite set of initial states, Sf S is a finite set of final states. As before, for a set of states {s1, ..., sn} S, if {s1, ..., sn} satisfies δ(s, γ), we will sometimes write s γ {s1, ..., sn} instead. We define the relation δ S Γ 2S as the least relation such that the following conditions hold: s ϵ δ {s} for every s S;

s γω δ n i=1 Si if s γ {s1, ..., sn} and si ω δ Si for every i : 1 i n. The AMA M accepts a configuration p, ω if there exists S Sf such that p ω δ S and p I. Let L(M) denote the set of all the configurations accepted by M. Proposition 2. (Cachat 2002) Let M = (S, Γ, δ, I, Sf) be an AMA. Deciding whether a configuration p, ω with p S and ω Γ is accepted by M or not can be done in O(|S| |δ| |ω|) time and O(|S|) space.

3 ATL Model Checking on PGSs In this section, we propose an automata-theoretic approach to the global model checking of ATL on PGSs with regular valuations. For this purpose, we need alternating pushdown systems with parity acceptance conditions. An Alternating Parity Pushdown System (APPDS) PP = (P, Γ, Δ, F) is an APDS (P, Γ, Δ) with the parity acceptance condition given by F : P {0, ..., k}. A path π in a run ρ of the APPDS PP is accepting if and only if the smallest number in {F(p) | p inf(π)} is even. A run ρ in the APPDS PP is accepting if and only if all paths of ρ are accepting. Let L(PP) denote the set of all configurations from which the APPDS PP has an accepting run. Theorem 2. (Hague and Ong 2009) For an APPDS PP = (P, Γ, Δ, F), an AMA M with O(|P|) states and O(|P| |Γ| 2|P |) transition rules can be computed in 2O(k|P |) time and space such that L(M) = L(PP), where k is the index of PP. Note that the nonemptiness problem for the (general) alternating parity pushdown tree automata (APPTA), of which APPDS can be considered as a special case, is undecidable. However, the APPDS considered here has always the same stack content over the same direction of the trees, which is essential for the decidability results. See also (Aminof et al. 2013) for further discussions on this point. Throughout this section, let P = (P, Γ, Δ, λl) be a PGS and φ be an ATL formula. Without loss of generality, we assume that φ is a Boolean combination of formulae of the

form A ψ, where ψ is an ATL formula. Therefore, an AMA Mφ can be computed via Boolean operations on AMAs. In the following, we will demonstrate how to compute, for each subformula A ψ of φ, an AMA M A ψ in a bottom-up approach to recognize the set of configurations of P satisfying A ψ. Assume that for each proper subformula A ψ of ψ, an AMA M A ψ =

(S A ψ , Γ A ψ , δ A ψ , I A ψ , S A ψ

has been computed so that L(M A ψ ) = {c CP | P, c |= A ψ }. Moreover, since AMAs are closed under complementation, we assume that M A ψ has also been computed to recognize CP \ L(M A ψ ). Then let A ψ1 be the ATL formula obtained from A ψ as follows: For each proper subformulae A ψ of ψ, replace each occurrence of A ψ with a fresh atomic proposition q A ψ . Let AP denote the union of AP and these fresh atomic propositions. Clearly ψ1 is an LTL formula over AP . Therefore, by Proposition 1 the global model checking of A ψ over P with the regular valuation l can be reduced to the global model checking of A ψ1 over P = (P, Γ, Δ, λl ), where l is the regular valuation extended from l by assigning L(M A ψ ) to the fresh atomic propositions q A ψ . In the following, we will construct an APPDS PP A ψ1

from P and A ψ1 so that L(PP A ψ1) = {c CP | P , c |= A ψ1}. From Theorem 2, it follows that the desired AMA M A ψ can be constructed from PP A ψ1. It remains to construct PP A ψ1. To do this, we first construct a DPA PAψ1 = (G, Σ, θ, g0, F) that recognizes all the ω-words satisfying ψ1 (cf. Theorem 1), where Σ = 2AP . As the next step, intuitively the existential selection of strategies of the agents from A for model checking A ψ1 on P is represented by the disjunctions in the transition rules of PP A ψ1. On the other hand, once the strategies of the agents from A are fixed, all the paths resulting from the selection of strategies of the agents outside A, should satisfy ψ1. This universal constraint is specified by the conjunctions in the transition rules of PP A ψ1. The runs of PAψ1 on these paths are mimicked via the runs of the APPDS PP A ψ1, where the satisfaction (resp. dissatisfaction) of an atomic proposition q AP on a configuration is verified by a new thread which keeps popping the stack and simulates the run of the AMA Mq (resp. M q ) over the configuration.

Suppose the DPA PAψ1 = (G, Σ, θ, g0, F) constructed from ψ1 has index k. Moreover, for every q AP , we assume that the AMA Mq = (Sq , Γ, δq , Iq , Sq

f ) and its

complement M q = (S q , Γ, δ q , I q , S q

f ) have been computed. Although the states from P may occur in different AMAs, for our purpose, we assume that each occurrence of p P in different Mq or M q carries a unique name, for instance, it is decorated by q (resp. q ), denoted by pq

(resp. p q ).

We construct PP A ψ1 = (P , Γ, Δ , F ) as follows.

q AP Sq S q ;

F : P {0, ..., k} such that for every p P ,

F (p ) = F(g), if p = [p, g] P G, 0, otherwise;

Δ is the smallest transition function satisfying the following conditions: i. for each pair (p, γ) P Γ, g G, α AP , Δ ( [p, g], γ ) =

q AP \α p q , γ

p ,ω succf (p,γ) [p , θ(g, α)], ω ;

ii. for every s γ {s1, ..., sn}

q AP δq δ q ,

Δ ( s, γ ) =

1 i n si, ϵ ;

iii. for every s

f , Δ ( s, ) = s, .

Theorem 3. Let PP A ψ1 = (P , Γ, Δ , F ) be constructed as above. Then for every configuration p, ω CP , P , p, ω |= A ψ1 iff [p, g0], ω L(PP A ψ1). Moreover, |P | and |Δ | are doubly exponential of |ψ1|, and polynomial of the size of P and the size of Mq for q AP . In addition, the index k is exponential of |ψ1|. We deduce from Theorem 3 and Theorem 2 that the size of Mφ is triply exponential in |φ| and polynomial in the size of P. From Proposition 2, we obtain the main result of this section. Theorem 4. The model checking problem for ATL over PGSs is 3EXPTIME-complete. The lower bound follows from a reduction from twoplayer pushdown games with winning conditions specified by LTL formulae, which was shown to be 3EXPTIMEcomplete in (L oding, Madhusudan, and Serre 2004) 1. An instance G of two-player pushdown games with winning conditions specified by LTL formulae is a tuple (P, λl, P0, P1, φ), where P = (P, Γ, Δ) is a pushdown system, λ : P Γ 2AP is a function that assigns each pair p, γ a subset of AP, (P0, P1) forms a partition of P, called respectively the set of states for player 0 and player 1, and φ is an LTL formula over AP, called the winning condition for player 0. Plays of G are defined as usual. A play of G, say (p0, γ0ω0)(p1, γ1ω1) . . . , is winning for player 0 if the ωword λ( p0, γ0 )λ( p1, γ1 ) . . . satisfies φ. Winning strategies and winning regions are then defined as usual.

1We could also prove the lower bound by a more involved reduction from the membership problem of 2EXPSPACE alternating Turing machines.

In the following, we construct in polynomial time a PGS P = (P {p }, Γ, Δ , λ ) and an ATL formula φ such that for each configuration c of P, P, c |= φ iff P , c |= φ . Ag = {ag0, ag1} where ag0, ag1 correspond to player 0 and 1 of P respectively. Ac = {1, . . . , K}, where K is the maximum number k such that Δ( p, γ ) = { p1, ω1 , . . . , pk, ωk } for some p P and γ Γ. For each p, γ P0 Γ such that Δ( p, γ ) = { p1, ω1 , . . . , pk, ωk }, and each d Dc, if d(ag0) = i {1, . . . , k}, then Δ ( p, γ , d) = pi, ωi , otherwise, Δ ( p, γ , d) = p , γ . Note that here the transitions of Δ are determined by the actions of the agent ag0, no matter what actions taken by the agent ag1. For each p, γ P1 Γ such that Δ( p, γ ) = { p1, ω1 , . . . , pk, ωk }, and each d Dc, if d(ag1) = i {1, . . . , k}, then Δ ( p, γ , d) = pi, ωi , otherwise, Δ ( p, γ , d) = p , γ . Note that here the transitions of Δ are determined by the actions of the agent ag1, no matter what actions taken by the agent ag0. For each configuration p, γω of P such that p P, λ ( p, γω ) = λ( p, γ ). For each configuration p , γω of P , λ ( p , γω ) = q . The LTL formula φ = {ag0} (G q φ).

4 Alternating-time μ-Calculus In this section, we propose a global model checking algorithm for the alternating-time μ-calculus on PGSs. Given a PGS P = (P, Γ, Δ, λl ), an AMC formula φ and a propositional valuation Ω for the free variables in φ. The algorithm constructs an AMA representing the denotation of φ with respect to P, i.e., φ P Ω. The algorithm follows closely the saturation method for the modal μ-calculus over pushdown systems (Hague and Ong 2011). In particular, for the least and greatest fixpoints, we shall apply the projection function to ensure termination. Because of the similarity of syntax, most procedures, as well as the correctness proof, are (almost) identical to those in (Hague and Ong 2011). However, to handle the path selective quantifier, we need to adapt those procedures for the box and diamond modalities of the modal μ-calculus, i.e., for ψ = A Xφ and ψ = [[A]]Xφ . Suppose we have generated an AMA (S1, Γ, δ1, I1, S1 f) for φ (resp. φ ), our task now is to generate a new AMA for ψ (resp. ψ ). This can be defined as

(S1 I, Γ, δ1 δ , I, S1 f),

where I = {[p, ψ] | p P} (resp. I = {[p, ψ ] | p P}), and

δ ([p, ψ], γ) =

p ,ω succf (p,γ)

δ ([p, ψ ], γ) =

p ,ω succf (p,γ)

where p ω δ1 Qp ω. The constructions for the other operators of the AMC follow those in (Hague and Ong 2011) accordingly.

Theorem 5. The model checking problem for AMC on PGSs is EXPTIME-complete.

The hardness follows from the hardness of model checking problems for the alternation-free modal μ-calculus over pushdown systems, which is EXPTIME-complete (Walukiewicz 2001), and the obvious observations that alternation-free μ-calculus is a fragment of (alternation-free) AMC, and pushdown systems are a special class of PGSs (i.e., when |Ag| = |Ac| = 1). Indeed we even have:

Corollary 1. The model checking problem for the alternation-free AMC on PGSs is EXPTIME-complete.

Since each ATL formula can be translated into an equivalent alternation-free AMC formula in linear time, we obtain the following result.

Corollary 2. The model checking problem for ATL on PGSs is EXPTIME-complete.

The lower bound follows from the fact that the control state reachability problem of APDSs is EXPTIME-complete (Suwimonteerabuth, Schwoon, and Esparza 2006)2: We can reduce this problem to the model checking problem for a simple ATL formula A Fq on PGSs.

5 Related Work Model checking for LTL/CTL on pushdown systems were well studied in the literature and were used to verify infinitestate closed systems such as sequential programs with recursion, see (Carayol and Hague 2014) for a survey. To verify infinite-state open systems, solving two-player games or module checking on pushdown systems were studied in several works (Walukiewicz 2001; Hague and Ong 2009; L oding, Madhusudan, and Serre 2004; Serre 2003; Aminof et al. 2013; Bozzelli, Murano, and Peron 2010). However, they are incomparable to multi-agent pushdown systems, as discussed in (Murano and Perelli 2015). Model checking techniques were extended to verify finite-state multi-agent systems (Bourahla and Benmohamed 2005; Bulling and Jamroga 2011; Jamroga and Murano 2015; Cerm ak, Lomuscio, and Murano 2015). Moreover, various extensions of alternating time temporal logics have been considered, for instance, ATL with strategy contexts (Lopes, Laroussinie, and Markey 2010), ATL with strategy interactions (Wang, Schewe, and Huang 2015), strategy logic (Chatterjee, Henzinger, and Piterman 2010), ATL with probabilistic extensions (Chen et al. 2013). Again, these works are restricted to finite-state multi-agent systems. The most closely related work is (Murano and Perelli 2015) which proposes an automata-theoretic approach to model checking for ATL on PGSs which are infinite-state

2Although the result in (Suwimonteerabuth, Schwoon, and Esparza 2006) is for the backward reachability problem, it is not hard to see that the proof therein can be slightly adapted to show that the control state reachability problem is EXPTIME-complete.

multi-agent systems. The main differences between (Murano and Perelli 2015) and our work have been discussed extensively in the introduction.

6 Conclusion In this paper, we proposed a novel top-down approach for the global model checking of ATL and AMC on PGSs with regular valuations. We show that they are 3EXPTIMEcomplete and EXPTIME-complete respectively; the latter complexity bound holds for the alternation-free fragment of AMC and ATL. These algorithms are saturation-based which we believe are crucial for efficient implementation. Future work includes, apart from providing tool support and case studies, investigations of other logics (as listed partially in the related work) over PGSs, in particular their efficient model checking algorithms and complexity.

7 Acknowledgments The authors are grateful to the anonymous referees for their constructive comments. Taolue Chen is partially supported by the ARC Discovery Project (DP160101652), the Singapore Ministry of Education Ac RF Tier 2 grant (MOE2015T2-1-137), and an oversea grant from the State Key Laboratory of Novel Software Technology, Nanjing Unviersity. Fu Song is partially supported by Shanghai Pujiang Program (No. 14PJ1403200), Shanghai Chen Guang Program (No. 13CG21), and NSFC Projects (No. 61402179, 61532019, and 91418203). Zhilin Wu is partially supported by the NSFC projects (No. 61272135, 61472474, and 61572478).

Alur, R.; Henzinger, T. A.; and Kupferman, O. 2002. Alternating-time temporal logic. J. ACM 49(5):672 713. Aminof, B.; Legay, A.; Murano, A.; Serre, O.; and Vardi, M. Y. 2013. Pushdown module checking with imperfect information. Inf. Comput. 223:1 17. Baier, C., and Katoen, J. P. 2008. Principles of model checking. MIT Press. Bouajjani, A.; Esparza, J.; and Maler, O. 1997. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR 97. LNCS 1243. Bourahla, M., and Benmohamed, M. 2005. Model checking multi-agent systems. Informatica (Slovenia) 29(2):189 198. Bozzelli, L.; Murano, A.; and Peron, A. 2010. Pushdown module checking. Formal Methods in System Design 36(1):65 95. Bulling, N., and Jamroga, W. 2011. Alternating epistemic mucalculus. In IJCAI 11, 109 114. Cachat, T. 2002. Symbolic strategy synthesis for games on pushdown graphs. In ICALP 02, 704 715. Carayol, A., and Hague, M. 2014. Saturation algorithms for model-checking pushdown systems. In AFL 14, 1 24. Cerm ak, P.; Lomuscio, A.; and Murano, A. 2015. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In AAAI 15, 2038 2044. Chatterjee, K.; Henzinger, T. A.; and Piterman, N. 2010. Strategy logic. Inf. Comput. 208(6):677 693.

Chen, T.; Forejt, V.; Kwiatkowska, M. Z.; Parker, D.; and Simaitis, A. 2013. Automatic verification of competitive stochastic systems. Formal Methods in System Design 43(1):61 92. Clarke, E. M., and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceeding of Workshop on Logics of Programs, Yorktown Heights, New York, 52 71. de Alfaro, L.; Henzinger, T. A.; and Majumdar, R. 2001. From verification to control: Dynamic programs for omega-regular objectives. In LICS 01, 279 290. Esparza, J.; Kucera, A.; and Schwoon, S. 2003. Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2):355 376. Hague, M., and Ong, C. L. 2009. Winning regions of pushdown parity games: A saturation method. In CONCUR 09, 384 398. Hague, M., and Ong, C. L. 2011. A saturation method for the modal μ-calculus over pushdown systems. Inf. Comput. 209(5):799 821. Jamroga, W., and Murano, A. 2015. Module checking of strategic ability. In AAMAS 15, 227 235. Kozen, D. 1983. Results on the propositional mu-calculus. Theor. Comput. Sci. 27:333 354. Kupferman, O., and Vardi, M. Y. 2001. Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3):408 429. L oding, C.; Madhusudan, P.; and Serre, O. 2004. Visibly pushdown games. In FSTTCS 04, 408 420. Lopes, A. D. C.; Laroussinie, F.; and Markey, N. 2010. ATL with strategy contexts: Expressiveness and model checking. In FSTTCS 10, 120 132. Murano, A., and Perelli, G. 2015. Pushdown multi-agent system verification. In IJCAI 15, 1090 1097. Muscettola, N.; Nayak, P. P.; Pell, B.; and Williams, B. C. 1998. Remote agent: To boldly go where no AI system has gone before. Artif. Intell. 103(1-2):5 47. Piterman, N., and Vardi, M. Y. 2004. Global model-checking of infinite-state systems. In CAV 04, 387 400. Piterman, N. 2007. From nondeterministic B uchi and streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3). Pnueli, A. 1977. The temporal logic of programs. In FOCS 77, 46 57. Serre, O. 2003. Note on winning positions on pushdown games with [omega]-regular conditions. Inf. Process. Lett. 85(6):285 291. Suwimonteerabuth, D.; Schwoon, S.; and Esparza, J. 2006. Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In ATVA 06, 141 153. Walukiewicz, I. 2001. Pushdown processes: Games and modelchecking. Inf. Comput. 164(2):234 263. Wang, F.; Schewe, S.; and Huang, C. 2015. An extension of ATL with strategy interaction. ACM Trans. Program. Lang. Syst. 37(3):9.