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.
In previous work [2], we have presented a logic, namely RB-ATL, which allows expressing and reasoning about properties of coalitional ability under resource constraints. 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 bandwidth. 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 network 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 written 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 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 numbers 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:
where p ∈ Φ, A ⊆ N and b ∈ B. Intuitively, ⟪A b ⟫◯ϕ says that the coalition A can co-operate (in one step) to make ϕ true without spending more than b amount of resources. Similarly, ⟪A b ⟫ϕ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 ⟪A b ⟫ ◻ ϕ 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:
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
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
is a mapping to indicate the minimal amount of resources required by each move available to each agent at a specific state.
• δ ∶ Q × N n → 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 sequences of states by Q ω as usual. Let λ = q 0 q 1 . . . ∈ Q ω , we denote λ[i] = q i and λ[i, j] = q i . . . q j . 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 D A (q) to be the set of all moves for A at q. Furthermore, given m ∈ D(q), we denote m A = (m a ) a∈A . Then we define the set of all possible outcomes by a move σ A ∈ D A (q) at a state q as follows
The cost of a move σ A ∈ D A (q) then is defined as cost(q, σ A ) = ∑ a∈A c(q, a, σ a ).
A strategy for a coalition A ⊆ N is a mapping F A which associates each sequence λq ∈ Q + to a move in D A (q). A computation λ ∈ Q ω is consistent with
. We denote by out(q, F A ) the set of all such sequences λ starting from q, i.e.
We denote out(q 0 , F A , b) the set of all such sequences. Then, a strategy F A is a b-strategy iff out(q, F A ) = out(q, F A , b) for any q ∈ Q.
Similarly to the case of moves and strategies, we define a co-move for a coalition A ⊆ N as a mapping σ c A ∶ D A (q) → Q such that σ c A (σ A ) ∈ out(q, σ A ) for any σ A ∈ D A (q). We denote D c A (q) be the set of all co-moves for A at a state 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 ∈ D A (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
Let us define out(q, F c A ) to be the set of all such sequences where q = λ[0]. We say a computa-
) for all j = 0, . . . , i and ∑ j cost(λ[j], σ j A ) ≤ b. Let us denote out(q, F c A , 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 ⊧ ⟪A b ⟫◯ϕ iff there exists a b-strategy F A such that for all λ ∈ out(q, F A ), S, λ[1] ⊧ ϕ iff there is a move σ A ∈ D A (q) such that for all q ′ ∈ out(σ A ), S, q ′ ⊧ ϕ
• S, q ⊧ ¬⟪A b ⟫◯ϕ iff there exists a co-strategy
there is a position i ≥ 0 such that S, λ[i] ⊧ ψ and S, λ[j] ⊧ ψ for all j ∈ {0, . . . , i − 1}
• S, q ⊧ ¬⟪A b ⟫ϕUψ iff there exists a co-strategy F c A such that for all λ ∈ out(q, F A , 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:
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.
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
We denote out(q 0 , F A , b) the set of all such sequences. Then, a strategy F A is a bstrategy iff out(q, F A ) = out(q, F A , 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)
• S, q ⊧ ϕ ∨ ψ iff S, q ⊧ ϕ or S, q ⊧ ψ • S, q ⊧ ϕ ∧ ψ iff S, q ⊧ ϕ and S, q ⊧ ψ • S, q ⊧ ⟪A b ⟫◯ϕ iff there exists a b-strategy F A such that for all λ ∈ out(q, F A ), S, λ[1] ⊧ ϕ. In other words, it is equivalent to say that there is a move σ A ∈ D A (q) such that for all q ′ ∈ out(σ A ), S, q ′ ⊧ ϕ
• S, q ⊧ ¬⟪A b ⟫◯ϕ iff there exists a co-strategy F c A such that for all λ ∈ out(q, F A , b), S, λ [1] ⊧∼ ϕ. In other words, it is equivalent to say that there is a co-move σ c ∈ D c A (q) such that for all σ A ∈ D A (q) and cost(σ A ) ≤ b, S, σ c (σ A ) ⊧∼ϕ
• S, q ⊧ ⟪A b ⟫ϕUψ iff there exists a b-strategy F A such that for all λ ∈ out(q, F A ), there is a position i ≥ 0 such that S, λ[i] ⊧ ψ and S, λ[j] ⊧ ψ for all j ∈ {0, . . . , i − 1}
• S, q ⊧ ¬⟪A b ⟫ϕUψ iff there exists a co-strategy F c A such that for all λ ∈ out(q, F A , 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] ⊧∼ϕ
In this section, we present an axiomatisation system of RBATL ∞ . We first introduce notations appearing in the axiomatisation. In the following, A, A 1 , A
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 resource, 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:
Similar to the reason of introducing + ∞ , we also define a zero bound 0b with respect to a bound b in B ∞ as follows, for all i = 1, . . . , |r| ( 0b
This means we ignore any component which is ∞.
The axiomatisation system of RBATL ∞ is as follows:
Inference rules
Proposition 1. The above axiomatization system for RBATL ∞ is sound and complete.
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 completeness, 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:
Given a tree T , � is the root of T . Nodes of T are elements of T . We define succ ∶ T → 2 T 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 (a 1 , . . . , a n ) where
Where encode ∶ {1, . . . , k} n → {0, . . . , k n − 1} is a bijective function which is defined as
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 a i for all i ∈ {1, . . . , n} and (a 1 , . . . , a n ) = 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.
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, (a 1 , . . . , a n )) = x⋅encode((a 1 , . . . , a n )). It is straightforward that S (T,V,C) is 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. D A (x) = D A (x ′ ) for any x, x ′ ∈ T , hence we shall write Δ A for D A (x).
Notice that when constructing the tree model for a consistent formula, we build k n -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 )
) 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 ⟪A b ⟫◯ϕ or ¬⟪A b ⟫◯ϕ 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 Φ = {⟪A b 1 1 ⟫◯ϕ 1 , . . . , ⟪A b k k ⟫◯ϕ k , ¬⟪A b ⟫◯ϕ} be a consistent set of formulas where:
• All A i are both non-empty and pair-wise disjoint
1 ⟫◯ϕ 1 , . . . , ⟪A b k k ⟫◯ϕ k , ⟪∅ e 1 ⟫◯χ 1 , . . . , ⟪∅ em ⟫◯χ m } be a consistent set of formulas where:
• All A i are both non-empty and pair-wise disjoint • ∑ i b i ≤ e j 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 consistent 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 :
, 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 ⟪A b ⟫◯ϕ or their negations from Φ and k some number where
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
1 ⟫◯ψ 1 , . . . , ¬⟪B d l l ⟫◯ψ l }∪ {⟪∅ e 1 ⟫◯χ 1 , . . . , ⟪∅ e h ⟫◯χ h } where all A i are non-empty, all B i 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|
Let e be a bound of resources such that e > deinf(e i ) for all i ∈ {1, . . . , h}.
We construct a tree with a root labelled by Φ and k n children, each is denoted by c = encode(a 1 , . . . , a n ) where a i ∈ {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) = a i 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 ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ wherein A p / = ∅, ϕ p is added to V (c) whenever c(i) = p for all i ∈ A p . Let min Ap be the smallest number in A p , we assign the cost of action p performed by min Ap to be b p , i.e. C(�, min Ap , p) = deinf(b p ). For actions of other agents i in A p , we assign C(�, i, p) = 0.
After considering all ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ , for all other unassigned-cost actions, 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
Finally, we will add at most one formula from the negation formulas of
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 + l c } as otherwise I = ∅ and the condition N ∖ B i j ⊆ I fails since B i j / = 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 ⟪A b ⟫◯ϕ in Φ ◯ , the proof is trivial as there is only one ∼ψ q ∈ V (c). If there are some ϕ p ∈ V (c) where ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ , then for each p, c(i) = p < m for all i ∈ A p . Hence, all A p are pair-wise disjoint. This simply shows that the set of ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ where ϕ p ∈ V (c) and ∼⟪B bq q ⟫◯ψ q satisfies the conditions of Lemma 1. Therefore, V (c) is consistent. Now, we consider every child c of the root where there is no ∼ ψ ∈ V (c) from some negation formula in Φ ◯ .
When there is no ϕ ∈ V (c) from the formulas of the form ⟪A b ⟫◯ϕ in Φ ◯ , the proof is trivial as there are only some χ q ∈ V (c). If there are some ϕ p ∈ V (c) where ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ and A p / = ∅, then for each p, c(i) = p < m for all i ∈ A p . Hence, all A p are pair-wise disjoint. For any χ q ∈ V (c) by some ⟪∅ eq ⟫◯χ q ∈ Φ ◯ , we have that e q ≥ C(c) ≥ ∑ p b p . This simply shows that the set of ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ where ϕ p ∈ V (c) and ⟪∅ eq q ⟫◯χ q satisfies the conditions of Lemma 2. Therefore, V (c) is consistent.
Let us now check the conditions of local consistency on the newly built tree. For ⟪A bp p ⟫◯ϕ p ∈ Φ ◯ , it is straightforward that the move σ Ap where all agents in A p performs action p < m has cost equal to b p and for any c ∈ out(σ Ap ), ϕ p ∈ V (c).
For ¬⟪B dp p ⟫◯ψ p ∈ Φ ◯ and σ being an arbitrary move of agents in B p of which cost is at most equal to d p , we will point out an output c ∈ out(σ) where ∼ψ ∈ V (c) and the actions of agents out of B p 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 B p , the costs of those unspecified actions are known to be e. Hence, we can determine the set Φ − ◯ (c) = {¬⟪B
i lc ⟫◯ψ i lc } as well as l c . It is obvious that ¬⟪B dp p ⟫◯ψ p ∈ Φ − ◯ (c), then p = i r for some 1 ≤ r ≤ l c . Let σ i be the action performed by agent i in B p , we define c(i) = σ i for all i ∈ B p . Let 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.
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
Consider the formula ⟪1 1 ⟫◯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.
Firstly, we say that a formula ⟪A b ⟫ϕUψ (¬⟪A b ⟫ ◻ ϕ) is realised from a node t of a Γ-labeled tree (T, V, C) if there exists a strategy (co-strategy)
Lemma 4. For each formula ⟪A b ⟫ϕUψ (¬⟪A b ⟫ ◻ ϕ) and x ∈ Γ, there is finite Γ-labeled k n -costed-tree (T, V, C) where:
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 (T x,ϕ , V x,ϕ , C x,ϕ ) which realises ϕ with the root having label x. Let the eventual formulas in cl(ϕ 0 ) be listed as ϕ e 0 , . . . , ϕ e m . 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 (T x,ϕ e 0 , V x,ϕ e 0 , C x,ϕ e 0 ) be the initial tree. • Given the tree constructed so far and the last used eventual formula ϕ e i . Then, for every leaf labelled by y ∈ Γ of the currently constructed tree, we replace it with the tree (T y,ϕ e j , V y,ϕ e j , C y,ϕ e j ) 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 following 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 ⊧ ϕ.
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 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 resourcebounded properties for multi-agent systems. In [4], the authors extend the temporal 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 ∞ .
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.
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
Let us consider the negation formulas in Φ � . We take each outcome into account 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 = (1
We consider the outcome c = (
We consider the outcome c = (3 3 , 6 0 ), then Φ � (c) = {¬⟪2 2 ⟫◯p}. Then
We can apply the similar argument, and obtain the following {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 ⟪A b ⟫ϕUψ and ⟪A b ⟫ ◻ ϕ by the following lemma. We also omit the proof.