Symbolic Model Checking for One-Resource RB+-ATL

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 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].

†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.

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].

2 RB±ATL

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 (∞, . . . ,∞).

Formulas of RB±ATL are defined by the following syntax

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 〉〉✷ϕ 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, σ) ↦→ 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 costA(s, σA) = ∑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,

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 〉〉✷ϕ 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 HybridModel 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〉〉✷ϕ 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 〉〉✷ϕ [ϕ′ ]M ← { s | s ∈ S ∧ BOX-STRATEGY(node0(s, b), 〈〈Ab 〉〉✷ϕ)} 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 〉〉✷ϕ, 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 〉〉✷ϕ is more complex, and requires two auxiliary functions: UNTIL-STRATEGY for 〈〈Ab 〉〉ϕU ψ and BOXSTRATEGY for 〈〈Ab 〉〉✷ϕ. 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 〉〉✷ϕ 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 mincA = ∑i∈A minci the minimal cost of any joint action by the non-empty coalition A. Again, mincA ≤ 0 and there is no joint action for A that costs less than mincA.

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 < mincA and X ⊆ S.

Proof. Assume that X ⊆ Y . Then:

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

For convenience, we drop the subscripts ϕ,ψ in the remainder of this section. Note that UAb(([〈〈A0 〉〉ϕU ψ], . . . , [〈〈Ab-mincA 〉〉ϕ U ψ])) = [〈〈Ab 〉〉ϕ U ψ].

Observe that since mincA ≤ 0 and b ≥ 0, we always have 0 ≤ b - b1 ≤ b -mincA for all b1 ∈ {mincA, . . . , b}.

Lemma 2. UAb is monotone.

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

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:

By Lemma 2, it is straightforward that ˆUAk is alsomonotone.

Finally, we define the function used for fixed-point characterisation of Until:

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.

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:

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 ψ].

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

Let ls,k = max{ls,λ | λ ∈ out(s, FA)}, we continue the proof by induction on ls,k that s ∈ ˆU lAk(Y ) for all l ≥ ls,k. Base case: If ls,k = 0, then s ∈ [ψ], hence s ∈ ˆU lAk(Y ) for

any l ≥ 1 by definition of ˆUAk .

Induction step: If ls,k > 0, then s ∈ [ϕ] ∩ [〈〈Ak1 〉〉©](Xk-k1 ) for some mincA ≤ 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 lAk-k1 (Y ) for all l ≥ ls′ ,k-k1 ; then, s′ ∈ ˆU lAk-k1 (Y ) for all l ≥ ls,k - 1 and s′ ∈ out(s, σ).

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

Therefore, s ∈ ˆU lAk(Y ) for all l ≥ ls,k. Let lk = max{ls,k | s ∈ Xk}, we have that s ∈ ˆU lAk (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,

It remains to find min. A coarse estimation is that min = maxcA × |S| where maxcA = ∑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 ∈ 〈〈AmaxcA×|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, costA(λ[i], F ′′A(λ[0, i])) ≤ maxcA for all i ≤ lλ; therefore, the total cost along λ[0, lλ] is less than maxcA × |S|; i.e., F ′′A is a (maxcA × |S|)-strategy; hence s ∈ 〈〈AmaxcA×|S| 〉〉ϕ U ψ.

4.2 Box Formulas

In this section, we show that [〈〈Ab 〉〉✷ϕ]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)

We shall drop the subscript ϕ for convenience. Intuitively, BAb(([〈〈A0 〉〉✷ϕ], . . . , [〈〈Ab-mincA 〉〉✷ϕ])) = [〈〈Ab 〉〉✷ϕ]. 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 〉〉✷ϕ] ⊇ [〈〈Ak 〉〉✷ϕ] for any bound k.

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

Again, the result of Lemma 8 means that [〈〈Amin 〉〉✷ϕ] = [〈〈Ak 〉〉✷ϕ] 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:

This function is also monotone.

Finally, we define the following function:

Lemma 9. BA is monotone.

Lemma 10. ([〈〈A0 〉〉✷ϕ], . . . , [〈〈Amin 〉〉✷ϕ]) 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,

It remains to find min. Again, a coarse estimation is that min = maxcA × |S|. The idea behind this estimation is that any strategy to satisfy 〈〈Amin 〉〉✷ϕ 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.

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 maxcA × |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 〉〉✷ϕ. For until formulas 〈〈Ab 〉〉ϕU ψ, the algorithm computes the least fixed point of UA,ϕ,ψ. It also makes use of the maximal cost maxcA 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〉〉✷ϕ see Algorithm 1 case ϕ′ = 〈〈Ab 〉〉ϕU ψ ¯ ρ ← ¯∅ and ¯ τ ← [ψ]M while ¯ τ ̸⊆ ¯ ρ do ¯ ρ ← ¯ ρ ∪ ¯ τ and ¯ τ ← UA,ϕ,ψ(¯ ρ) if b < maxcA × |S| then [ϕ′ ]M ← ¯ ρb else[ϕ′ ]M ← ¯ ρmaxcA×|S| case ϕ′ = 〈〈Ab 〉〉✷ϕ ¯ ρ ← ¯ S and ¯ τ ← [ϕ]M while ¯ ρ ̸⊆ ¯ τ do ¯ ρ ← ¯ τ and ¯ τ ← BA,ϕ(¯ ρ) if b < maxcA × |S| then [ϕ′ ]M ← ¯ ρb else[ϕ′ ]M ← ¯ ρmaxcA×|S| return [ϕ0]M

Both are defined in Section 4.1. For box formulas 〈〈Ab 〉〉✷ϕ, 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.

Theorem1. Algorithm2 runs in timeO(|Act||Agt|×|Agt|3× |S|4 ×(-mp)×m2c ) 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 TPre.

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 maxcA × |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(TPre). Then the computation of ˆUA(Mc×|S|)(¯ ρ) is O(TPre × (Mp + (Mc × |S|))) and the computation of UA,ϕ,ψ( ¯ ρ) is O(TPre × (Mp + (Mc × |S|)) × (Mc × |S|)). Finally, the loop for until formulas takes time

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 TPre, Mc and Mp gives O(|Act||Agt| × |Agt|3 × |S|4 × (-mp) × m2c ).

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).

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.