Verifying Pushdown Multi-Agent Systems against Strategy Logics

1 Introduction

A multi-agent system (MAS), in a nutshell, 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. One of the most important models for multi-agent systems is (finite-state) concurrent game structures. Very recently (at IJCAI'15), a class of infinite-state multi-agent systems, i.e., pushdown multi-agent systems, was also studied [Murano and Perelli, 2015]. These infinite MASs are modeled naturally by pushdown game structures (PGSs), which are the main focus of the current paper.

To specify the behavior of MASs, a well-known logical formalism is Alternating-Time Logic (ATL), or its extension ATL⇤ where more complex temporal properties can be expressed [Alur et al., 2002]. In contrast to traditional reactive systems, for MASs, properties expressing cooperation and enforcement of agents must be taken into account. When these properties are concerned, ATL-like logics suffer, unfortunately, from significant limitations, which has been observed in a number of recent papers (e.g., [Chatterjee et al., 2010; Mogavero et al., 2012; 2014]). In particular, in these logics one is unable to refer explicitly to specific strategies a group of agents might take, which handicap the specification of many important MAS-specific properties, typically involving game-theoretic notions of agents in a cooperative and/or adversarial setting.

⇤Equal contribution.

To remedy these shortcomings, strategy logic (SL, [Mogavero et al., 2014]) has recently been put forward. In SL, strategies are explicitly referred to by using first-order quantifiers and bindings to agents. As a result, sophisticated concepts such as Nash equilibria, which cannot be expressed in ATL⇤ , can naturally be encoded in SL. On the other hand, it is probably not surprising that the expressiveness of SL comes with a price of high computational complexity. For instance, its satisfiability problem is at least NON-ELEMENTARY hard. In light of this, several fragments of SL have been studied, for instance, Nested-Goal, Boolean-Goal, Conjunctivegoal, Disjunctive-goal, and One-Goal Strategy Logic, respectively denoted by SL[NG], SL[BG], SL[CG], SL[DG], SL[1G] [Mogavero et al., 2013; 2014; Cerm´ak et al., 2015]. Independently, Wang et al [Wang et al., 2015] put forward basic strategy-interaction logic (BSIL), which is a proper extension of ATL (but incomparable to ATL⇤ ). The main technical ingredient of BSIL is a new modal operator, viz, strategy interaction quantifier. As a specification language, BSIL bears an appropriate and natural balance between the expressiveness and the verification complexity.

For verification, we are mostly interested in model checking, a well-established formal method that allows to automatically verify correctness of systems. Model checking finite-state concurrent game structures is well-understood now. In particular, it is known that model checking SL[NG] or SL[BG] is already NON-ELEMENTARY hard [Mogavero et al., 2014; Bouyer et al., 2015], SL[CG], SL[DG] or SL[1G] is 2EXPTIME-complete, and BSIL is PSPACE-complete. In contrast, much less is known for PGSs. Only very recently, model checking ATL⇤ and alternating-time θ-calculus is shown to be 3EXPTIME-complete and EXPTIME-complete respectively [Murano and Perelli, 2015; Chen et al., 2016]. An obvious question is, how to model check PGSs against strategy logic? The current paper aims to fill in this gap.

It is known that SL[NG]/SL[BG] semantics might admit non-behavioral strategies, meaning that a choice of an agent at a given point of a play may depend on choices other agents can make in the future or in counter-factual plays [Mogavero et al., 2013; Wang et al., 2015]. This is not interesting from an MAS perspective. For this reason, we only consider the following subclasses: 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 3EXTIMEcomplete, which is not harder than the problem for the subsumed logic ATL⇤ , while the problem becomes 2EXPTIMEcomplete when considering BSIL. These results confirm the observation that SL[CG], SL[DG], SL[1G] do not increase the verification complexity in the asymptotic sense, comparing to ATL⇤ , and that BSIL indeed is "simpler" in terms of verification complexity.

Our model checking algorithms are automata-theoretic and evidently are also applicable to concurrent (finite) game structures. One of the distinguished features is that they are able to perform global model checking, i.e., to compute (a finite representation of) the set of states that satisfy a given property. The importance of global model checking has been discussed in, e.g., [Piterman and Vardi, 2004]. It is crucial when repeated checks are required, or where the model checking is only a component of the verification process. It is also very useful when studying coverage metrics [Chockler et al., 2006] for model checking, which could be used when an MAS practitioner cannot guarantee the correctness of specifications or system models. Specifically for the pushdown structures, our model checking algorithms are also saturationbased, which are amenable to implementations. Moreover, they 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. For two reasons we consider regular valuations of atomic propositions: (1) the algorithm iteratively computes, for a (sub-)formula, a possibly infinite, but regular set of configurations. This (sub-)formula will then be replaced by a fresh atomic proposition with the regular set as the valuation, (2) Regular valuations do not bring extra cost to our algorithm, but may make the specification more convenient, see e.g. [Esparza et al., 2003].

As another contribution, we also clarify the expressiveness of BSIL and SL. While it seems that BSIL is incomparable with SL[1G], we show that it is strictly less expressive than SL[CG] and SL[DG]. This was not known before to the best of our knowledge.

Related Work. LTL/CTL model checking on pushdown systems were well studied in the literature which can be used to verify infinite-state closed systems (see [Carayol and Hague, 2014] for a survey). Two-player games or module checking on pushdown systems were also extensively studied; see, e.g., [Walukiewicz, 2001; Hague and Ong, 2009; L¨oding et al., 2004; Serre, 2003; Aminof et al., 2013; Bozzelli et al., 2010] which can be used to verify infinitestate open systems. However, as discussed in [Jamroga and Murano, 2014], module checking (model checking open systems) is incomparable to model checking MAS.

Model checking techniques were extended to verify finitestate MASs against variants of temporal logics, typically based on ATL. For instance, [Bourahla and Benmohamed, 2005; Bulling and Jamroga, 2011; Jamroga and Murano, 2015]; see [Chen et al., 2016] for further references. The most closely related work is [Cerm´ak et al., 2015]. The authors provided symbolic model checking algorithms for SL[1G], but restricted to finite MASs. In contrast, we consider infinite MASs and much more expressive fragments of SL. We note that [Wang et al., 2015] also presented automatabased model checking algorithms for BSIL. However, their method was based on tree automata, which is considerably different from ours.

2 Pushdown Game Structures

We write [n] = ¶1↪ 2↪ ▷ ▷ ▷ ↪ n♦. 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 = AcAg be the set of decisions of the agents in Ag. For each agent a 2 Ag and decision d 2 Dc, let d(a) denote the action chosen by a in d.

Definition 1 (Pushdown Game Structures, [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 hp↪ !i 2 P ⇥ Γ⇤ a set of atomic propositions. W.l.o.g., we assume that ? 2 Γ is a special bottom stack symbol never popped up from the stack.

A configuration hp↪ !i of the PGS P consists of a state p 2 P , a stack content ! 2 Γ⇤ . We denote by CP the set P ⇥ Γ⇤ . For every (p↪ γ↪ d) 2 P ⇥Γ⇥Dc with ∆(hp↪ γi↪ d) = (p0 ↪ !), we usually write hp↪ γi d ,!P hp0 ↪ !i instead.

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. A path ⇡ is compatible with an assignment υA : A ! ⇥ over the set A of agents, if for every i ≥ 0, there is a decision d 2 Dc such that ⇡i d =)P ⇡i+1 and d(a) = υA(a)(⇡<i) for all a 2 A. Given a configuration c 2 CP and an assignment υA over the set A of agents, let QP (c↪ υA) = ¶⇡ ♣ ⇡ 2 QP (c) ^ ⇡ is compatible with υA♦▷

The transition relation =)P: CP ⇥Dc ⇥ CP of the PGS P is defined by the following rule: for every !0 2 Γ⇤ , hp↪ γ!0 i d =)P hp0 ↪ !!0 i if hp↪ γi d ,!P hp0 ↪ !i. The transition relation =)P represents possible concurrent moves of the players involved in the game. A track of P is a finite sequence ⇡ = c0▷▷▷cn over C ⇤P such that 8i : 0  i < n, ci d =)P ci+1. A path of P is an infinite sequence ⇡ = c0c1▷▷▷ over CP such that 8i ≥ 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 ci, ⇡≥i denote ci▷▷▷cn (resp. cici+1▷▷▷) of ⇡, ⇡<i denote the prefix sequence c0▷▷▷ci-1 of ⇡. Let TP ✓ C+ P denote the set of all tracks in P, QP ✓ C !P denote the set of all paths in P. Furthermore, given a configuration c, we denote by TP(c) (resp. QP (c)) the set ¶⇡ 2 TP ♣ ⇡0 = c♦ (resp. ¶⇡ 2 QP ♣ ⇡0 = c♦).

A valuation υ : V [ Ag ! ⇥ is a function assigning to each agent and element from V a strategy. Given a valuation υ, a configuration c of P, a play corresponding to (c↪ υ) is the unique outcome of P determined by the strategies υ(a)

of all agents a 2 Ag participating to it. Formally, a play corresponding to (c↪ υ) is a path ⇡ 2 QP (c) such that for every 8i ≥ 1, ⇡i-1 di =)P ⇡i and di(a) = υ(a)(⇡<i) for every a 2 Ag. Given an integer i ≥ 0, let (c↪ υ)i denote the pair (⇡i↪ υi) such that ⇡i is the i-th configuration of the play ⇡ corresponding to (c↪ υ), and υi is the updated valuation after the i-steps of the play ⇡, more precisely, υi is the valuation such that 8x 2 V [ Ag, υi(x) is a strategy satisfying that 8⇡0 2 TP(ci), υi(x)(⇡0 ) = υ(x)(⇡<i⇡0 ).

3 Strategy Logic

3.1 SL[CG] and SL[DG]

SL[CG] and SL[DG] are extensions of the logic LTL by introducing quantification prefixes and binding prefixes. A quantification prefix } 2 ¶hxi↪ [x] ♣ x 2 V ♦♣V ♣ over a set of strategy variables V is a ♣V ♣-length word in which each variable x 2 V is either existentially quantified hxi, or universally quantified [x]. Let ♣}♣ denote the length of }, that is, ♣V ♣, }(i) denote the ith symbol hxi or [x] in }, and }(x) denote the position of x in }. Let QPreV denote the set of all quantification prefixes over V . A partial binding prefix is a word (a1↪ x1) ▷ ▷ ▷ (an↪ xn) 2 (Ag ⇥ V )⇤ such that ai 6= aj for i 6= j. A binding prefix is a partial binding prefix of length ♣Ag♣, i.e., a1↪ ▷ ▷ ▷ ↪ an is an enumeration of all agents in Ag. An LTL formula preceded by a binding prefix is called a goal. In SL[CG], goals are restricted into conjunctive form. Dually, goals are restricted into disjunctive form in SL[DG]. Given a formula φ which is a Boolean combination of goals [i'i, let free(φ) denote the set of strategy variables appearing in the binding prefixes [0i s.

Definition 2 (SL[CG] and SL[DG]). [Mogavero et al., 2014; 2013] The syntax of SL[CG] and SL[DG] is defined as follows, with ? = ^ for SL[CG] and ? = _ for SL[DG]:

where q 2 AP, [ is a binding prefix, } 2 QPrefree( ) is a quantification prefix over free( ).

Given a valuation υ : V [ Ag ! ⇥, a configuration c of a PGS P and an SL[CG] or SL[DG] formula ', the satisfaction relation P↪ c↪ υ ♣= ' is inductively defined as follows:

• ÷ P↪ c↪ υ ♣= q iff q 2 λ(c);
• ÷ P↪ c↪ υ ♣= ≻' iff P↪ c↪ υ 6♣= ';
• ÷ P↪ c↪ υ ♣= '1 ^ '2 iff P↪ c↪ υ ♣= '1 and P↪ c↪ υ ♣= '2;
• ÷ P↪ c↪ υ ♣= hxi' iff 9✓ 2 ⇥, P↪ c↪ υ[✓◁x] ♣= ', where υ[✓◁x] is equal to υ except for υ[✓◁x](x) = ✓;
• ÷ P↪ c↪ υ ♣= [x]' iff 8✓ 2 ⇥, P↪ c↪ υ[✓◁x] ♣= ';
• ÷ P↪ c↪ υ ♣= (a↪ x)' iff P↪ c↪ υ[υ(x)◁a] ♣= ';
• ÷ P↪ c↪ υ ♣= X' iff P↪ (c↪ υ)1 ♣= ';
• ÷ P↪ c↪ υ ♣= '1U'2 iff 9i ≥ 0, P↪ (c↪ υ)i ♣= '2 and for every j : 0  j < i, P↪ (c↪ υ)j ♣= '1.

Note that, all agents are bound to some strategies in υ when interpreting X' or '1U'2. A configuration c of a PGS P satisfies a formula ', denoted by P↪ c ♣= ', iff there is a valuation υ such that P↪ c↪ υ ♣= '. Let k'kP denote the set of configurations c of P such that P↪ c ♣= '.

Proposition 1. SL[CG] is as expressive as SL[DG].

One-Goal SL (SL[1G]) is a special class of SL[CG] and SL[DG] in which quantification and binding prefixes merge into one rule, i.e., }['.

3.2 Basic Strategy-Interaction Logic

BSIL [Wang et al., 2015] is an extension of alternating-time temporal logic (ATL) [Alur et al., 2002] for specifying collaboration among agents. BSIL has three types of formulae: state formulae, tree formulae and path formulae, where state formulae and path formulae are used to express properties on states and paths of MAS respectively, while tree formulae are used to describe the interaction of strategies.

Definition 3 (BSIL). BSIL formulae are defined by the following three syntax rules:

where, q 2 AP , A ✓ Ag.

hAi is called a strategy quantifier (SQ for short) and h+Ai is called a strategy-interaction quantifier (SIQ for short). One can observe that each SIQ h+Ai is bounded by some SQ hA0 i, that is, h+Ai⌧ or h+Ai' only appears as a subformula of hA0 i⌧ 0 . Moreover, SIQs h+Ai do not cross path modal operators X, U or R, which is important and allows us to analyze the interaction of strategies locally in a configuration and then enforce the interaction along all paths from this configuration, as pointed out by Wang et al. [Wang et al., 2015]. We will use to denote h+;i . Let ♣φ♣ denote the length of φ. State formulae are called BSIL formulae. In the rest of this paper, we use φ↪ φ1↪ ▷▷▷ to denote state formulae, ⌧↪ ⌧1↪ ▷▷▷ to denote tree formulae and '↪ '1↪ ▷▷▷ to denote path formulae.

As in SL, the semantics of BSIL is defined over PGSs. Let P = (P↪ Γ↪∆↪ λ) be a PGS. Given a state formula φ and a configuration c 2 CP, the satisfiability relation P↪ c ♣= φ is defined inductively as follows:

• ÷ P↪ c ♣= q iff q 2 λ(c);
• ÷ P↪ c ♣= ≻φ iff P↪ c 6♣= φ;
• ÷ P↪ c ♣= φ1 ^ φ2 iff P↪ c ♣= φ1 and P↪ c ♣= φ2;
• ÷ P↪ c ♣= hAi⌧ iff 9υA : A!⇥, P↪ c↪ υA ♣= ⌧;

Given a tree formula ⌧, a valuation υ and a configuration c 2 CP, the satisfiability relation P↪ c↪ υ ♣= ⌧ is defined inductively as follows:

• ÷ P↪ c ♣= hAi' iff 9υA : A ! ⇥, 8⇡ 2 QP (c↪ υA), P↪ ⇡ ♣= '.
• ÷ P↪ c↪ υ ♣= ⌧1 _ ⌧2 iff P↪ c↪ υ ♣= ⌧1 or P↪ c↪ υ ♣= ⌧2;
• ÷ P↪ c↪ υ ♣= ⌧1 ^ ⌧2 iff P↪ c↪ υ ♣= ⌧1 and P↪ c↪ υ ♣= ⌧2;
• ÷ P↪ c↪ υ ♣= h+Ai⌧ iff 9υA : A!⇥, P↪ c↪ υ ⌦ υA ♣= ⌧;

• ÷ P↪ c↪ υ ♣= h+Ai' iff 9υA : A ! ⇥, 8⇡ 2 QP (c↪ υ ⌦ υA), P↪ ⇡ ♣= ',

where, υ ⌦ υA is the valuation such that for every a 2 Ag, (υ⌦υA)(a) is υA(a) if a 2 A, otherwise υ(a). The semantics of path formulae is entirely standard, hence is omitted.

It was shown that BSIL is incomparable with ATL⇤ [Wang et al., 2015], while SL[1G] subsumes ATL⇤ [Mogavero et al., 2012]. Therefore, there are some SL[1G] formulae (as well as SL[CG] and SL[DG]) that cannot be expressed in BSIL. On the other hand, it is difficult to construct an equivalent SL[1G] formula for the BSIL formula h¶1♦i((h¶+2♦iGp ^ h¶+2♦iGq) _ h¶+2♦iGq0 ). We note that, however, this formula can be translated into an SL[CG] formula hx1ihy1ihy2i((1↪ x1)(2↪ y1)Gp^(1↪ x1)(2↪ y2)Gq)_ hx1ihy3i((1↪ x1)(2↪ y3)Gq0 ), where Ag = ¶1↪ 2♦. In general, we have the following result.

Theorem 1. For each BSIL formula φ, an equivalent SL[CG] or SL[DG] formula φ0 can be constructed.

3.3 Automata for Logic Formulae

In this section, we recall some connection of logic and automata which will be used in our model checking algorithms. First, recall the syntax of LTL:

Definition 4. 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 2 G is the initial state and F : G ! ¶0↪ ▷▷▷↪ k♦ is a rank function assigning each state g 2 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 2 δ(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 2 inf(⇡)♦ is even. PA is called deterministic if for every (g↪ ↵) 2 G⇥⌃, ♣δ(g↪ ↵)♣  1. The transition function δ in a deterministic parity automaton (DPA) is written as δ : G⇥⌃!G.

Theorem 2. [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 φ.

Let BL(X↪U↪R) denote the set of all Boolean combinations (^↪ _) of the formulae in the forms Xφ, φUφ and φRφ such that φ ::= q ♣ ≻q ♣ φ ^ φ ♣ φ _ φ, q 2 AP.

Definition 5. A deterministic B¨uchi automaton (DBA) BA is a DPA (G↪ ⌃↪ δ↪ g0 ↪ F ) such that F : G ! ¶0↪ 1♦. A DBA BA is called 1-weak (1W-DBA for short) if each SCC (strongly connected component) in the transition graph of BA contains at most one state [Vardi, 1995].

For each BL(X↪U↪R) formula of the form Xφ1, φ1Uφ2 or φ1Rφ2, one can construct an equivalent 1W-DBA with at most 2 states. Furthermore, 1W-DBA is closed under intersection and union. Then, we get that:

Proposition 2. For every BL(X↪U↪ R) formula φ, we can construct a 1W-DBA with 2O(♣φ♣) states recognizing all of the !-words that satisfy φ.

3.4 The Model Checking Problem

In this work, we consider the global model checking problem. Namely, given a PGS P and a BSIL, SL[CG] or SL[DG] formula φ, we compute kφkP, the set of configurations of P satisfying φ. Note that for the PGS model, we consider regular valuations [Esparza et al., 2003], i.e., the labeling function is given as l : AP ! 2CP such that for every q 2 AP, l(q) is a regular set (technically, it is represented by an alternating multi-automaton; see below for definition). The labeling function l can be lifted to the function λl : P ⇥ Γ⇤ ! 2AP : for every c 2 CP, λl(c) = ¶q 2 AP ♣ c 2 l(q)♦.

4 Model Checking Algorithms

Our approaches rely crucially on alternating pushdown systems which we first review, as follows.

4.1 Alternating Pushdown Systems

Given a set X, let B+(X) denote the set of positive Boolean formulae over X. For a set Y ✓ X and a formula 2 B+(X), Y satisfies if assigning true to elements of Y and assigning false to elements of X ∩ Y makes true.

Definition 6 (Alternating Pushdown Systems). 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 ¶hp1↪ !1i↪ ▷▷▷↪ hpn↪ !ni♦ ✓ P ⇥ Γ⇤ and every pair hp↪ γi 2 P ⇥ Γ, if ¶hp1↪ !1i↪ ▷▷▷↪ hpn↪ !ni♦ satisfies the positive Boolean formula ∆(p↪ γ), we sometimes write hp↪ γi -!P ¶hp1↪ !1i↪ ▷▷▷↪ hpn↪ !ni♦. If hp↪ γi -!P ¶hp1↪ !1i↪ ▷▷▷↪ hpn↪ !ni♦, then hp↪ γ!i =)P ¶hp1↪ !1!i↪ ▷▷▷↪ hpn↪ !n!i♦ for every ! 2 Γ⇤ . For every pair hp↪ γi 2 P ⇥ Γ, we suppose in this work that the Boolean formula ∆(hp↪ γi) is in the disjunctive normal form. The size ♣∆♣ of ∆ is defined as P(p↪γ)2P⇥Γ ♣∆(hp↪ γi)♣, where ♣∆(hp↪ γi)♣ denotes the number of satisfying sets of the Boolean formula ∆(hp↪ γi).

A run ⇢ of the APDS P from a configuration hp↪ !i is a CP-labeled tree (Tr↪ r) such that r(✏) = hp↪ !i, and for every node t 2 Tr with r(t) = hp0 ↪ !0 i and its children t0↪ ▷▷▷↪ tn, it must be the case that hp0 ↪ !0 i =)P ¶hp00 ↪ !00 i↪ ▷▷▷↪ hp0n ↪ !0n i♦ where r(ti) = hp0i ↪ !0i 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 r(⇡) be the sequence of configurations along ⇡, and inf(⇡) denote the set of control states appearing infinitely often in r(⇡).

For an APDS, we consider the following acceptance conditions:

• ÷ parity: an APDS (P↪ Γ↪∆) is equipped with a function F : P ! ¶0↪ ▷▷▷↪ k♦, where k is referred to as the index.
• ÷ conjunctive parity: in this case, an APDS (P↪ Γ↪∆) is equipped with F = ¶Fi♦i2[m] such that for every i 2 [m], Fi : P ! ¶0↪ ▷▷▷↪ ki♦. We call k = max¶ki ♣ i 2 [m]♦ as the index of the APDS with the conjunctive parity acceptance condition.

Given a run ⇢, a path ⇡ in the run ⇢ is accepting if

• ÷ parity: the smallest number in ¶F(p) ♣ p 2 inf(⇡)♦ is even.
• ÷ conjunctive parity: 8i 2 [m] such that the smallest number in ¶Fi(p) ♣ p 2 inf(⇡)♦ is even.

A run ⇢ in the APDS P is accepting iff all the paths in ⇢ are accepting. Let L(P) denote the set of all configurations from which P has an accepting run. In the sequel, we usually write APDS-P, and APDS-CP for APDS with parity and conjunctive parity acceptance conditions respectively.

We observe that APDS-CP with F = ¶Fi♦i2[m] can be seen as APDS with O(mk) Streett pairs [Chatterjee et al., 2007], which can be transformed into APDS-P by using index appearance records (e.g. [Gurevich and Harrington, 1982; Schwoon, 2001]).

Theorem 3. [Gurevich and Harrington, 1982; Schwoon, 2001] Given an APDS-CP P = (P↪ Γ↪∆↪ F) with F = ¶Fi♦i2[m], we can construct an APDS-P P 0 = (P 0 ↪ Γ↪∆0 ↪ F 0 ) in O(♣∆♣(mk)!) time such that L(P) = L(P 0 ). Moreover, ♣P 0 ♣ = O(♣P♣(mk)!), ♣∆0 ♣ = O(♣∆♣(mk)!) and the index k0 of P 0 is O(mk).

Alternating Multi-Automata

Definition 7 (AlternatingMulti-Automata). [Bouajjani et al., 1997] Let P = (P↪ Γ↪ ∆) be an APDS. An Alternating MultiAutomaton (AMA) is a tuple M = (S↪ Γ↪ δ↪ I↪ Sf ), where S is a finite set of states with S ◆ P, Γ is an 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 2 S;

The AMAMaccepts a configuration hp↪ !i if there exists S0 ✓ Sf such that p ! -!δ S0 and p 2 I. Let L(M) denote the set of all the configurations accepted by M. A set of configurations C ✓ CP is called regular if there exists an AMA M such that L(M) = C.

• ÷ s γ! -!δ Si2[n] Si if s γ -! ¶si♦i2[n] and si ! -!δ Si for every i 2 [n].

Proposition 3. [Cachat, 2002] Let M= (S↪ Γ↪ δ↪ I↪ Sf) be an AMA. Deciding whether a configuration hp↪ !i with p 2 S and ! 2 Γ⇤ is accepted by M or not can be done in O(♣S♣ · ♣δ♣ · ♣!♣) time and O(♣S♣) space.

4.2 SL[CG] and SL[DG] Model Checking

In this section, we consider the problem of model checking SL[CG] and SL[DG]. Thanks to Proposition 1, it is sufficient to consider SL[CG]. Given a PGS P = (P↪ Γ↪∆↪ λ) and an SL[CG] formula φ, we first deal with the case that φ is a principal sentence = }(Vi2[n] [iφi) such that for every i 2 [n], φi is an LTL formula, [i binds all of the agents to some strategy variables, and } quantifies all of the strategy variables in [i [Cerm´ak et al., 2015].

To compute k kP, we proceed as follows. First, we construct a DPA PAi = (Gi↪⌃i↪ δi↪ g0 i ↪ Fi) with index ki that accepts all the !-words satisfying φi, for every i 2 [n]. Furthermore, for every q 2 AP, we assume that AMA Mq = (Sq ↪ Γ↪ δq ↪ I q ↪ 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 2 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 ).

Next, we construct an APDS-CP for the SL[CG] principal sentence .

For χ 2 Ac♣}♣ and d 2 Dc, d is said to be compatible with χ under [i, if for every a 2 Ag, χ(}([i(a))) = d(a), where }([i(a)) is the position of the variable [i(a) in }. A state mapping f is a partial function from [n] to Si2[n] Gi such that for every i 2 [n], if f(i) is defined, then f(i) 2 Gi. Let F be the set of all state mapping functions with f0 2 F such that for every i 2 [n], f0(i) = g0 i .

We define APDS-CP P = (P 0 ↪ Γ↪∆0 ↪ F 0 ), where

• ÷ F 0 = ¶F 0 i ♦i2[n], F 0 i : P 0 ! ¶0↪ ▷▷▷↪ k♦ is the parity objective such that the following conditions hold:
• ÷ ∆0 is the smallest transition function satisfying the following constraints: for each [p↪ χ↪ f] 2 P 0 , γ 2 Γ, and ↵ ✓ AP ,

1. ∆0 ([p↪ χ↪ f]↪ γ) = V a2Ach[p↪ χa↪ f]↪ γi, if ♣χ♣ < ♣}♣ and }(♣χ♣ + 1) = [x] for some x 2 V ;

if ♣χ♣ = ♣}♣, ∆(hp↪ γi↪ d) = hp0 ↪ !i, furthermore, for every i 2 [n], f 0 (i) = δi(f(i)↪ ↵) if f(i) is defined and d is compatible with χ under [i, and f 0 (i) is undefined otherwise;

Theorem 4. For every configuration hp↪ !i 2 CP, hp↪ !i 2 k kP iff h[p↪ ✏↪ f0]↪ !i 2 L(P ). The size of P is doublyexponential of and polynomial of P and AMAsMq , where = }(Vi2[n] [iφi).

Theorem 5. [Hague and Ong, 2009] For an APDS-P P = (P↪ Γ↪ ∆↪ F ), an AMA M with O(♣P ♣) states and O(♣P ♣ · ♣Γ♣ · 2♣P♣ ) transition rules can be computed in 2O(k♣P♣) time such that L(M) = L(P), where k is the index of P.

Applying Theorem 3 and Theorem 5, we get that:

Corollary 1. For an APDS-CP P = (P↪ Γ↪∆↪ ¶Fi♦i2[m]) with index k, an AMA M with O(♣P♣(mk)!) states and O((mk)!♣P ♣ · ♣Γ♣ · 2♣P ♣(mk)! ) transition rules can be computed in 2O(♣P♣(mk)!) time such that L(M) = L(P).

For each principal sentence , we can construct an AMA M in triply-exponential time of and exponential time of P and the AMAsMq such that L(M ) = k kP. Moreover, the number of states ofM is doubly-exponential of the size of the principal sentence and polynomial of the size of the PGS and that of the AMAsMq .

The lower bound follows from the fact that SL[1G] subsumes ATL⇤ [Laroussinie et al., 2008; Cerm´ak et al., 2015] and the model checking problem for ATL⇤ on PGSs is 3EXPTIME-complete [Chen et al., 2016].

For any general SL[CG] formula φ, a formula φ0 can be constructed by replacing simultaneously all the subformulae of φ that are principal sentences by some fresh atomic propositions q and extending the labeling function λ by λ(q ) = L(M ). We then construct AMAs for the principal sentences in φ0 . Iteratively applying this procedure at most ♣φ♣ times, we can get an AMAMφ such that L(Mφ) = kφkP.

Corollary 2. The model checking problems for SL[1G], SL[CG] and SL[DG] on PGSs are 3EXPTIME-complete.

Remark 1. Our construction relies crucially on the behavioral strategies, which SL[CG]/SL[DG] enjoys according to [Mogavero et al., 2013]. The main reason is that for a fragment of SL, the strategy quantifications can be replaced by action quantifications (which is the case in our construction) only if it admits behavioral strategies. For instance, although it is tempting to think that our construction can be naturally extended to SL[BG], the obvious extension would be incomplete (due to the non-behavioral strategies). This can be illustrated by using the example in Fig. 3 from [Mogavero et al., 2013]. We will make this point explicit in the next version.

4.3 BSILModel Checking

In this section, we turn to BSIL. Let us fix a PGS P = (P↪ Γ↪∆↪ λ) and a BSIL formula . In case that is a Boolean combination of the formulae of the form hAi⌧ or hAi', an AMA can be computed via Boolean operations on AMAs. Hence, we will focus on the case that = hAi⌧ or hAi' and assume furthermore that each proper sub-state formula of ⌧ or ' has been replaced by a fresh atomic proposition with an associated AMA. Such formulae are called simple BSIL formulae.

Recall that Theorem 1 translates a BSIL formula to an equivalent SL[CG] formula. We can apply this translation to a simple BSIL formula , obtaining an SL[CG] formula 0 which is of the form Wi2[k] hXii[Yi] Vj2[li] [i↪j i↪j, where Xi↪ Yi are sets of strategy variables, each [i↪j is a binding prefix, and each i↪j is a BL(X↪U↪R) formula. Moreover, k =O(2♣ ♣ ) and li =O(♣ ♣) for every i 2 [k].

For each disjunct ⇠ = hXii[Yi] Vj2[li] [i↪j i↪j, we then apply the construction for SL[CG] to obtain an AMA capturing k⇠kP. However, we observe that, in this case, since i↪j is a BL(X↪U↪R) formula, instead of a fully-fledged LTL formula, we can use 1W-DBA instead of DPA (cf. Section 3.3) which only incurs a singly exponential blow-up. As a result, we are able to compute an AMA M such that L(M) = k⇠kP, the number of states of M is polynomial in the size of P and exponential in the size of ⇠.

It is then not difficult to obtain an AMA M0 for 0 , i.e., L(M0 ) = k 0 kP. Note that here although 0 may contain exponentially many disjuncts, the number of states of M0 is still polynomial in the size of P and exponential in the size of 0 . This result, in conjunction with Proposition 3, yields the main result of this section:

Theorem 6. The model checking problem for BSIL is 2EXPTIME-complete, and EXPTIME-complete for fixed formulae.

Since BSIL subsumes ATL, and the model checking problem for ATL on PGSs is EXPTIME-complete for fixed ATL formulae [Chen et al., 2016], we conclude that the model checking problem for BSIL is EXPTIME-hard for fixed formulae. The 2EXPTIME-hardness for non-fixed formulae is obtained by a reduction from the word problem of EXPSPACE-bounded alternating Turing machines T . We can construct, in polynomial time, a PGS P with two agents E and A simulating the existential moves of T and the universal moves of T , respectively. The plays of P have two phases. In the first phase, P guesses a computation tree of T over the input word and pushes the guessed symbols in each path of the computation tree into the stack. In the second phase, P pops up the content of the stack, and checks at the same time that the sequence of symbols stored in the stack is indeed an encoding of a valid computation path of T , with the help of some BSIL formula. (The further details will be provided in the full version of the paper.)

5 Conclusion

In this paper, we have investigated model checking algorithms for variants of strategy logic over PGSs.

We showed that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, while for BSIL is 2EXPTIME-complete. Future work includes implementation, extension to SL[AG] and games with imperfect recall or partial information.

6 Acknowledgments

Taolue Chen is partially supported by the ARC Discovery Project (DP160101652), the Singapore Ministry of Education AcRF Tier 2 grant (MOE2015-T2-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 ChenGuang 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).