An extension of RB-ATL Nguyen Hoang Nga Abstract RB-ATL is a logic to specify coalitional properties of multiagent systems where actions cost certain amount of resources. RB-ATL allows us to express properties such as within a limited amount of resources, a group of agents can produce a particular result but not another. This paper extends RB-ATL so that it is possible to express coalitional properties where we only consider the limitation over a subset of all resources. 1 Introduction In previous work [2], we have presented a logic, namely RB-ATL, which allows expressing and reasoning about properties of coalitional ability under resource con- straints. The logic extended ATL [3] where a bound over resources is added into each cooperation modality. Each resource bound, defined as a vector, specifies the upper bound over each resource available to (or willing to contribute by) an agent or a group of agents. This means it is not possible to express properties in RB-ATL where the upper bound over a subset of resources is of interest. For example, let us consider a set of two resources: memory and network band- width. It is possible to express in RB-ATL the property that Agents 1 and 2 can enforce p to become true without using more than 4 units of memory and 2 units of network bandwidth by the formula ⟪{1, 2}(4,2) ⟫⊺Up. However, if we would like to express the same property except we do not care about how much net- work bandwidth can be used, it is not possible to do so in RB-ATL unless the language allows infinite disjunction. For this reason, the property can only be writ- ten as ⋁n≥0 ⟪{1, 2}(4,n) ⟫⊺Up. In order to express such properties, in this paper, we extend RB-ATL by allowing the inclusion of an extra symbol ∞ in the resource bounds. The idea is that whenever no limit is required over a resource, we can set the bound for this resource as ∞. We also show that the resulting logic RBATL∞ is sound and complete. The remainder of this paper is structured as follows. We first briefly recall the syntax and semantics of RB-ATL. Then, we introduce the syntax and semantics 1 35 of the extended logic RBATL∞ . After that, we give a complete axiomatization followed by a sketch proof of the completeness. At the end is the section of related work and conclusion. 2 Resource-bounded ATL As RBATL∞ is based on RB-ATL [2], we first briefly recall RB-ATL. RB-ATL extended ATL in order to allow expressing properties of coalitional ability under limited amounts of resources. Bounds on resources are defined as vectors of num- bers each of which corresponds to the bound on a type of resources. If we fix a finite set of resources r, then the set of bounds is defined as B = N∣r∣ . Given a set of propositions Φ and a finite set of agents N , formulas of RB-ATL are defined by the following syntax: ϕ ∶∶= p ∣ ¬ϕ ∣ ϕ ∨ ψ ∣ ⟪Ab ⟫◯ϕ ∣ ⟪Ab ⟫ϕUψ ∣ ⟪Ab ⟫ ◻ ϕ where p ∈ Φ, A ⊆ N and b ∈ B. Intuitively, ⟪Ab ⟫◯ϕ says that the coalition A can co-operate (in one step) to make ϕ true without spending more than b amount of resources. Similarly, ⟪Ab ⟫ϕUψ means that the coalition A can co-operate (in many consecutive steps) to eventually make ψ true without spending more than b amount of resources while keeping ϕ true; and ⟪Ab ⟫ ◻ ϕ says that the coalition A can co-operative from now on to guaranty that ϕ is true without spending more than b amount of resources. For convenience, we only study the soundness and completeness of the normal form version of RB-ATL whose syntax is as follows: ϕ ∶∶= (¬)p ∣ ϕ ∨ ψ ∣ ϕ ∧ ψ ∣ (¬)⟪Ab ⟫◯ϕ ∣ (¬)⟪Ab ⟫ϕUψ ∣ (¬)⟪Ab ⟫ ◻ ϕ For short, normal form RB-ATL are referred to as RB-ATL in the rest of this paper. We also use ∼ϕ to denote the equivalent normal form formula of ¬ϕ. Semantics of RB-ATL is defined in terms of Resource-bounded Concurrent Game Structures (RB-CGS) together with the notions of move, co-move, strategy and co-strategy. A Resource-bounded Concurrent Game Structure (RB-CGS) is a tuple S = (n, Q, Π, π, d, c, δ) where: • n ≥ 1 is the number of players (agents), we denote the set of players {1, . . . , n} by N • Q is a non-empty set of states • Π is a finite set of propositional variables 2 36 • π ∶ Q → ℘(Π) is a mapping which assigns each state in Q a subset of propositional variables • d ∶ Q × N → N is a mapping to indicate the number of available moves (actions) for each player a ∈ N at a state q ∈ Q such that d(q, a) ≥ 1. At each state q ∈ Q, we denote the set of joint moves available for all players in N by D(q). That is D(q) = {1, . . . , d(q, 1)} × . . . × {1, . . . , d(q, n)} • c ∶ Q × N × N → B is a mapping to indicate the minimal amount of resources required by each move available to each agent at a specific state. • δ ∶ Q × Nn → Q is a mapping which assigns the next state of the system after agents perform a joint move in D(q) from a state. From the definition of RB-CGSs, resource bounds are used to specify the costs of actions performed by agents. In order to express the spending of a subset of agents in one or many steps, we aggregate the spending of each agent in the subset. This type of aggregation is called parallel aggregation. Another type of aggregation is called serial where an agent (coalition) performs some (joint) action and then performs another (joint) action; the aggregative spending of the agent (coalition) after the two steps is the serial aggregation of the costs of the two (joint) actions. For simplicity, we assume in this paper that both types of aggregations are defined as addition. Given a RB-CGS S = (n, Q, Π, π, d, c, δ), we denote the set of infinite se- quences of states by Qω as usual. Let λ = q0 q1 . . . ∈ Qω , we denote λ[i] = qi and λ[i, j] = qi . . . qj . A move for a coalition A ⊆ N at a state q ∈ Q is a tuple σA = (σa )a∈A such that 1 ≤ σa ≤ d(q, a). For convenience, we denote DA (q) to be the set of all moves for A at q. Furthermore, given m ∈ D(q), we de- note mA = (ma )a∈A . Then we define the set of all possible outcomes by a move σA ∈ DA (q) at a state q as follows out(q, σA ) = {q ′ ∈ Q ∣ ∃m ∈ D(q) ∶ mA = σA ∧ q ′ = δ(q, m)} The cost of a move σA ∈ DA (q) then is defined as cost(q, σA ) = ∑a∈A c(q, a, σa ). A strategy for a coalition A ⊆ N is a mapping FA which associates each sequence λq ∈ Q+ to a move in DA (q). A computation λ ∈ Qω is consistent with FA iff for all i ≥ 0, λ[i + 1] ∈ out(λ[i], FA (λ[0, i])). We denote by out(q, FA ) the set of all such sequences λ starting from q, i.e. q = λ[0]. Given a bound b ∈ B, a computation λ ∈ out(q, FA ) is b-consistent with FA iff, for every i ≥ 0, ∑ij=0 cost(λ[i], FA (λ[0, i])) ≤ b. We denote out(q0 , FA , b) the set of all such 3 37 sequences. Then, a strategy FA is a b-strategy iff out(q, FA ) = out(q, FA , b) for any q ∈ Q. Similarly to the case of moves and strategies, we define a co-move for a coali- tion A ⊆ N as a mapping σA c ∶ DA (q) → Q such that σA c (σA ) ∈ out(q, σA ) for any σA ∈ DA (q). We denote DA (q) be the set of all co-moves for A at a state c q ∈ Q. A state q ′ is consistent with a co-move σ c iff there is some move σA such that σ c (σA ) = q ′ . We define the set of consistent outcomes for a co-move σ c by out(q, σ c ) = {q ′ ∈ Q ∣ q ′ is consistent with σ c } Given a bound b ∈ B, a state q ′ is b-consistent with a co-move σ c at q iff there is some move σA ∈ DA (q) with cost(q, σA ) ≤ b such that σ c (σA ) = q ′ . We denote the set of b-consistent outcomes for a co-move σ c by out(q, σ c , b) = {q ′ ∈ Q ∣ q ′ is b-consistent with σ c at q} A co-strategy for a coalition A ⊆ N is a mapping FAc which assigns each sequence λq ∈ Q+ to a co-move in DA c (q). We say a computation λ ∈ Qω is con- sistent with FA iff, for all i ≥ 0, λ[i + 1] ∈ out(λ[i], FAc (λ[0, i])). Let us define c out(q, FAc ) to be the set of all such sequences where q = λ[0]. We say a computa- tion λ ∈ out(q, FAc ) is b-consistent with FAc iff, for all i ≥ 0, there is a sequence of moves σA 0 ∈ DA (λ[0]), . . . , σA i ∈ DA (λ[i]) such that λj+1 = FAc (λ[0, j])(σA j ) for all j = 0, . . . , i and ∑j cost(λ[j], σA j ) ≤ b. Let us denote out(q, FAc , b) be the set of all such sequences where q = λ[0]. The truth of a RB-ATL formula ϕ at a state q of a RB-CGS S is defined by induction on the structure of ϕ. We ignore the propositional cases, other cases are listed as follows: • S, q ⊧ ⟪Ab ⟫◯ϕ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA ), S, λ[1] ⊧ ϕ iff there is a move σA ∈ DA (q) such that for all q ′ ∈ out(σA ), S, q ′ ⊧ ϕ • S, q ⊧ ¬⟪Ab ⟫◯ϕ iff there exists a co-strategy FAc such that for all λ ∈ out(q, FA , b), S, λ[1] ⊧∼ ϕ iff there is a co-move σ c ∈ DA c (q) such that for all σA ∈ DA (q) and cost(σA ) ≤ b, S, σ (σA ) ⊧∼ϕ c • S, q ⊧ ⟪Ab ⟫ ◻ ϕ iff there exists a b-strategy FA for any λ ∈ out(q, FA ), S, λ[i] ⊧ ϕ for all i ≥ 0 • S, q ⊧ ¬⟪Ab ⟫ ◻ ϕ iff there exists a co-strategy FAc for any λ ∈ out(q, FAc , b), S, λ[i] ⊧ ϕ for all i ≥ 0 4 38 • S, q ⊧ ⟪Ab ⟫ϕUψ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA ), there is a position i ≥ 0 such that S, λ[i] ⊧ ψ and S, λ[j] ⊧ ψ for all j ∈ {0, . . . , i − 1} • S, q ⊧ ¬⟪Ab ⟫ϕUψ iff there exists a co-strategy FAc such that for all λ ∈ out(q, FA , b), either S, λ[i] ⊧ ψ for all i ≥ 0 or if there is a position i ≥ 0 such that S, λ[i] ⊧ ψ then there exists 0 ≤ j < i such that S, λ[j] ⊧∼ϕ 3 Syntax and semantics of RBATL∞ We define the set of resource bounds with infinity as B∞ = (N ∪ {∞})∣r∣ . To make addition and comparison over resource bounds compatible with infinity, we extend them to include the case ∞ as follows: n+∞=n+∞ = ∞ ∞+∞ = ∞ n ≤ ∞ ∞ ≤ ∞ where n ∈ N. Notice that costs of actions in RB-CGSs are still defined by B while bounds appearing in RB-ATL formulas may include infinity. The syntax of (normal form) RBATL∞ is defined as follows. ϕ ∶∶= (¬)p ∣ ϕ ∨ ψ ∣ ϕ ∧ ψ ∣ (¬)⟪Ab ⟫◯ϕ ∣ (¬)⟪Ab ⟫ϕUψ ∣ (¬)⟪Ab ⟫ ◻ ϕ where p ∈ Φ, b ∈ B∞ and A ⊆ N . We define the ⟪∅b ⟫◯ modality as the dual one of ⟪N b ⟫◯, i.e. ⟪∅b ⟫◯ϕ ≡ ¬⟪N b ⟫◯ ∼ ϕ. This modality is to say that a system of multiple agents cannot avoid some thing if they are not allowed to spend more than some b amount of resources. The semantics of RBATL∞ is also defined by means of RB-CSGs. However, we need to extend the notion of b-consistency of strategies to include the case where b ∈ B∞ . Given a bound b ∈ B∞ and a strategy FA , a computation λ ∈ out(q, FA ) is b-consistent with FA iff, for every i ≥ 0, ∑ij=0 cost(λ[i], FA (λ[0, i])) ≤ b. We denote out(q0 , FA , b) the set of all such sequences. Then, a strategy FA is a b- strategy iff out(q, FA ) = out(q, FA , b) for any q ∈ Q. Similar extensions are also applied for the case of co-moves and co-strategies. Given a RB-CGS S = (n, Q, Π, π, d, c, δ), the truth of a RBATL∞ formula is defined inductively as follows where A is a non-empty coalition: • S, q ⊧ p iff p ∈ π(q) • S, q ⊧ ¬p iff p ∉ π(q) 5 39 • S, q ⊧ ϕ ∨ ψ iff S, q ⊧ ϕ or S, q ⊧ ψ • S, q ⊧ ϕ ∧ ψ iff S, q ⊧ ϕ and S, q ⊧ ψ • S, q ⊧ ⟪Ab ⟫◯ϕ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA ), S, λ[1] ⊧ ϕ. In other words, it is equivalent to say that there is a move σA ∈ DA (q) such that for all q ′ ∈ out(σA ), S, q ′ ⊧ ϕ • S, q ⊧ ¬⟪Ab ⟫◯ϕ iff there exists a co-strategy FAc such that for all λ ∈ out(q, FA , b), S, λ[1] ⊧∼ ϕ. In other words, it is equivalent to say that there is a co-move σ c ∈ DA c (q) such that for all σA ∈ DA (q) and cost(σA ) ≤ b, S, σ (σA ) ⊧∼ϕ c • S, q ⊧ ⟪∅b ⟫◯ϕ iff for every b-strategy FN for all λ ∈ out(q, FA ), S, λ[1] ⊧ ϕ • S, q ⊧ ¬⟪∅b ⟫◯ϕ iff there is a b-strategy FN such that for all λ ∈ out(q, FN ), S, λ[1] ⊧∼ϕ • S, q ⊧ ⟪Ab ⟫ ◻ ϕ iff there exists a b-strategy FA for any λ ∈ out(q, FA ), S, λ[i] ⊧ ϕ for all i ≥ 0 • S, q ⊧ ¬⟪Ab ⟫ ◻ ϕ iff there exists a co-strategy FAc for any λ ∈ out(q, FAc , b), S, λ[i] ⊧ ϕ for all i ≥ 0 • S, q ⊧ ⟪Ab ⟫ϕUψ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA ), there is a position i ≥ 0 such that S, λ[i] ⊧ ψ and S, λ[j] ⊧ ψ for all j ∈ {0, . . . , i − 1} • S, q ⊧ ¬⟪Ab ⟫ϕUψ iff there exists a co-strategy FAc such that for all λ ∈ out(q, FA , b), either S, λ[i] ⊧ ψ for all i ≥ 0 or if there is a position i ≥ 0 such that S, λ[i] ⊧ ψ then there exists 0 ≤ j < i such that S, λ[j] ⊧∼ϕ 4 Axiomatisation In this section, we present an axiomatisation system of RBATL∞ . We first in- troduce notations appearing in the axiomatisation. In the following, A, A1 , A2 denotes non-empty coalitions, b, b1 , b2 and d ∈ B∞ . We say that b +∞ d = e for any b, d and e ∈ B∞ iff for every i = 1, . . . , ∣r∣, bi + di = ei if ei =/ ∞ bi = di = ∞ if ei = ∞ 6 40 Intuitively, +∞ is used to split the usage of resources over multiple stages. As ∞ in some bound component means no constraint is required on the corresponding re- source, we can also ignore the limitation on this resource in each stage by assigning ∞ to the corresponding component in each stage. For example, consider the bound (2, 3, ∞), it can be split into (1, 2, ∞) and (1, 1, ∞) so that the bound on the third resource is ignored. Using +∞ rather than + makes sure that the number of ways to split of resource bounds is finite. Hence, we define the following macros: ⟪Ab ⟫◯ ◻ ϕ = ⋁b1 +∞ b2 =b ⟪Ab1 ⟫◯⟪Ab2 ⟫ ◻ ϕ ¬⟪Ab ⟫◯ ◻ ϕ = ⋀b1 +∞ b2 =b ¬⟪Ab1 ⟫◯⟪Ab2 ⟫ ◻ ϕ ⟪Ab ⟫◯ϕUψ = ⋁b1 +∞ b2 =b ⟪Ab1 ⟫◯⟪Ab2 ⟫ϕUψ ¬⟪Ab ⟫◯ϕUψ = ⋀b1 +∞ b2 =b ¬⟪Ab1 ⟫◯⟪Ab2 ⟫ϕUψ ⟪∅b ⟫◯ ◻ ϕ = ⋀b1 +∞ b2 =b ⟪∅b1 ⟫◯⟪∅b2 ⟫ ◻ ϕ ¬⟪∅b ⟫◯ ◻ ϕ = ⋁b1 +∞ b2 =b ⟪∅b1 ⟫◯⟪∅b2 ⟫ ◻ ϕ Similar to the reason of introducing +∞ , we also define a zero bound 0̄b with respect to a bound b in B∞ as follows, for all i = 1, . . . , ∣r∣ 0 if bi =/ ∞ (0̄b )i = � ∞ otherwise This means we ignore any component which is ∞. The axiomatisation system of RBATL∞ is as follows: Axioms (PL) Tautologies of Propositional Logic (�) ¬⟪Ab ⟫◯� (⊺) ⟪Ab ⟫◯⊺ (B) ⟪Ab ⟫◯ϕ → ⟪Ad ⟫◯ϕ where b ≤ d (S) ⟪Ab11 ⟫◯ϕ ∧ ⟪Ab22 ⟫◯ψ → ⟪(A1 ∪ A2 )b1 +b2 ⟫◯(ϕ ∧ ψ) where A1 ∩ A2 = ∅ (S∅ ) ⟪∅b1 ⟫◯ϕ ∧ ⟪∅b2 ⟫◯ψ → ⟪∅b1 ⟫◯(ϕ ∧ ψ) where b1 ≤ b2 (SN ) ⟪N b1 ⟫◯ϕ ∧ ⟪∅b2 ⟫◯ψ → ⟪N b1 ⟫◯(ϕ ∧ ψ) where b1 ≤ b2 7 41 (FP◻ ) ⟪Ab ⟫ ◻ ϕ ↔ ϕ ∧ (⟪Ab ⟫◯ ◻ ϕ ∨ ⟪A0̄b ⟫◯(⟪Ab ⟫ ◻ ϕ)) (FPU ) ⟪Ab ⟫ϕUψ ↔ ψ ∨ (ϕ ∧ (⟪Ab ⟫◯ϕUψ ∨ ⟪A0̄b ⟫◯(⟪Ab ⟫ϕUψ))) (N◯ ) ⟪∅b ⟫◯ϕ ↔ ¬⟪N b ⟫◯(¬ϕ) (N◻ ) ⟪∅b ⟫ ◻ ϕ ↔ ϕ ∧ ¬⟪N b ⟫⊺U¬ϕ (NU ) ⟪∅b ⟫ϕUψ ↔ ¬(⟪N b ⟫¬ψU¬(ϕ ∨ ψ) ∨ ⟪N b ⟫ ◻ ¬ψ) Inference rules ϕ, ϕ → ψ (MP) ψ ϕ→ψ (⟪Ab ⟫◯-Monotonicity) ⟪Ab ⟫◯ϕ → ⟪Ab ⟫◯ψ (⟪∅b ⟫◻-Necessitation) ϕ ⟪∅b ⟫ ◻ ϕ θ → (ϕ ∧ (⟪Ab ⟫◯ ◻ ϕ ∨ ⟪A0̄b ⟫◯θ)) (⟪Ab ⟫◻-Induction) θ → ⟪Ab ⟫ ◻ ϕ (ψ ∨ (ϕ ∧ (⟪Ab ⟫◯ϕUψ) ∨ ⟪A0̄b ⟫◯θ))) → θ (⟪Ab ⟫U-Induction) ⟪Ab ⟫ϕUψ → θ Proposition 1. The above axiomatization system for RBATL∞ is sound and com- plete. In the rest of this section, we provide a sketch proof of Proposition 1. As the proof of soundness is straightforward, it is ignored here. To prove the com- pleteness, as usual, we will construct a model for any consistent formula ϕ0 of RBATL∞ . The constructed models are in the form of fixed-branch trees defined as follows. Given a finite alphabet Θ, we denote the sets of finite words and infinite words of Θ by Θ∗ and Θω , respectively. Definition 1. A tree T is a subset of N∗ where for any x ⋅ c ∈ T , where x ∈ N∗ and c ∈ N: • x∈T • x ⋅ c′ ∈ T for all 0 ≤ c′ ≤ c 8 42 Given a tree T , � is the root of T . Nodes of T are elements of T . We define succ ∶ T → 2T as a function to return the successors of a node x ∈ T . Formally, succ(x) = {x ⋅ c ∈ T ∣ c ∈ N}. The degree d(x)of a node x is defined as the cardinality of succ(x), i.e. d(x) = ∣succ(x)∣. A node x is a leaf iff d(x) = 0. A node x is an interior node iff d(x) > 0. Definition 2. Given a set Θ, a Θ-labeled tree is a pair (T, V ) where T is a tree and V ∶ T → Θ is a mapping which labels each node of T with an element of Θ. Given a finite set of agents N = {1, . . . , n}, for the purpose of constructing models for consistent formulas of RB-ATL, we are interested in a special form of Θ-labeled trees (T, V ) where Θ is the set 2Π of subsets of propositions and the degree of every node of T is fixed by some given number k ∈ N, i.e. deg(x) = k n for all x ∈ T . Then, a 2Π -labeled tree (T, V ) with a fixed degree k n can be considered as the skeleton of a model for RB-ATL formulas. We call a tree with a fixed degree k n as a k n -tree. Informally, each node of T is considered as a state. From each state x ∈ T , there are k n transitions to its successors, namely from x ⋅ 0 to x ⋅ k n − 1. We can name each transition from x to x ⋅ c by a tuple (a1 , . . . , an ) where 1. 1 ≤ ai ≤ k 2. encode((a1 , . . . , an )) = c Where encode ∶ {1, . . . , k}n → {0, . . . , k n − 1} is a bijective function which is defined as encode((x1 , . . . , xn )) = (x1 − 1)k n−1 + (x2 − 1)k n−2 + . . . + (xn − 1) For convenience, we call the inverse function of encode as decode. Then, each transition from x to x ⋅ c can be considered as the effect of the joint action of n agents in N where agent i performs the action ai for all i ∈ {1, . . . , n} and (a1 , . . . , an ) = decode(c). Moreover, to become a model for RB-ATL formulas, we need to supply for each 2Π -labeled k n -tree (T, V ) a costing function which defines the cost of each action of an agent at a node on the tree. We have the following definition. Definition 3. A 2Π -labeled k n -costed-tree is a tuple (T, V, C) where (T, V ) is a 2Π -labeled k n -tree and C ∶ T × N × {1, . . . , k} → B is a costing function. Given a 2Π -labeled k n -costed-tree (T, V, C), we define the corresponding RB- CGS S(T,V,C) = (n, T, Π, V, d, C, δ) where d(x, i) = k for all x ∈ T and i ∈ N and δ(x, (a1 , . . . , an )) = x⋅encode((a1 , . . . , an )). It is straightforward that S(T,V,C) is 9 43 well-defined. We shall write (T, V, C), x ⊧ ϕ for S(T,V,C) , x ⊧ ϕ and (T, V, C) ⊧ ϕ for (T, V, C), � ⊧ ϕ. Furthermore, we also have that in S(T,V,C) , the available joint actions for any coalition A at any state are the same, i.e. DA (x) = DA (x′ ) for any x, x′ ∈ T , hence we shall write ΔA for DA (x). Notice that when constructing the tree model for a consistent formula, we build n k -costed-trees which are labeled by subsets of formulas rather than only a subset of propositional variables. However, we can consider them as models for RB-ATL formulas by restricting the labeling function V over the set of propositions, i.e. V (t) ∩ Π. Finally, we define a simple tree as a tree which consists of only a root and its children. The ingredients for labeling nodes of tree during the construction are defined in terms of closure of ϕ0 . Definition 4. The closure cl(ϕ0 ) is the smallest set of formulas that satisfies the following closure condition: • All sub-formulas of ϕ including itself are in cl(ϕ0 ) • If ⟪Ab ⟫ ◻ ϕ is in cl(ϕ0 ), then so are ⟪Ab1 ⟫◯⟪Ab2 ⟫ ◻ ϕ for all b1 +∞ b2 = b and also ⟪A0b ⟫◯⟪Ab ⟫ ◻ ϕ • If ⟪Ab ⟫ϕUψ is in cl(ϕ0 ), then so are ⟪Ab1 ⟫◯⟪Ab2 ⟫ϕUψ for all b1 +∞ b2 = b and also ⟪A0b ⟫◯⟪Ab ⟫ϕUψ • If ϕ is in cl(ϕ0 ), then so is ∼ϕ • cl(ϕ0 ) is also closed under finite positively boolean operator (∨ and ∧) up to tautology equivalence. Hence, cl(ϕ0 ) is finite. We denote cl(ϕ0 )◯ to be the set of all formulas of form ⟪Ab ⟫◯ϕ or ¬⟪Ab ⟫◯ϕ in cl(ϕ0 ). Then, the following three lemmas describe each step of the construction of the tree model. We only provide the proof of the last lemma. Lemma 1. Let Φ = {⟪Ab11 ⟫◯ϕ1 , . . . , ⟪Abkk ⟫◯ϕk , ¬⟪Ab ⟫◯ϕ} be a consistent set of formulas where: • All Ai are both non-empty and pair-wise disjoint • ⋃i Ai ⊆ A • ∑i bi ≤ b We have Ψ = {ϕ1 , . . . , ϕk , ∼ϕ} is also consistent. 10 44 Lemma 2. Let Φ = {⟪Ab11 ⟫◯ϕ1 , . . . , ⟪Abkk ⟫◯ϕk , ⟪∅e1 ⟫◯χ1 , . . . , ⟪∅em ⟫◯χm } be a consistent set of formulas where: • All Ai are both non-empty and pair-wise disjoint • ∑i bi ≤ ej for all j We have Ψ = {ϕ1 , . . . , ϕk , χ1 , . . . , χm } is also consistent. We now use the above lemma to construct a simple tree which is locally con- sistent for a consistent set of formulas. Definition 5. A tree (T, V, C) is locally consistent if and only if for any interior node t ∈ T : 1. If ⟪Ab ⟫◯ϕ ∈ V (t), then there is a move σA such that C(t, A, σA ) ≤ b and for any c ∈ out(σA ) we have ϕ ∈ V (c) 2. If ¬⟪Ab ⟫◯ϕ ∈ V (t), then for any move σA with C(t, A, σA ) ≤ b, there exists c ∈ out(σA ) where ∼ϕ ∈ V (c) Lemma 3. Let Φ be a finite consistent set of formulas, Φ◯ the subset of Φ which contains all formulas of the forms ⟪Ab ⟫◯ϕ or their negations from Φ and k some number where ∣Φ◯ ∣ < k, there is a simple k n -costed-tree (T, V, C) which is locally consistent such that V (�) = Φ. Proof. Firstly, we have ¬⟪N b ⟫◯ϕ and ¬⟪∅b ⟫◯ϕ are equivalent to ⟪∅b ⟫◯ ∼ ϕ and ⟪N b ⟫◯ ∼ ϕ, respectively. Therefore, we only consider the case when Φ◯ does not contain formulas of the form ¬⟪N b ⟫◯ϕ and ¬⟪∅b ⟫◯ϕ. Assume that Φ◯ = {⟪Ab11 ⟫◯ϕ1 , . . . , ⟪Abmm ⟫◯ϕm }∪ {¬⟪B1d1 ⟫◯ψ1 , . . . , ¬⟪Bldl ⟫◯ψl }∪ {⟪∅e1 ⟫◯χ1 , . . . , ⟪∅eh ⟫◯χh } where all Ai are non-empty, all Bi are both non-empty and not equal to the grand coalition N . We define a vector max ∈ B where each component of max is the maximal bound except infinity of the corresponding resource appearing in Φ◯ . In the case that there is no maximal bound, then the component of max is set to 0. For example, assume that ∣r∣ = 2 and Φ◯ = {⟪{1, 2}(2,2) ⟫◯p, ⟪{1}(3,∞) ⟫◯p}, then max = (3, 2); in another case, if Φ◯ = {⟪{1}(3,∞) ⟫◯p} then max = (3, 0). Then, we define a function deinf ∶ B∞ → B which removes infinity from a bound as follows: deinf(b) = b′ where for all i = 1, . . . , ∣r∣ (b)i if (b)i =/ ∞ (b′ )i = � maxi +1 otherwise 11 45 Let e be a bound of resources such that e > deinf(ei ) for all i ∈ {1, . . . , h}. We construct a tree with a root labelled by Φ and k n children, each is denoted by c = encode(a1 , . . . , an ) where ai ∈ {1, . . . , k}. Intuitively, we allow each agent i to perform k different actions and the special action k for each agent will be considered as the costless idle-action. We shall denote c(i) = ai for the action performed by agent i with the corresponding outcome c. In the following, we define the labeling function V (c) for each node c and the cost function C(�, i, a) for each agent i and action a ∈ {1, . . . , k}. For each ⟪App ⟫◯ϕp ∈ Φ◯ wherein Ap =/ ∅, ϕp is added to V (c) whenever b c(i) = p for all i ∈ Ap . Let minAp be the smallest number in Ap , we assign the cost of action p performed by minAp to be bp , i.e. C(�, minAp , p) = deinf(bp ). For actions of other agents i in Ap , we assign C(�, i, p) = 0̄. After considering all ⟪App ⟫◯ϕp ∈ Φ◯ , for all other unassigned-cost actions, b i.e. actions a > m but a < k for all agents, we simply set their costs to be e. The action k performed by all agents is defined to associate with the cost 0. We denote C(c) = ∑i∈N C(�, i, c(i)). Then, for each ⟪∅pp ⟫◯χp ∈ Φ◯ , χp is added to V (c) e whenever C(c) ≤ ep . Finally, we will add at most one formula from the negation formulas of Φ◯ to V (c). We denote C(c, A) = ∑i∈A C(�, i, c(i)). For each c, let Φ−◯ (c) = {¬⟪B d ⟫◯ψ ∈ Φ◯ ∣ C(c, B) ≤ d} = {¬⟪Bi1 1 ⟫◯ψi1 , . . . , ¬⟪Billc ⟫◯ψlc } where di d i1 < i2 < . . . < ilc . Let I = {i ∣ m < c(i) ≤ m + lc } and j = ∑i∈I (c(i) − 1 − m) c mod lc + 1. Consider ¬⟪Bij j ⟫◯ψij : if N ∖ Bij ⊆ I, then ∼ψij is added into V (c). di We now need to show that our simple tree is locally consistent. In the first step, we show that all labels are consistent. It is obvious that V (�) = Φ is consistent. Let us firstly consider every child c of the root where ∼ ψq ∈ V (c) from some negation formula in Φ◯ . This will imply that there will be no χ ∈ V (c) from the formulas of the form ⟪∅b ⟫◯χ in Φ◯ . The reason is that because some ∼ ψq ∈ V (c), there must be some agent performing an action a ∈ {m + 1, . . . , m + lc } as otherwise I = ∅ and the condition N ∖ Bij ⊆ I fails since Bij =/ N . We know that the cost of this action is e, then C(c) ≥ e, therefore, no χ will be added into V (c). When there is no ϕ ∈ V (c) from the formulas of the form ⟪Ab ⟫◯ϕ in Φ◯ , the proof is trivial as there is only one ∼ψq ∈ V (c). If there are some ϕp ∈ V (c) where ⟪App ⟫◯ϕp ∈ Φ◯ , then for each p, c(i) = p < m for all i ∈ Ap . Hence, all Ap b are pair-wise disjoint. This simply shows that the set of ⟪App ⟫◯ϕp ∈ Φ◯ where b ϕp ∈ V (c) and ∼⟪Bq q ⟫◯ψq satisfies the conditions of Lemma 1. Therefore, V (c) b is consistent. Now, we consider every child c of the root where there is no ∼ ψ ∈ V (c) from some negation formula in Φ◯ . 12 46 When there is no ϕ ∈ V (c) from the formulas of the form ⟪Ab ⟫◯ϕ in Φ◯ , the proof is trivial as there are only some χq ∈ V (c). If there are some ϕp ∈ V (c) where ⟪App ⟫◯ϕp ∈ Φ◯ and Ap =/ ∅, then for each p, c(i) = p < m for all i ∈ Ap . Hence, b all Ap are pair-wise disjoint. For any χq ∈ V (c) by some ⟪∅eq ⟫◯χq ∈ Φ◯ , we have that eq ≥ C(c) ≥ ∑p bp . This simply shows that the set of ⟪App ⟫◯ϕp ∈ Φ◯ b where ϕp ∈ V (c) and ⟪∅q ⟫◯χq satisfies the conditions of Lemma 2. Therefore, eq V (c) is consistent. Let us now check the conditions of local consistency on the newly built tree. For ⟪App ⟫◯ϕp ∈ Φ◯ , it is straightforward that the move σAp where all agents b in Ap performs action p < m has cost equal to bp and for any c ∈ out(σAp ), ϕp ∈ V (c). For ¬⟪Bp p ⟫◯ψp ∈ Φ◯ and σ being an arbitrary move of agents in Bp of which d cost is at most equal to dp , we will point out an output c ∈ out(σ) where ∼ψ ∈ V (c) and the actions of agents out of Bp are within m + 1 and m + l which always cost e amount of resources. Even though we do not know the exact actions of agents out of Bp , the costs of those unspecified actions are known to be e. Hence, we can determine the set Φ−◯ (c) = {¬⟪Bi1 1 ⟫◯ψi1 , . . . , ¬⟪Bil lc ⟫◯ψilc } as well as lc . It di di c is obvious that ¬⟪Bp p ⟫◯ψp ∈ Φ−◯ (c), then p = ir for some 1 ≤ r ≤ lc . Let σi d be the action performed by agent i in Bp , we define c(i) = σi for all i ∈ Bp . Let I ′ = {i ∈ Bq ∣ m < c(i) ≤ m + lc } and j ′ = ∑i∈I ′ (c(i) − 1 − m)) mod lc . We select an arbitrary i′ ∉ Bp and set c(i′ ) = m + (r − 1 − j ′ ) mod lc + 1. For all other i ∉ Bp , let c(i) = m + 1. Then, we have I = {i ∣ m < c(i) ≤ m + lc } = (N ∖ Bp ) ∪ I ′ . Therefore, ∑i∈I (c(i) − 1 − m) mod lc + 1 = ∑i∈I ′ ∪{i′ } (c(i) − 1 − m) mod lc + 1 = (j ′ + c(i′ ) − 1 − m) mod lc + 1 = (r − 1) mod lc + 1 = r, and N ∖ Bp ⊆ I because I = (N ∖ Bp ) ∪ I ′ . Hence ∼ψp ∈ V (c). Let us consider an example of building such a locally consistent tree. Consider a system of 2 agents, i.e. N = {1, 2}, 1 resource, i.e. ∣r∣ = 1, and the following set Φ� of RB-ATL formulas. Φ� = {⟪11 ⟫◯p, ⟪2∞ ⟫◯(p → q), ¬⟪12 ⟫◯q, ¬⟪22 ⟫◯p, ⟪∅2 ⟫◯(¬q)} It is easy to see that max = 2 and we can pick e = 3. We now construct a simple tree which is locally consistent and the root is labeled by Φ� . As ∣Φ� ∣ = 5, let us consider the number of actions for each agent k = 6. Then, the set of outcomes is O = {(i, j) ∣ 1 ≤ i, j ≤ 6}. Consider the formula ⟪11 ⟫◯p ∈ Φ� , we add to the label of every V ((1, j)) the formula p, for any 1 ≤ j ≤ 6. The cost of action 1 of agent 1 is 1. 13 47 Consider the formula ⟪2∞ ⟫◯(p → q) ∈ Φ� , we add to the label of every V ((i, 2)) the formula p → q, for any 1 ≤ i ≤ 6. The cost of action 2 of agent 2 is max +1 = 3. As we mean the action 6 for both agents to be the idle action, we simply assign the cost 0 for 6 of both agents. Then we assign the cost e = 3 for all cost-unassigned actions of both agents. After this step, we add ¬q to every outcome (i, j) of which the total cost of i and j is no more than 2. We have the assignment of labels V ((i, j)) for every 1 ≤ i, j ≤ 6 so far as in the following table where each column (row) corresponds to an action of agent 1 (2) together with its cost. AC 11 23 33 43 53 60 13 {p} {} {} {} {} {} 2 3 {p, p → q} {p → q} {p → q} {p → q} {p → q} {p → q} 33 {p} {} {} {} {} {} 4 3 {p} {} {} {} {} {} 53 {p} {} {} {} {} {} 6 0 {p, ¬q} {} {} {} {} {¬q} Let us consider the negation formulas in Φ� . We take each outcome into ac- count to decide whether one of the sub-formulas of the negation formulas in Φ� is included in the label of the outcome. We consider the outcome c = (11 , 13 ), then Φ� (c) = {¬⟪12 ⟫◯q}. Then lc = 1, I = {i ∣ 2 < c(i) ≤ 2 + 1} = ∅. Therefore, as N ∖ {1} ⊆/ I, ¬q is not included in V (c). We consider the outcome c = (11 , 33 ), then Φ� (c) = {¬⟪12 ⟫◯q}. Then lc = 1, I = {i ∣ 2 < c(i) ≤ 2 + 1} = {2}. Therefore, as N ∖ {1} ⊆ I, ¬q is included in V (c). We consider the outcome c = (33 , 60 ), then Φ� (c) = {¬⟪22 ⟫◯p}. Then lc = 1, I = {i ∣ 2 < c(i) ≤ 2 + 1} = {1}. Therefore, as N ∖ {2} ⊆ I, ¬p is included in V (c). We can apply the similar argument, and obtain the following table. AC 11 23 33 43 53 60 13 {p} {} {} {} {} {} 2 3 {p, p → q} {p → q} {p → q} {p → q} {p → q} {p → q} 33 {p, ¬q} {} {} {} {} {¬q} 4 3 {p} {} {} {} {} {} 53 {p} {} {} {} {} {} 6 0 {p, ¬q} {} {¬p} {} {} {¬q} In the following, Γ is the finite set of all maximal consistent sets of formulas from cl(ϕ0 ). As cl(ϕ0 ) is finite, Γ is also finite. We extend the construction for satisfying eventuality formulas which are in forms of ⟪Ab ⟫ϕUψ and ⟪Ab ⟫ ◻ ϕ by the following lemma. We also omit the proof. 14 48 Firstly, we say that a formula ⟪Ab ⟫ϕUψ (¬⟪Ab ⟫ ◻ ϕ) is realised from a node t of a Γ-labeled tree (T, V, C) if there exists a strategy (co-strategy) FA such that for all λ ∈ out(t, FA , b) (λ ∈ out(t, FAc , b)), there is some i such that ψ ∈ V (λ[i]) and ϕ ∈ V (λ[j]) for all j ∈ {0, i − 1} (∼ϕ ∈ V (λ[i])). Lemma 4. For each formula ⟪Ab ⟫ϕUψ (¬⟪Ab ⟫ ◻ ϕ) and x ∈ Γ, there is finite Γ-labeled k n -costed-tree (T, V, C) where: • k = ∣cl(ϕ0 )◯ ∣ + 1 • (T, V, C) is locally consistent • V (�) = x • If ⟪Ab ⟫ϕUψ ∈ x (¬⟪Ab ⟫◻ϕ ∈ x) then (T, V, C) realises ⟪Ab ⟫ϕUψ (¬⟪Ab ⟫◻ ϕ)from � Then, the final construction is as follows. For each consistent set x in Γ and an eventual formula ϕ of cl(ϕ0 ), we have a finite tree (Tx,ϕ , Vx,ϕ , Cx,ϕ ) which realises ϕ with the root having label x. Let the eventual formulas in cl(ϕ0 ) be listed as ϕe0 , . . . , ϕem . In the following, we have the definition of the final tree. Definition 6. The final tree (Tϕ0 , Vϕ0 , Cϕ0 ) is constructed inductively as follows. • Initially, select an arbitrary x ∈ Γ such that ϕ0 ∈ x. As that formula is consistent, x must exist. Let (Tx,ϕe0 , Vx,ϕe0 , Cx,ϕe0 ) be the initial tree. • Given the tree constructed so far and the last used eventual formula ϕei . Then, for every leaf labelled by y ∈ Γ of the currently constructed tree, we replace it with the tree (Ty,ϕej , Vy,ϕej , Cy,ϕej ) where j = i + 1 if i < m or j = 0 if otherwise. Let Sϕ0 be the model which is based on (Tϕ0 , Vϕ0 , Cϕ0 ). We have the follow- ing truth lemma which completes the proof of completeness of the axiomatization system for RBATL∞ . The proof of this lemma is omitted in this paper. Lemma 5. For every node t of (Tϕ0 , Vϕ0 , Cϕ0 ) and every formula ϕ ∈ cl(ϕ0 ), if ϕ ∈ Vϕ0 (t) then Sϕ0 , t ⊧ ϕ. 5 Related work and Conclusion The extended logic RBATL∞ is an useful tool which allows us to flexibly express properties in multiagent systems where available amount of resources may affect 15 49 the ability of the agents. Rather than specifying upper-bounds on every resource in a property, we can set up limitation over some resources which are of interest. A sound and complete axiomatization of RBATL∞ is also presented in this paper. Recently, there have been several efforts on logics for expressing resource- bounded properties for multi-agent systems. In [4], the authors extend the tem- poral logic CTL (and CTL∗ ) where agents not only consume but also produce resources. However, such logics only express properties of single agent system. In [1], the authors extend ATL in order to express properties of coalitional abilities of bounded-memory multi-agent systems. The limitation of memory in the logic is set up by restricting the size of strategy mappings and the length of history in each strategy mapping. Both extensions have no axiomatization result. In the future, we will consider the satisfiability and model-checking problem of RBATL∞ . Acknowledgments I gratefully acknowledge Natasha Alechina for supporting and giving me valuable comments and suggestions about the proofs. I also thank anonymous referees for careful reading, corrections and suggestions on the text. References [1] Thomas Ågotnes and Dirk Walther. A logic of strategic ability under bounded memory. Journal of Logic, Language and Information, 18(1):55–77, 2009. [2] Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. Resource-bounded alternating-time temporal logic. In Wiebe van der Hoek, Gal Kaminka, Yves Lesperance, Michael Luck, and Sandip Sen, editors, Pro- ceedings of the Ninth International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, Canada, May 2010. IFAAMAS, IFAAMAS. (to appear). [3] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM (JACM), 49(5):672–713, 2002. [4] Nils Bulling and Berndt Farwer. RTL and RTL∗ : Expressing abilities of resource-bounded agents. In J. Dix, M. Fisher, and P. Novak, editors, Pro- ceedings 10th International Workshop Computational Logic in Multi-Agent Systems, pages 2–19, 2009. 16 50