The Complexity of Model Checking Succinct Multiagent Systems

1 Introduction

Model checking [Clarke et al., 1999] is a promising technique used in the verification of a system implementation against its specification. Taking as inputs a model describing the system implementation and a logic formula characterizing the system specification, a model checking algorithm automatically determines whether the formula is satisfied in the model. Traditional model checking works with temporal logics [Pnueli, 1977; Clarke et al., 1986], which can express properties quantified in terms of time. In particular, branching-time temporal logics CTL and CTL � can express the safety or liveness properties on all or some of the paths from a state.

The research on model checking techniques has been extended to work with systems consisting of multiple interacting agents (or components, processes, etc). The system's behaviour depends on agents' strategies, which provide instructions for the agents to make decisions. To characterise these specifications, various logical frameworks on reasoning about strategies have been put forward. In particular, alternatingtime temporal logics (ATL and ATL � ) [Alur et al., 2002] generalise CTL and CTL � with selective quantifications over the paths, by quantifying agents' strategy ability.

In a multiagent system, an agent usually has to make decisions based on incomplete information. It is allowed to partially observe the system state and reason about the system or other agents' behaviours based on the observations. An incomplete information system is particularly suitable for the case where agents have private information which they do not want to be accessed by other agents. In this paper, we assume that agents conduct reasoning based on their current observations. With this assumption, there are two variants 1 of ATL and ATL � , namely ATLir, and ATL � ir .

1 We follow the naming conventions from [Schobbens, 2004].

Kaile Su

Jinan University, China IIIS, Gri�th University, Australia

This paper is to clarify the computational complexities of model checking these logics on multiagent systems. The complexity result of a model checking problem provides a theoretical indication on the scalability of a model checking algorithm. Most of existing works on studying model checking complexity assume an explicit representation of the system implementation by e.g., explicitly enumerating the states and the transition relation, etc. However, this is inconsistent with the ways most of the existing model checkers work.

In the paper, we work with succinct representations of multiagent systems. A succinct representation can be a concurrent representation, where agents run concurrently on their own (explicit) protocols, or a symbolic representation, where agents' protocols are described by boolean formulas. Concurrent representation has been taken as modelling languages of several model checkers, such as Verics [Kacprzak et al., 2008]. Symbolic representation serves as intermediate structure of most BDD-based or SAT-based symbolic model checkers. Modelling languages of some model checkers, for example NuSMV [Cimatti et al., 2002], MCMAS [Lomuscio et al., 2009] and MCK [Gammie and van der Meyden, 2004], can be translated into a symbolic representation in an obvious way. Therefore, it is more practical to work with succinct representations than explicit representation.

Model checking complexities for explicit representation have been well-understood for the logics that we are interested in. In particular, [Clarke et al., 1986] and [Emerson and Lei, 1987] give the complexities for CTL and CTL � , respectively. [Schobbens, 2004; Jamroga and Dix, 2008] present the complexity for ATLir and [Schobbens, 2004] shows the complexity for ATL � ir .

Model checking complexities for succinct representations are less studied. All complexity results, together with those for explicit representation, are given in Table 1. We prove the results for concurrent representation and symbolic representations. Some related works will be discussed in relevant sections.

2 Multiagent Systems

As a usual structure stated in [Fagin et al., 1995], a multiagent system consists of a set Agt of agents running simultaneously in an environment. Let Var be a set of atomic propositions. The syntax of the language ATL � is as follows:

where p 2 Var and G � Agt is a set of agents. Other operators can be obtained in the usual way, e.g., A� = :E:�, F� = TrueU�, etc. � is called state formula and ' is called path formula.

The language CTL � is a sublanguage of ATL � by removing strategy operator hhGii from the syntax of ATL � . The language ATL (CTL) is a sublanguage of ATL � (CTL � , respectively) by assuming that every path formula ' is immediately prefixed with a branching operator E or A 2 . In the following, we will present semantics of the languages on multiagent systems of several di�erent representations.

In a multiagent system, at each time, every agent is in some local state, and the environment is in some environment state. A global state is a collection of environment state and local states, one for each agent. At a global state, every agent will make an observation over the system, take a local action and update its local state, and the environment will update the environment state according to the joint local action of the agents.

2.1 Explicit Representation

Let Act = �i2AgtActi be a set of joint actions, where Acti is a finite set of actions that may be performed by agent i 2 Agt. We use O to denote the set of all possible observations. A labeled transition system M, an explicit representation, consists of a tuple (S; I; fNigi2Agt; fOigi2Agt; �!; �) where S is a set of states, I � S is a set of initial states, Ni : S ! P(Acti) n f;g assigns each state a nonempty set of legal actions that may be taken by agent i, Oi : S ! O provides agent i with an observation on each state, �!� S � Act � S is a transition relation, and � : S ! P(Var) labels each state with a set of atomic propositions. We assume that the transition relation �! is serial, i.e., for every joint action a 2 Act and every state s, there exists a state t such that (s; a; t) 2�!.

A (uniform and memoryless) strategy �i of agent i maps each state s 2 S to a nonempty set of local actions such that �i(s) � Ni(s) and for all states s; t 2 S , Oi(s) = Oi(t) implies �i(s) = �i(t). Further, a strategy �i is deterministic if �i(s) is a singleton set for all s 2 S . Given a strategy �j for some j 2 Agt, we write M�j for the system (S ; I; f� jg[fNigi, j;i2Agt ; fOigi2Agt ; �!; �) where the legal action function Nj of agent j is replaced with the strategy � j. We say that the agent j follows strategy �j in system M�j. For a set G � Agt of agents, we write �G = f�igi2G for its collective strategy and M�G for the system where every agent i 2 G

2 The variant of immediately prefixing every path formula with a strategy operator can be expressed with this syntax.

follows strategy �i. Moreover, for any system M in which a (maybe empty) set of agents follow their own strategies, we write M0 for the original system where no strategy has been applied.

A fullpath � of M is an infinite sequence of states s0s1:::, such that 9a 2 Act : (si; a; si+1) 2�! for all i � 0. We use �(m) to denote the state sm and �[m] to denote the su�x starting from sm. Moreover, we write Path(M; s) for the set of fullpaths � of M such that �(0) = s.

The semantics of ATL � in a labeled transition system M can be entailed by a relation M; s j= �, inductively defined as follows for state s 2 S and formula �.

• � M; s j= p for p 2 Var if p 2 �(s)
• � M; s j= :� if not M; s j= �
• � M; s j= �1 _ �2 if M; s j= �1 or M; s j= �2
• � M; s j= hhGii� if there exists a collective strategy �G such that M0�G; s j= �
• � M; s j= E' if there is some � 2 Path(M; s) such that M; � j= '

where

• � M; � j= � if M; �(0) j= �
• � M; � j= :' if not M; � j= '
• � M; � j= '1 _ '2 if M; � j= '1 or M; � j= '2
• � M; � j= X' if M; �[1] j= '
• � M; � j= '1U'2 if there exists m � 0 such that M; �[k] j= '1, for all 0 � k � m � 1, and M; �[m] j= '2

Note that, when dealing with formula hhGii�, the strategy �G is applied on the original system M0, instead of the current system M. Given a labeled transition system M and a formula � of some language, the model checking problem is to decide whether M; s j= � for all s 2 I.

For labeled transition systems, the complexity of model checking will be measured over the number jS j of states, the number jActj of actions, and the size j�j of formula. The size of transition relation is polynomial with respect to both jS j and jActj. The size of a formula is measured over the number of modalities it contains.

2.2 Concurrent Representation

A multiagent system can also be defined by specifying the agents and the environment individually. This approach has been adopted by the modeling languages of some model checkers, for example Verics [Kacprzak et al., 2008]. We define a representation that shares common characterisations among them and has su�cient expressiveness. Informally, in a concurrent representation of a multiagent system, every agent and the environment run an individual protocol. At each time, an agent will make an observation over the environment, and then based on the observation and its own current local state, choose a subset of local actions according to its protocol. For every joint action of the agents, the environment will update the state in light of its protocol.

The set Var of atomic propositions is partitioned into disjoint sets Varx for x 2 Agt [ feg. Let Obsi be the set of observations which agent i 2 Agt can observe from environment states. The environment Ae is a tuple (Le; Ie; fPigi2Agt; �!e ; �e), where Le is a set of environment states, Ie � Le is a set of initial states, Pi : Le ! Obsi provides agent i with an observation on each environment state, �!e� Le �Act � Le is a transition relation, and �e : Le ! P(Vare) is a labelling function. Note that jObsij � jLej. The environment has no local action, but may nondeterministically update its own state by taking into consideration the joint actions taken by the agents.

An agent Ai, for i 2 Agt, is a tuple (Li; Ii; �!i; �i), where Li is a set of local states, Ii � Li is a set of initial states, �!i� Li � Obsi � Acti � Li is a transition relation: a tuple (li; oi; ai; l 0 i ) 2�!i means that when agent i is at state li and has an observation oi on the environment state, it may take action ai and move into the state l 0 i . If there are several ai with the same li and oi, the agent i will nondeterministically choose one of them to execute. A strategy �i of agent i can then be redefined as a function mapping from Li � Obsi to P(Acti).

Without loss of generality, we let Agt = f1; :::; ng. Given a concurrent representation C = fAigi2Agt[feg, we can construct its corresponding labeled transition system M(C) = (S; I; fNigi2Agt; fOigi2Agt; �!; �) such that

1. S = Le ��i2AgtLi, I = Ie ��i2AgtIi,
2. for all states s � (le; l1; :::; ln), Oi(s) = (Pi(le); li),
3. for all states s � (le; l1; :::; ln) 2 S and all ai 2 Acti, we let ai 2 Ni(s) if and only if there exists a local state l 0 i 2 Li such that (li; Pi(le); ai; l 0 i ) 2�!i,
4. for all states s � (le; l1; :::; ln), s 0 � (l 0 e ; l 0 1 ; :::; l 0 n ) and joint actions a � (a1; :::; an), we have that (s; a; s 0 ) 2�! if and only if (le; a; l 0 e ) 2�!e and for all agents i 2 Agt, there is (li; Pi(le); ai; l 0 i ) 2�!i, and
5. �(s) = S x2Agt[feg �x(lx).

The model checking problem is, given a concurrent representation C and a formula �, to decide whether M(C) j= �. The complexity is measured over the number j S x2Agt[feg Lxj of local states, the number j S i2Agt Actij of local actions, and the size of formula �.

2.3 Symbolic Representation

To conduct model checking, most BDD-based or SAT-based model checkers transform a multiagent system described by a modeling language into a certain form of symbolic representation, which uses propositional formulas to represent system components, e.g., the set of initial states, the transition relation, etc. Here we take a usual form of symbolic representation which are expressive enough to describe multiagent systems. Also, we note that modeling languages of some model checkers, e.g., NuSMV [Cimatti et al., 2002], MCMAS [Lomuscio et al., 2009] and MCK [Gammie and van der Meyden, 2004], can be converted into such a representation linearly in an obvious way.

The general idea for a symbolic representation comes from the fact that a formula can be taken to represent a set of states or a transition relation. Every truth assignment over a set of state variables can be regarded as a state. Therefore, a formula over the set of state variables represents the set of states whose corresponding assignments satisfy the formula. Furthermore, a transition from a state to a next state by taking an action can be a truth assignment to the union set of state variables, action variables, and next-time state variables. A formula over the union set of variables can then represent a set of transitions, i.e., a transition relation.

Given a set V of atomic propositions, we let V 0 = fv 0 j v 2 Vg be the set of next-time variables of V, and write B(V) to be the set of propositional formulas over V. Local actions S i2Agt Acti can be regarded as atomic propositions. The environment Agte is a tuple (Vare; Inie; Trne), where Vare is a set of environment variables, formula Inie 2 B(Vare) represents a set of initial states, formula Trne 2 B(Vare [ Vare 0 [ S i2Agt Acti) represents a transition relation of the environment. We assume that the propositional formulas are of size polynomial with respect to the variables. This assumption also applies to the agents.

An agent Agti is a tuple (Vari; OVari; Inii; Trni), for i 2 Agt, where Vari is a set of local variables, OVari � Vare is a set of environment variables that are observable to agent i, formula Inii 2 B(Vari) represents a set of initial states, formula Trni 2 B(OVari [ Vari [ Vari 0 [ Acti) represents a transition relation for agent i. For a set V of variables and a formula f over V, we write sa(V; f ) for the set of satisfiable assignments of V on f . A strategy �i of agent i can then be redefined as a boolean formula over the variables OVari [ Vari [ Acti.

Given a symbolic representation F = fAgtigi2Agt[feg, we can construct its corresponding labeled transition system M(F) = (S; I; fNigi2Agt; fOigi2Agt; �!; �) such that

1. S = sa(Var; True), I = sa(Var; Inie ^ V i2Agt Inii),
2. for all states s 2 S and all ai 2 Acti, we let ai 2 Ni(s) if and only if Trni ^ s ^ ai , False 3 ,
3. �!= sa(Var [Var 0 [ S i2Agt Acti; Trne ^ V i2Agt Trni),
4. for all states s 2 S , Oi(s) = s � (OVari [ Vari), and
5. p 2 �(s) if and only if p 2 s.

The model checking problem is, given a symbolic representation F and a formula �, to decide whether M(F) j= �. The complexity is measured over the number jVarj of atomic propositions, the number j S i2Agt Actij of local actions, and the size j�j of formula.

3 Complexity Results for Incomplete Information Systems

Now we are ready to investigate the complexities of model checking logics in the two succinct representations of multiagent systems.

3.1 Concurrent Representation

Our concurrent representation of a multiagent system is different with the concurrent programs in [Kupferman et al., 2000]. The concurrent representation is based on the idea of synchronous languages (e.g, Esterel and Lustre) which have been widely used in modelling reactive systems. On the other hand, concurrent programs base the idea on process algebraic languages, which have been extensively studied for modelling asynchronous processes.

3 A state or an observation can be represented either as a set of literals (variables or their negations), or the conjunction of them.

A concurrent program can be seen as a complete information multiagent system where there exists no environment and agents synchronise their behaviours by taking the same action. Each agent i has a set of legal action Acti which may be overlapping, and the product system has actions S i2Agt Acti. A tuple (s; a; t) is a transition between states s � (l1; :::; ln) and t � (l 0 1 ; :::; l 0 n ), if for all i 2 Agt, 1) a 2 Acti implies (li; a; l 0 i ) 2�!i, and 2) a < Acti implies li = l 0 i . Due to different constructions, we can not directly derive complexity results of concurrent representation from those of concurrent programs.

[Jamroga and Agotnes, 2007] investigates modular interpreted systems (MIS), in which agents take actions by considering the influence emitted by other agents. For ATLIr and ATLir model checking, an MIS will be unfolded into di�erent explicit representations. They conjectured that although ATLIr model checking is easier than that of ATLir in explicit representation, it is harder in MIS. This is di�erent with our results which are based on multiagent systems.

Theorem 1 The complexity of model checking CTL is PSPACE-hard for the concurrent representation of multiagent systems.

Proof: We proceed by a reduction from the problem of accepting an empty input tape on linear bounded automata (LBA). A nondeterministic Turing machine (NTM) T is a tuple (Q; � ; �; q0; F) where Q is a finite set of states, � is a finite set of alphabets including a special blank symbol b, � : Q � � ! P(Q � � � f�1; 1g) is the transition relation, q0 2 Q is the initial state, and F � Q is the set of accepting states. Intuitively, a transition (q; a; q 0 ; a 0 ; d) means that when the machine is at state q and reads a from the current tape cell, it will transit to state q 0 , write a 0 to the current cell, and move its reading head to one of the neighbour cells in the direction d. The head moves left, if d = �1, and moves right, if d = 1.

We define the size of a Turing machine as the size of space needed to record its transition relation, i.e., 2� j�j 2 � jQj 2 . An LBA is an NTM which uses n tape cells for a Turing machine description of size n. It is well known that the following problem is PSPACE-complete: given an LBA, to decide whether there exists a computation that accepts empty tape.

We let Agt = f1; :::; ng such that each tape cell is controlled by an agent. For i 2 Agt, we define i � 1 = i + 1, if i < n, and = n, otherwise. Moreover, i � �1 = i � 1, if i > 1, and = 1, otherwise. Let Acti = f�g [ facta j a 2 � n fbgg for i 2 Agt. We write ai for agent i's local action in the joint action a. The environment Ae is (Le; Ie; fPigi2Agt; �!e; �e) such that

1. Le = Q � f1::ng, i.e., an environment state records the machine state q and the current reading head position,
2. Ie = f(q0; 1)g, i.e., initially, the machine is at initial state and the reading head is at the leftmost position,
3. Pi(s) = s, i.e., agents can see the environment state,
4. for all (q; a; q 0 ; a 0 ; d) 2 �, we let ((q;m); ja; (q 0 ;m � d)) 2�!e for all 1 � m � n, if jam = acta 0 and jak = � for all k , m, and
5. acc 2 �e((q; m)) for all 1 � m � n, if q 2 F.

Let Obsi = Le. Agent Ai is (Li; Ii; �!i; �i) such that

1. Li = �, i.e., the agent records the symbol on its cell,
2. Ii = fbg, i.e., the agent starts with the blank symbol,
3. the transition relation �!i includes
4. (a) (a; (q; i); acta 0 ; a 0 ) for all (q; a; q 0 ; a 0 ; d) 2 �, and
5. (b) (a; (q; k); �; a) for all q 2 Q and k , i,
6. �i(l) = ; for all local state l 2 Li.

To see how the systemC = fAigi2Agt[feg simulates the computation of the LBA, we first see that ((q0; 1); b; :::; b), the single initial state of M(C), corresponds to the initial configuration of the machine T that it is at state q0, the reading head resides at position 1, and the tape is empty. Then for any state such that le = (q;m) and lm = a, if there is a transition (q; a; q 0 ; a 0 ; d) 2 � then by the construction, agent Am will transit into state a 0 and execute the action acta 0 . Other agents Ak for k , m will execute � action and stay at the same state. The environment will respond to the joint action by transiting into state q 0 and moving the reading head to the position m � d.

Therefore, the existence of a computation to accept the empty tape (i.e., reach an accepting state) is equivalent to the model checking problem M(C) j= EF acc. �

Theorem 2 The complexity of model checking ATL � ir is in PSPACE for the concurrent representation of multiagent systems.

Proof: We present a PSPACE model checking algorithm for ATL � ir . To decide if M(C) j= �, the algorithm returns the reversed result of the following procedure:

1. guesses an initial states s0 of the model M(C) and
2. returns the reversed result of sat(C; s0; �).

The function sat(C; s; �) is computed inductively as follows.

• � sat(C; s; p) for p 2 Var if p 2 �(s).
• � sat(C; s; :�) if not sat(C; s; �)
• � sat(C; s; �1 _ �2) if sat(C; s; �1) or sat(C; s; �2)
• � sat(C; s; hhGii�) is the result of guessing a strategy �G and then verifying sat(C0[�G]; s; �), where C0[�G] is a system by updating every agent i 2 G's transition relation �!i to make it consistent with the strategy �i in the original systemC0.
• � sat(C; s; E') if psat(C; s; ').

The function psat(C; s; ') is computed via the automata theoretic approach for LTL model checking [Vardi and Wolper, 1986], whose idea is to reduce the model checking problem into the language emptiness problem of the product B¨uchi automaton M(C) � A', where A' is the B¨uchi automaton for the formula '. Note that, we use A', instead of the usual A:' in LTL model checking, because ' comes from formula E'. The sizes of the automaton A' and the system M(C) are exponential with respect to ' and C, respectively. However, we do not need to construct them (and the product automaton) explicitly. Instead, we treat the emptiness check as a Savitchstyle search [Savitch, 1970] by a nondeterministic procedure which takes polynomial size of space. We omit the details of the search algorithm because it is a simple adaptation to the standard automata theoretic approach [Vardi and Wolper, 1986].

The nondeterministic search algorithm on M(C) � A' involves the evaluations of state subformulas of ' over the states of M(C). These evaluations can be done inductively by taking the procedure sat(C; s; ).

Let nL = j S x2Agt[feg Lxj and nA = j S i2Agt Actij. To handle state formulas, the algorithm needs to remember the current state, which takes O(jAgtj�log nL) bits, the current strategy �, which takes up to P i2Agt jLij�jLej�jActij = O(jAgtj�nL 2 �nA) bits, and the current formula, which takes up to O(j�j) bits of space. To handle path formulas, the algorithm needs up to O((jAgtj � lognL + j�j) 2 ) bits of space for the Savitch-style search. Therefore, the space requirement is sp = O((jAgtj � log nL + j�j) 2 + jAgtj � nL 2 � nA).

The algorithm uses at = O(j�j) number of alternations. By Theorem 4.2 of [Chandra et al., 1980], the algorithm can be simulated by a deterministic machine using space at � sp + sp 2 , which is polynomial with respect to jAgtj, nL, j�j, and nA. Therefore, it is in PSPACE. �

The above theorems lead to the following conclusions.

Corollary 1 The complexities of model checking CTL, CTL � , ATLir , ATL � ir are all PSPACE-complete for the concurrent representation of multiagent systems.

Proof: The lower bounds are obtained by Theorem 1 and the fact that CTL is a sublanguage of all other languages. The upper bounds are obtained by Theorem 2 and the fact that all other languages are subsumed by ATL � ir . �

3.2 Symbolic Representation

Now we move on to examine the complexity on symbolic representation. As will be shown, the complexities for CTL and CTL � are the same with those on concurrent representation. However, the complexities for ATLir and ATL � ir are higher than those on concurrent representation.

Theorem 3 The complexities of model checking CTL and CTL � are PSPACE-complete for the symbolic representation of multiagent systems.

Proof: The lower bound is obtained by a reduction from concurrent representation. Let C = fAxgx2Agt[feg. We introduce two boolean variables bs and b 0 s for each state s 2 S x2Agt[feg Lx and one boolean variable bo for each observation o 2 Obsi with i 2 Agt. We define several formulas:

1. fx;s = bs ^ V t2Lxnfsg :bt, expressing that s is the current state of x 2 Agt [ feg, and f 0 x;s = b 0 s ^ V t2Lxnfsg :b 0 t , expressing that s is the next-time state of x 2 Agt [ feg,
2. gi;o = bo ^ V o 0 2Obsi;o 0 ,o :bo 0 , expressing that the current observation of agent i on the environment state is o, and
3. hi = W s2Le ( fe;s ^ gi;Pi(s)), expressing the function Pi by the relation between states and observations.

For a joint action a � (a1; :::; an), we let ka = V i2Agt ai. We construct Agte = (Vare; Inie; Trne) such that

1. Vare = fbs j s 2 Leg [ S i2Agtfbo j o 2 Obsig,
2. Inie = V i2Agt hi ^ W s2Ie fe;s, and

Intuitively, in Trne, the formula W (s;a;t)2�!e fe;s ^ ka ^ f 0 e;t encodes all possible transitions, and then the formula V i2Agt hi tells the observations of agents. It is similar for Inie. Moreover, we have Agti = (Vari; OVari; Inii; Trni) such that

From the way of constructing its explicit representation, a global transition �! will need to have the same gi;o on both Trni and Trne. It reflects the fact that agent makes an observation on the environment state, and then the observation is taken into consideration when making local transition.

The symbolic representation F = fAgtigi2Agt[feg is of size polynomial with respect to C, and the above construction can be done in polynomial time. Also, it is not hard to see that M(C) j= � if and only if M(F) j= �.

The upper bound can be obtained by reusing the algorithm in Theorem 2. We only describe the di�erences. First, the procedure for sat(C; s; hhGii�) is removed and therefore the algorithm needs only a constant number, instead of a polynomial number, of alternations. Second, during the Savitchstyle search for path formulas, the guessing of states can be done in polynomial time by guessing the value for each variable in Var. Third, the evaluation of transitions between states are done by guessing a joint action and then evaluating the satisfiability of the boolean formula Trne ^ V i2Agt Trni, which by definition is in polynomial size.

Therefore, the complexity is in PSPACE because the algorithm can be implemented by a nondeterministic machine with polynomial space. �

Theorem 4 The complexities of model checking ATLir and ATL � ir are NEXP-complete for the symbolic representation of multiagent systems.

Proof: The lower bound can be obtained by a reduction from satisfiability of dependency quantified boolean formulas (DQBF) [Peterson et al., 2001]. Let X1; :::Xn; Y1; :::Yn be tuples of boolean variables and F(X1; :::; Xn; Y1; :::; Yn) be a boolean formula over these variables. A DQBF formula can be written as

Intuitively, the formula requires that the values of variables Y1 depend only on the values of X1, the values of Y2 depend only on the values of X1 and X2, and so on. More precisely, such a formula is satisfiable if there exist tuples of boolean expressions g1(X1) (in variables X1) through gn(X1; : : : ; Xn) (in variables X1; : : : ; Xn) such that the QBF formula

is True. It has been shown that every QBF formula can be expressed as a DQBF formula, and the satisfiability problem of DQBF is NEXPTIME-complete [Peterson et al., 2001].

Given a DQBF formula, we construct a symbolic representation. Let X = X1 [ ::: [ Xn and Y = Y1 [ ::: [Yn. The system consists of a set of agents Agt = Y. Every agent decides the value of a variable from some Yk based on the values of the variables X1; : : : ; Xk, which are made observable. Agent y 2 Y has two actions, i.e., Acty = fsetTy; setFyg.

The environment represents the X and Y variables and handles the evaluation of the formula F. More specifically, we have Agte = (Vare; Inie; Trne) such that

1. Vare = X [ Y [ f f g, Inie = True,
2. Trne = V y2Y((setTy ) y 0 ) ^ (setFy ) :y 0 )) ^ ( f , F(X1; :::; Xn; Y 0 1 ; :::; Y 0 n ),

where Y 0 j = fy 0 j y 2 Yjg for 1 � j � n. That is, the environment sets the next-time value of each variable y 0 2 Y to true if the corresponding agent is performing the action setTy. The value of the formula F, assigned to the variable f , is then computed by taking the next-time values. For every k = 1 : : : n and variable y 2 Yk, we have agent Agty = (Vary; OVary; Iniy; Trny) such that

1. Vary = ;, OVary = X1 [ : : : [ Xk consists of the set of X variables on which y may depend,
2. Iniy = True, and Trny = setTy _ setFy.

Intuitively, every agent is attached with a variable, and an agent observes the variables on which the value of its variable depends and then makes decision on the value of its variable. Therefore, it is straightforward to show that the satisfiability of DQBF formula is equivalent to decide whether M(F) j= hhYiiAX f .

For the upper bound, we can reuse the algorithm in Theorem 2, with some changes to obtain a di�erent complexity. One of the significant changes exists in dealing with strategy formulas. A strategy �i may be represented by giving the truth table for the formula �(v), where the input variables are OVari [ Vari [ Acti. Each time when dealing with formula hhGii�, the algorithm nondeterministically guesses this truth table representation of �i for every i 2 G. This phase takes exponential time.

To handle path formulas ', we explicitly construct the product automaton M(F) � A', which is of exponential size with respect to both F and '. Note that, we do not explicitly construct F0[�G]. Instead, we will look up the truth table when evaluating a transition relation. The checking of the emptiness of a B¨uchi automaton can be done in polynomial time [Vardi and Wolper, 1986].

Finally, because the number of alternation is polynomial, the algorithm can be implemented with a nondeterministic machine in exponential time, i.e., in NEXPTIME. �

4 Conclusion and FutureWork

This paper presents complexity results for model checking several logics (CTL, CTL � , ATLir, ATL � ir ) on two succinct representations of multiagent systems. For concurrent representation, it is shown that all of them are PSPACE-complete. On the other hand, for symbolic representation, the complexities for branching time logics remain at PSPACE-complete, while they are NEXPTIME-complete for ATLir and ATL � ir . The reason for this increase is that the size of a strategy is exponential for symbolic representation.

The increase of computational complexity from PSPACE to NEXPTIME for symbolic representation reflects the actual situation that it is hard to find an e�cient symbolic algorithm for ATLir and ATL � ir . There are only a few attempts. In [Lomuscio and Raimondi, 2006], an algorithm is proposed to first explicitly enumerate all possible strategies for a group and then for every strategy, applying symbolic algorithm for CTL over the system updated with that strategy. This work is later extended with the capability of handling fairness constraints in [Busard et al., 2013]. Because the number of strategies can be exponential over the number of system states (and local actions if considering nondeterministic strategies), the explicit enumeration of strategies can not make the algorithms scale well in practical examples. In [Huang and van der Meyden, 2014b], a fully symbolic algorithm is proposed to tackle this situation. The general idea is to have a symbolic encoding of the strategy space, and then take advantage of the spacee�ciency of BDDs in achieving a succinct encoding of the product system. The experimental results show a significant improvement over the previous approach. A similar idea is also presented in [Cerm´ak et al., 2014] independently for a slightly di�erent logic.

For the future work, we may study the complexity for logics with richer expressiveness, e.g., [Huang and van der Meyden, 2014c; 2014a; Cerm´ak et al., 2014], or di�erent memory requirements such as perfect recall, where agents have memory to remember all past observations, or clock semantics, where agents can observe a common global clock value. For semantics with memory, we mention existing complexity results for explicit representation [van der Meyden and Shilov, 1999; Huang and van der Meyden, 2010; Guelev et al., 2011; Huang, 2015].

We are also interested in the complexity for succinct representations of complete information systems. Complete information systems can be seen as special cases of incomplete information systems, such that agents can observe the underlying system state. It is therefore reasonable to expect that the complexity may be lowered.

Acknowledgement The authors thank the support of Australian Research Council (DP120102489 and DP150101618), National Natural Science Foundation of China (No.61272415 and No.61003056), and Fundamental Research Funds for the Central Universities of China (No.21615441).