# symbolic_model_checking_for_oneresource_rbatl__41c3d102.pdf

Symbolic Model Checking for One-Resource RB ATL

Natasha Alechina1 and Brian Logan1 and Hoang Nga Nguyen1 and Franco Raimondi2

1 School of Computer Science, University of Nottingham, UK 2 Department of Computer Science, Middlesex University, UK 1 {nza,bsl,hnn}@cs.nott.ac.uk, 2 f.raimondi@mdx.ac.uk

RB ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The modelchecking problem for RB ATL is known to be decidable. However the only available modelchecking algorithm for RB ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB ATL, 1RB ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.

1 Introduction

Alternating Time Temporal Logic (ATL) [Alur et al., 2002] is widely used to characterise coalitional abilities in multi-agent systems. Recently, several extensions of ATL have been proposed that can express coalitional ability under resource constraints, for example [Alechina et al., 2009; Bulling and Farwer, 2010; Alechina et al., 2010; Della Monica et al., 2011; 2013; Bulling and Goranko, 2013; Alechina et al., 2014]. These logics allow reasoning about coalitional ability under resource constraints such as: given resources b, coalition A has a strategy to achieve ϕ . There are many different variants of ATL with resources. If resource production is allowed, the model-checking problem for many of these variants becomes undecidable [Bulling and Farwer, 2010; Bulling and Goranko, 2013]. For resource logics where the model-checking problem is known to be decidable, the only symbolic model-checking algorithm that has been proposed to date is that given in [Alechina et al., 2015], which describes an implementation of symbolic

Acknowledgements: This work was supported by the Engineering and Physical Sciences Research Council [grants EP/K033905/1 and EP/K033921/1]. We would also like to thank the anonymous IJCAI 15 reviewers whose comments and suggestions helped to improve the paper.

model-checking for the resource-consumption only logic RBATL. Symbolic model-checking uses Binary Decision Diagrams (BDDs) [Bryant, 1986] to represent sets of states symbolically, and over the last 20 years it has been successfully employed as a powerful optimisation technique in a range of model checkers such as MCK [Gammie and Van Der Meyden, 2004] and MCMAS [Lomuscio et al., 2009]. In this paper we provide a symbolic model-checking algorithm for a fragment of the logic RB ATL. RB ATL does have a decidable model-checking problem, however it is EXPSPACE-hard [Alechina et al., 2014]. The modelchecking algorithm proposed by Alechina et al. [2014] uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB ATL, 1RB ATL, that allows only one resource type, for example, money. This is a natural special case of resource logics, since in many situations only one resource is of interest, or multiple resources are mutually convertible. For example, in [Della Monica et al., 2013] it is assumed that all resources can be converted into money. The main contribution of this paper is a fixed point characterisation of 1RB ATL modalities. This makes it possible to provide a symbolic model-checking algorithm for 1RB ATL. We analyse the complexity of the model-checking algorithm, and also evaluate the performance of an MCMAS-based [Lomuscio et al., 2009] implementation of the algorithm on an example problem that can be scaled to large state spaces. The evaluation suggests that the symbolic implementation is scalable and performs much better than the algorithm from [Alechina et al., 2014].

The logic RB ATL was introduced in [Alechina et al., 2014] as a generalisation of RB-ATL [Alechina et al., 2010]. In contrast to RB-ATL which allows only consumption of resources, RB ATL allows agents to both produce and consume resources. In this section, we briefly recall the syntax and semantics of RB ATL. Let Agt = {a1, . . . , an} be a set of n agents, Res = {res1, . . . , resr} be a set of r resources, Π be a set of propositions and B = Nr be a set of resource bounds where N = N0 { }. We denote by 0 the smallest bound (0, . . . , 0) and the greatest bound ( , . . . , ).

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

Formulas of RB ATL are defined by the following syntax

ϕ ::= p | ϕ | ϕ ψ | Ab ϕ | Ab 2ϕ | Ab ϕ U ψ

where p Π is a proposition, A Agt, and b B is a resource bound. Here, Ab ϕ means that a coalition A can ensure that the next state satisfies ϕ under resource bound b. Ab 2ϕ means that A has a strategy to make sure that ϕ is always true, and the cost of this strategy is at most b. Similarly, Ab ϕ U ψ means that A has a strategy to enforce ψ while maintaining the truth of ϕ, and the cost of this strategy is at most b. To interpret this language, the definition of concurrent game structures [Alur et al., 2002] is extended with resource consumption and production.

Definition 1. A resource-bounded concurrent game structure (RB-CGS) is a tuple M = (Agt, Res, S, Π, π, Act, d, c, δ) where:

Agt is a non-empty set of n agents, Res is a non-empty set of r resources and S is a non-empty set of states.

Π is a finite set of propositional variables and π : Π (S) is a truth assignment that associates each proposition in Π with a subset of states where it is true.

Act is a non-empty set of actions which includes idle, and d : S Agt (Act) \ { } is a function that assigns to each s S a non-empty set of actions available to each agent a Agt. For every s S and a Agt, idle d(s, a). We denote joint actions by all agents in Agt available at s by D(s) = d(s, a1) d(s, an).

c : S Agt Act Zr is a partial function that maps a state s, an agent a and an action α d(s, a) to a vector of integers where the integer in position i indicates consumption or production of resource resi by the action (positive value for consumption and negative value for production). We stipulate that c(s, a, idle) = 0 for all s S and a Agt.

δ : (s, σ) 7 S is a function that, for every s S and joint action σ D(s), gives the state resulting from executing σ in s.

Given a RB-CGS M, we denote the set of all infinite sequences of states (computations) by Sω and the set of nonempty finite sequences of states by S+. For a computation λ = s0s1 . . . S+ Sω, we use the notation λ[i] = si and λ[i, j] = si . . . sj j i 0. Below, we use the usual point-wise notation for vector comparison and addition. In particular, (b1, . . . , br) (d1, . . . , dr) iff bi di i {1, . . . , r}, and (b1, . . . , br) + (d1, . . . , dr) = (b1 + d1, . . . , br + dr). We assume that for any b Z, b and b + and b = . Given a function f returning a vector, we denote by fi the function that returns the i-th component of the vector returned by f. Given a RB-CGS M and a state s S, a joint action by a coalition A Agt is a tuple σA = (σa)a A such that σa d(s, a). The set of all joint actions for A at state s is denoted by DA(s). Given a joint action by the grand coalition σ D(s), σA denotes the joint action executed by A: σA = (σa)a A. The set of all possible outcomes of a joint action

σA DA(s) at state s is: out(s, σA) = {s S | σ D(s) : σA = σ A s = δ(s, σ )}. The cost of a joint action σA DA(s) is defined as cost A(s, σA) = P a A c(s, a, σa). Given a RB-CGS M, a strategy for a coalition A Agt is a mapping FA : S+ Act such that, for every λs S+, FA(λs) DA(s). A computation λ Sω is consistent with a strategy FA iff, for all i 0, λ[i + 1] out(λ[i], FA(λ[0, i])). We denote by out(s, FA) the set of all consistent computations λ of FA that start from s. Given a bound b B, a computation λ out(s, FA) is b-consistent with FA iff, for every i 0,

j=0 cost A(λ[j], FA(λ[0, j])) b

Note that this definition implies that the cost of every prefix of the computation is below b. The set of all b-consistent computations of FA starting from state s is denoted by out(s, FA, b). FA is a b-strategy iff out(s, FA) = out(s, FA, b) for any state s. Given a RB-CGS M and a state s, the truth of a RB ATL formula ϕ with respect to M and s is defined inductively on the structure of ϕ as follows (the atomic case and the Boolean connectives are defined in the standard way):

M, s |= Ab ϕ iff b-strategy FA such that for all λ out(s, FA): M, λ[1] |= ϕ;

M, s |= Ab 2ϕ iff b-strategy FA such that for all λ out(s, FA) and i 0: M, λ[i] |= ϕ; and

M, s |= Ab ϕ U ψ iff b-strategy FA such that for all λ out(s, FA), i 0: M, λ[i] |= ψ and M, λ[j] |= ϕ for all j {0, . . . , i 1}.

Since the infinite resource bound version of RB ATL modalities correspond to the standard ATL modalities, we write A γ = A γ. Note that although we only consider infinite paths, the condition that the idle action with cost 0 is always available makes the model-checking problem easier (we only need to find a strategy with a finite prefix under bound b to satisfy formulas of the form Ab ϕ and Ab ϕ U ψ, and then the strategy can make the idle choice forever). This makes the logic closer to the finitary semantics in [Bulling and Farwer, 2010].

3 Hybrid Model Checking RB ATL

The model-checking problem for RB ATL is the question whether, for a given RB-CGS structure M, state s and RB ATL formula ϕ, M, s |= ϕ. An algorithm for solving the model-checking problem of RB ATL was presented in [Alechina et al., 2014], and is restated in Algorithm 1. Given a RB-CGS structure M and a formula ϕ0, the algorithm returns the set [ϕ0]M of states in M that satisfy ϕ, i.e., [ϕ0]M = {s | M, s |= ϕ0}. The algorithm makes use of the primitive operator Sub(ϕ0) which computes all sub-formulas of ϕ0 in the usual way, and, in addition, if Ab γ Sub(ϕ), its infinite resource version A γ is also added to Sub(ϕ). Sub(ϕ) is ordered in increasing order of complexity, and the infinite

Algorithm 1 Labelling ϕ0

function RB ATL-LABEL(M, ϕ0) for ϕ Sub(ϕ0) do case ϕ = p, ϕ, ϕ ψ, A ϕ, A ϕ U ψ, A 2ϕ standard, see [Alur et al., 2002] case ϕ = Ab ϕ [ϕ ]M Pre(A, [ϕ]M, b) case ϕ = Ab ϕ U ψ [ϕ ]M { s | s S UNTIL-STRATEGY(node0(s, b), Ab ϕ U ψ)} case ϕ = Ab 2ϕ [ϕ ]M { s | s S BOX-STRATEGY(node0(s, b), Ab 2ϕ)} return [ϕ0]M

resource version of each modal formula comes before the bounded version. Note that if a state s is not annotated with A γ then s cannot satisfy the bounded resource version Ab γ. The algorithm then proceeds by cases. For all formulas in Sub(ϕ) apart from Ab ϕ, Ab ϕ U ψ and Ab 2ϕ, the standard ATL model-checking algorithm [Alur et al., 2002] is used. The implementation of these cases can therefore be done symbolically. Labelling states with Ab ϕ makes use of a function Pre(A, ρ, b), which, given a coalition A, a set ρ S and a bound b, returns a set of states s in which A has a joint action σA with cost(s, σA) b such that out(s, σA) ρ. Labelling states with Ab ϕ U ψ and Ab 2ϕ is more complex, and requires two auxiliary functions: UNTIL-STRATEGY for Ab ϕ U ψ and BOXSTRATEGY for Ab 2ϕ. Essentially, these functions search the existence of a strategy for A which satisfies the corresponding formula by depth-first and-or search of M. For a detailed description of these functions, see [Alechina et al., 2014]. While the function Pre(A, ρ, b) can be implemented symbolically as shown in [Alechina et al., 2015], the last two cases call auxiliary functions that search state by state. Therefore, they can only be implemented non-symbolically, resulting in a hybrid (partially symbolic, partially non-symbolic) implementation.

4 Symbolic Model Checking 1RB ATL

1RB ATL is a fragment of RB ATL with |Res| = 1. Resource bounds in 1RB ATL are therefore in N and action costs in Z. In this section, we present a symbolic implementation for the cases of until formulas Ab ϕ U ψ and box formulas Ab 2ϕ in Algorithm 1 by providing a fixed point characterisation of these formulas. This will enable us to provide a symbolic implementation for the model-checking problem of 1RB ATL. The of question whether a similar approach would work with more than one resource type is open. In particular it is not clear how to generalise the functions used for the fixed point characterisation of until and box formulas below. It is also not clear how, given a coalition A and

a model M, to estimate the maximal possible cost of a strategy by A to satisfy an until formula (this estimate is required for the model-checking algorithm). Intuitively, if there is a cycle where resource r1 is produced and resource r2 is consumed, and a cycle where r1 is consumed and r2 is produced, it is not obvious what are the maximal amounts of r1 and r2 that may be needed to satisfy an until formula. This is a hard problem related to the upper bound on reachability in Petri nets (which is also an open problem, [Leroux, 2013]). Below, we use the usual point-wise notation for comparison, intersection and union of vectors of sets. In particular, for some k 1, (b1, . . . , bk) (d1, . . . , dk) iff bi di i {1, . . . , k}, (b1, . . . , br) (d1, . . . , dr) = (b1 d1, . . . , br dr) and (b1, . . . , br) (d1, . . . , dr) = (b1 d1, . . . , br dr). We drop the subscript M in [ϕ]M when this does not lead to ambiguity.

4.1 Until Formulas In this section, we show that [ Ab ϕ U ψ]M can be computed from the least fixed point of a function UA,ϕ,ψ which does not depend on b (only on costs of actions in M). For each agent i Agt, we denote by minci = min{c(s, i, a) | a Acti, s S} the minimal cost of any action by an agent i. Obviously, minci 0 due to the presence of idle, and the fact that there is no action for i that costs less that minci. Similarly, we denote by minc A = P i A minci the minimal cost of any joint action by the non-empty coalition A. Again, minc A 0 and there is no joint action for A that costs less than minc A. We extend the definition of [ Ab ] : (S) (S) in [Alechina et al., 2010] with b Z { } as [ Ab ](X) = {s S | σ DA(s) : cost(σ) b out(s, σ) X}. Obviously, [ Ab ](X) = for any b < minc A and X S.

Lemma 1. [ Ab ] is monotone.

Proof. Assume that X Y . Then:

s [ Ab ](X) σ DA(s) : cost(σ) b out(s, σ) X σ DA(s) : cost(σ) b out(s, σ) X Y

s [ Ab ](Y )

Therefore, [ Ab ](X) [ Ab ](Y ).

Next we define a predecessor to the function UA,ϕ,ψ that does depend on the bound b:

UAb,ϕ,ψ((X0, . . . , Xb minc A)) = [ψ] [ϕ]

minc A b1 b [ Ab1 ](Xb b1))

For convenience, we drop the subscripts ϕ,ψ in the remainder of this section. Note that UAb(([ A0 ϕ U ψ], . . . , [ Ab minc A ϕ U ψ])) = [ Ab ϕ U ψ]. Observe that since minc A 0 and b 0, we always have 0 b b1 b minc A for all b1 {minc A, . . . , b}.

Lemma 2. UAb is monotone.

Proof. Assume that X = (X0, . . . , Xb minc A), Y = (Y0, . . . , Yb minc A) and X Y , i.e., Xi Yi for all 0 i b minc A. Then,

UAb(X) = [ψ] ([ϕ] [

minc A b1 b [ Ab1 ](Xb b1))

minc A b1 b [ Ab1 ](Yb b1))

by Xi Yi for all 0 i b minc A and Lemma 1 = UAb(Y ) 2

Lemma 3. There exists a bound min N such that [ Amin ϕ U ψ] [ Ak ϕ U ψ] for any bound k.

Proof. Consider an infinite sequence of bounds 0, 1, . . .. As (S) is finite, there is an infinite subsequence 0 i1 < i2 < . . . such that [ Ai1 ϕ U ψ] = [ Ai2 ϕ U ψ] = [ Ai3 ϕ U ψ] = . . . Let min = i1. For any k, there exists j 1 such that k ij. Then [ Aij ϕ U ψ] [ Ak ϕ U ψ] As [ Ai1 ϕ U ψ] = [ Aij ϕ U ψ], we have that [ Amin ϕ U ψ] [ Ak ϕ U ψ].

From Lemma 3, [ Amin ϕ U ψ] = [ Ak ϕ U ψ] for k min. As a result, we define the following function which is similar to UAk but accepts input vectors of the same size min + 1 for any k 0:

ˆUAk,ϕ,ψ((X0, . . . , Xmin)) = [ψ] ([ϕ] [

minc A k1 k [ Ak1 ]( Xk k1 if k k1 min Xmin otherwise ))

By Lemma 2, it is straightforward that ˆUAk is also monotone. Finally, we define the function used for fixed-point characterisation of Until:

UA,ϕ,ψ((X0, . . . , Xmin))

= ( ˆUAk((XA0, . . . , Xmin)))0 k min

Lemma 4. UA is monotone.

Proof. This is straightforward as, by Lemma 2, ˆUAk is monotone for any k.

Lemma 5. ([ A0 ϕ U ψ], . . . , [ Amin ϕ U ψ]) is the least fixed point of UA.

Proof. The Lemma follows from Claims 1 and 2 below by Knaster-Tarski s fixed-point theorem.

Claim 1. X = ([ A0 ϕ U ψ], . . . , [ Amin ϕ U ψ]) is a prefixed point of UA.

Proof. To show that X is the prefixed point of UA, we need to prove that UA(X) X, i.e., ˆUAk(X) Xk for all 0 k min:

s ˆUAk(X) s [ψ] ([ϕ] [

minc A k1 k [ Ak1 ]( Xk k1 if k k1 min Xmin otherwise ))

s [ψ] ([ϕ] [

minc A k1 k [ Ak1 ](Xk k1))

as Xk k1 = Xmin for all k k1 > min s [ψ] or s ([ϕ] [

minc A k1 k [ Ak1 ](Xk k1))

s [ψ] or k1 {minc A, k} :

s [ϕ] [ Ak1 ](Xk k1)

If s [ψ], then it is obvious that s Xk = [ Ak ϕ U ψ]. If s [ϕ] [ Ak1 ](Xk k1) = [ Ak1 ] ([ Ak k1 ϕ U ψ]), then there exists a joint action σ DA(s) such that cost(σ) k1 and out(s, σ) [ Ak k1 ϕ U ψ]. Then, for all s out(s, σ), there exists a k k1-strategy Fs to satisfy Ak k1 ϕ U ψ. Let us consider the strategy F where F(s) = σ and F(ss λ) = Fs (s λ) for all λ S . Obviously, F is a k-strategy to satisfy Ak ϕ U ψ. Therefore, s [ Ak ϕ U ψ].

Claim 2. Let X = ([ A0 ϕ U ψ], . . . , [ Amin ϕ U ψ]). For any pre-fixed point Y of UA, Y X.

Proof. We have that Y UA(Y ); as UA is monotone, it also implies Y UA(Y ) U 2 A(Y ) . . . U i A(Y ) . . . In order to prove Y X, we show that for all 0 k min, there exists i : Xk ˆU i Ak(Y ) where ˆU i Ak(Y ) is the shorthand for ˆUAk(U i 1 A (Y )). First,

s Xk s [ Ak ϕ U ψ] s k-strategy FA : λ out(s, FA) :

ls,λ 0 : λ[ls,λ] |= ψ l < ls,λ : λ[l ] |= ϕ

Let ls,k = max{ls,λ | λ out(s, FA)}, we continue the proof by induction on ls,k that s ˆU l Ak(Y ) for all l ls,k.

Base case: If ls,k = 0, then s [ψ], hence s ˆU l Ak(Y ) for any l 1 by definition of ˆUAk. Induction step: If ls,k > 0, then s [ϕ] [ Ak1 ](Xk k1) for some minc A k1 k, i.e., σ DA(s) : cost(s, σ) k1 out(s, σ) Xk k1. Then ls ,k k1 < ls,k (i.e., ls ,k k1 ls,k 1) for all s out(s, σ) Xk k1. By the induction hypothesis, we have that s ˆU l Ak k1(Y ) for all l ls ,k k1; then, s ˆU l Ak k1(Y ) for all l ls,k 1 and s out(s, σ).

This means for all l ls,k 1 we have:

out(s, σ) ˆU l Ak k1(Y ) [ Ak1 ](out(s, σ))

[ Ak1 ]( ˆU l Ak k1(Y ))

as [ Ak1 ] is monotone s [ϕ]

[ Ak1 ]( ˆU l Ak k1(Y ))

s ˆU l+1 Ak (Y )

Therefore, s ˆU l Ak(Y ) for all l ls,k. Let lk = max{ls,k | s Xk}, we have that s ˆU l Ak(Y ) for all l lk and s Xk, i.e., Xk ˆU lk Ak(Y ).

As usual, the least fixed point (Xk)0 k min of UA can be computed by repeatedly applying UA to ( , . . . , ) until a fixed point is reached. Then,

[ Ab ϕ U ψ] = Xb if b min Xmin otherwise.

It remains to find min. A coarse estimation is that min = maxc A |S| where maxc A = P i A maxci with maxci = max{c(s, i, a) | a Acti, s S}, i.e. the maximal cost of any action of any agents in A. The idea behind this estimation is that any strategy to satisfy Amin ϕ U ψ can be converted into a strategy that does not revisit any states (does not contain loops) on a path to a state where ψ is satisfied. This is made precise by the following lemma. Lemma 6. If s Ak ϕ U ψ for some k N then s Amaxc A |S| ϕ U ψ.

Proof. As s Ak ϕ U ψ, there exists a k-strategy FA such that for all λ out(s, FA): lλ 0 : λ[lλ] |= ψ and l < lλ : λ[l ] |= ϕ. Let us construct a simpler strategy F A based on FA as follows: for an arbitrary λ out(s, FA) such that l1 < l2 lλ : λ[l1] = λ[l2] : F A(λ[0, l1]λ ) = FA(λ[0, l2]λ ) for any λ S ; for others λ , F A(λ ) = FA(λ). We repeat this construction until no further simplifications can be made. Let F A be the resulting strategy. We have that for all λ out(s, F A): lλ 0 : λ[lλ] |= ψ and l < lλ : λ[l ] |= ϕ. Furthermore, no state is repeated along any λ[0, lλ] where λ out(s, F A). This means lλ < |S|. Furthermore, cost A(λ[i], F A(λ[0, i])) maxc A for all i lλ; therefore, the total cost along λ[0, lλ] is less than maxc A |S|; i.e., F A is a (maxc A |S|)-strategy; hence s Amaxc A |S| ϕ U ψ.

4.2 Box Formulas In this section, we show that [ Ab 2ϕ]M can be computed from the greatest fixed point of a function BA,ϕ defined below. First, we define a function (dependent on the bound b)

BAb,ϕ((X0, . . . , Xb minc A)) = [ϕ]

minc A b1 b [ b1 ](Xb b1))

We shall drop the subscript ϕ for convenience. Intuitively, BAb(([ A0 2ϕ], . . . , [ Ab minc A 2ϕ])) = [ Ab 2ϕ]. Then, we have the following result: Lemma 7. BAb is monotone.

Proof. The proof is similar to that of Lemma 2.

Lemma 8. There exists a bound min N such that [ Amin 2ϕ] [ Ak 2ϕ] for any bound k.

Proof. The proof is similar to that of Lemma 3.

Again, the result of Lemma 8 means that [ Amin 2ϕ] = [ Ak 2ϕ] for k kmin. As a result, we define the following function, which is similar to BAk but accepts input vectors of the same size min + 1 for any k 0:

ˆBAk,ϕ((X0, . . . , Xmin)) = ([ϕ]

minc A k1 k [ Ak1 ]( Xk k1 if k k1 min Xmin otherwise ))

This function is also monotone. Finally, we define the following function:

BA,ϕ((X0, . . . , Xmin)) =

( ˆBAk((X0, . . . , Xmin)))0 k min

Lemma 9. BA is monotone. Lemma 10. ([ A0 2ϕ], . . . , [ Amin 2ϕ]) is the greatest fixed point of BA.

Proof. The proof is similar to that of Lemma 5.

As usual, the greatest fixed point (Xk)0 k min of BA can be computed by repeatedly applying BA to (S, . . . , S) until a fixed point is reached. Then,

[ Ab 2ϕ] = Xb if b min Xmin otherwise.

It remains to find min. Again, a coarse estimation is that min = maxc A |S|. The idea behind this estimation is that any strategy to satisfy Amin 2ϕ will eventually maintain a zero-cost cycle. Then, it can be simplified so that the prefix leading to the zero-cost cycle does not repeat a state. Lemma 11. If s Ak 2ϕ for some k N then s Amaxc A |S| 2ϕ.

Proof. The proof is similar to that of Lemma 3.

4.3 Symbolic Algorithm for 1RB ATL The above results enable us to provide the symbolic model checking algorithm for 1RB ATL shown in Algorithm 2. In Algorithm 2, denotes a vector of size maxc A |S|+1 where i denotes the i-th element of for i 0. The algorithm differs from Algorithm 1 only for the cases of until formulas Ab ϕ U ψ and box formulas Ab 2ϕ. For until formulas Ab ϕ U ψ, the algorithm computes the least fixed point of UA,ϕ,ψ. It also makes use of the maximal cost maxc A of any action by agents in A which can be computed in advance.

Algorithm 2 Labelling ϕ0

function 1RB ATL-LABEL(M, ϕ0) for ϕ Sub(ϕ0) do case ϕ = p, ϕ, ϕ ψ, A ϕ, Ab ϕ, A ϕ U ψ, A 2ϕ see Algorithm 1 case ϕ = Ab ϕ U ψ ρ and τ [ψ]M while τ ρ do ρ ρ τ and τ UA,ϕ,ψ( ρ) if b < maxc A |S| then [ϕ ]M ρb else [ϕ ]M ρmaxc A |S| case ϕ = Ab 2ϕ ρ S and τ [ϕ]M while ρ τ do ρ τ and τ BA,ϕ( ρ) if b < maxc A |S| then [ϕ ]M ρb else [ϕ ]M ρmaxc A |S| return [ϕ0]M

Both are defined in Section 4.1. For box formulas Ab 2ϕ, the algorithm computes the greatest fixed point of BA,ϕ as defined in Section 4.2. The correctness of these two cases is due to Lemmas 5, 6, 10 and 11. Termination is guaranteed as the set S of states in M is finite. Theorem 1. Algorithm 2 runs in time O(|Act||Agt| |Agt|3 |S|4 ( mp) m2 c) where mp is the least cost of any action and mc is the greatest cost of any action.

Proof. We only discuss the three RB ATL modalities. First, observe that the function Pre(A, [ϕ]M, b) used in the computation of [ Ab ϕ]M case involves evaluating a boolean expression which encodes all possible joint actions of A and their costs (one boolean per cost). The size of this expression is O(|Act||Agt| |Agt|). Hence the operation takes time O(|Act||Agt| |Agt|). For readability, we abbreviate |Act||Agt| |Agt| as TP re. For the next two cases, we will use the following abbreviations. Mc = |Agt| mc is the maximal cost of any joint action. Mc |S| is an upper bound on maxc A |S| used in the algorithm. Mp = |Agt| mp is the maximal production of resource by any joint action. For Until formulas, the loop is executed at most |S| times. During each iteration, UA,ϕ,ψ( ρ) is computed. Since UA,ϕ,ψ( ρ) = ( ˆUA0( ρ), . . . , ˆUA(Mc |S|)( ρ)), and the computation of ˆUA(Mc |S|)( ρ) is the most expensive, let us compute the time required for that and multiply by Mc |S|. ˆUA(Mc |S|)( ρ) = [ψ] ([ϕ] (Z1 . . . ZMp+(Mc |S|))), where each Zj is of the form [ Akj ]( ρj), so computing it takes time O(TP re). Then the computation of ˆUA(Mc |S|)( ρ) is O(TP re (Mp + (Mc |S|))) and the computation of

UA,ϕ,ψ( ρ) is O(TP re (Mp + (Mc |S|)) (Mc |S|)). Finally, the loop for until formulas takes time

O(TP re (Mp + (Mc |S|)) (Mc |S|) |S|)

A similar analysis shows that the running time of the Box loop is the same, hence so is the running time of the whole algorithm. Substituting expressions for TP re, Mc and Mp gives O(|Act||Agt| |Agt|3 |S|4 ( mp) m2 c).

Note that the |Act||Agt| component is the cost of computing Pre symbolically, and it corresponds to the number of all possible joint actions in the model. If the set of joint actions is considered to be part of the input, the algorithm runs in time polynomial in the size of the model.

5 Experimental Evaluation of Performance

In this section, we describe an experiment designed to show the scalability of the symbolic implementation of the modelchecking algorithm for 1RB ATL, and compare its performance with that of the hybrid model-checking algorithm for RB ATL. Consider a scenario in which three agents compete in an infinite sequence of car races by spending and earning money. Each car is equipped with one of three possible types of engine T = {1, 2, 3}. Initially, agent 1 has an engine of type 1, agent 2 of type 2, and agent 3 of type 3. Each race consists of 3 steps:

Set-up: Agents can choose whether to upgrade their engine; upgrading from engine type i to type i + 1 costs $1 (i |T| 1).

Race: Agents can choose to race (at a cost of $1), or to remain idle (at a cost of $0). The ranking of the race is decided as follows: idle agents have rank 4th. The other agents are partitioned in disjoint sets of participants with the same engine type. The agents in the set with engine type 3 have rank 1st; the agents in the next partition have a rank equal to the number of agents in the previous set plus the rank of those agents, and so on.

Award: Agents can execute an action to accept their ranking, or perform an idle action. The action of accepting their ranking produces $3 if the agent ranks 1st, $2 if they rank 2nd, and $1 for 3rd.

The race is then repeated. If all agents decide to race starting from the configuration above, agent 3 will win and produce $3, agent 2 will produce $2, while agent 1 will produce $1. It is possible to verify that no agent can participate in the race with a bound of $0. It is also possible to verify that agent 1 cannot be ranked 1st with a bound of $2, but it can if the bound is $3 (because it can decide to upgrade but not race in the first two rounds, and only race in the third one). More interestingly, it is possible to verify that if agents 1 and 2 cooperate, then they can both be ranked 1st under a bound $1. To achieve this, one of the two agents has to idle (not race), until the other agent has accumulated enough money to upgrade its engine; when both agents have upgraded their engines they can both win the race.

This scenario can be scaled up to any number of agents and any number of engine types. We have implemented Algorithm 2 on top of the model checker MCMAS [Lomuscio et al., 2009] and we have encoded examples in which the number of engine types |T| {3, 4, 5, 6}1. In the experiment, we verify, for each encoding with T types of engines, whether agent 1 can eventually win the race within the bounds b {|T| 1, |T|} and the coalition of agents 1 and 2 can cooperate so that eventually agent 1 wins the race. In other words, we want to check if the formulas ϕ1(b) = {1}b U 1fst for b {|T| 1, |T|} and ϕ2 = {1, 2}1 U 1fst where 1fst is a proposition that is only true in states where agent 1 ranks first. The experiment was carried out on a quad-core 64-bit Processor running at 2.66 GHz with 32GB of memory. The results are summarised in Table 1 (Holds records whether the formula is true in the model). As it can be seen, in this example the symbolic algorithm always uses less memory. It also outperforms the hybrid algorithm when verifying ϕ1 (from 2 to 1961 times faster) and catches up when verifying ϕ2 (eventually 3 times faster).

Hybrid Symbolic Ratio Hybrid Symbolic Ratio No 0.509 0.175 2.91 10.23 9.09 1.12 Yes 0.595 0.175 3.40 10.23 9.09 1.12 Yes 0.210 0.745 0.28 10.01 9.16 1.09 No 37.300 0.826 45.16 11.40 9.31 1.22 Yes 64.252 0.821 78.26 11.40 9.31 1.22 Yes 1.649 5.146 0.32 10.82 9.51 1.14 No 4582.360 3.543 1293.36 14.19 10.22 1.39 Yes 6792.980 3.463 1961.59 15.60 10.22 1.53 Yes 14.678 19.154 0.77 13.52 10.33 1.31 No time-out 6.233 - 10.15 - Yes time-out 6.182 - 10.15 - Yes 115.370 30.013 3.84 14.57 10.23 1.42

Time (s) Memory (MB) Types Fomulas Holds

time-out time-out

Table 1: Comparison between symbolic and hybrid implementations. Time-out means no termination within 3 hours.

6 Conclusion and future work We have presented a fixed point characterisation of coalition modalities in the resource logic 1RB ATL. This enabled us to state and implement a symbolic model-checking algorithm for 1RB ATL. We gave an evaluation of the performance of the algorithm on a parameterised example, which shows that the symbolic algorithm is more scalable than the hybrid one. We conjecture that full RB ATL does not have a fixed point characterisation. In future work, we plan to settle this question and investigate other resource logics (or their fragments) with decidable model-checking problems.

References [Alechina et al., 2009] N. Alechina, B. Logan, H. N. Nguyen, and A. Rakib. A logic for coalitions with bounded resources. In Proc. of the 21st International Joint Conference on Artificial Intelligence, volume 2, pages 659 664. AAAI Press, 2009.

1Available from www.vrbmas.org/dl/ijcai15.zip

[Alechina et al., 2010] N. Alechina, B. Logan, H. N. Nguyen, and A. Rakib. Resource-bounded alternatingtime temporal logic. In Proc. of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), pages 481 488. IFAAMAS, 2010. [Alechina et al., 2014] N. Alechina, B. Logan, H. N. Nguyen, and F. Raimondi. Decidable Model-Checking for a Resource Logic with Production of Resources. In 21st European Conference on Artificial Intelligence, pages 9 14, 2014. [Alechina et al., 2015] N. Alechina, B. Logan, H. N. Nguyen, F. Raimondi, and L. Mostarda. Symbolic modelchecking for resource-bounded ATL. In Proc. of the 14th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2015), pages 1809 1810. IFAAMAS, 2015. [Alur et al., 2002] R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672 713, 2002. [Bryant, 1986] Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677 691, 1986. [Bulling and Farwer, 2010] N. Bulling and B. Farwer. On the (un-)decidability of model checking resource-bounded agents. In Proc. of the 19th European Conference on Artificial Intelligence (ECAI 2010), volume 215, pages 567 572. IOS Press, 2010. [Bulling and Goranko, 2013] N. Bulling and V. Goranko. How to be both rich and happy: Combining quantitative and qualitative strategic reasoning about multi-player games (extended abstract). In Proc. 1st International Workshop on Strategic Reasoning, SR 2013, volume 112 of EPTCS, pages 33 41, 2013. [Della Monica et al., 2011] D. Della Monica, M. Napoli, and M. Parente. On a logic for coalitional games with priced-resource agents. Electr. Notes Theor. Comput. Sci., 278:215 228, 2011. [Della Monica et al., 2013] D. Della Monica, M. Napoli, and M. Parente. Model checking coalitional games in shortage resource scenarios. In Proc. of the 4th International Symposium on Games, Automata, Logics and Formal Verification (Gand ALF 2013, volume 119 of EPTCS, pages 240 255, 2013. [Gammie and Van Der Meyden, 2004] P. Gammie and R. Van Der Meyden. MCK: Model checking the logic of knowledge. In Computer Aided Verification, pages 479 483. Springer Berlin Heidelberg, 2004. [Leroux, 2013] J. Leroux. Acceleration for Petri Nets. In Proc. of the 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, volume 8172 of LNCS, pages 1 4. Springer, 2013. [Lomuscio et al., 2009] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proc. of the 21st International Conference on Computer Aided Verification, CAV 09, pages 682 688, 2009.