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}(
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 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
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: ϕ ∶∶= p ∣ ¬ϕ ∣ ϕ ∨ ψ ∣ ⟪A ⟫◯ϕ ∣ ⟪Ab⟫ϕU ψ ∣ ⟪A ⟫ ◻ ϕ b b b where p ∈ Φ, A ⊆ N and b ∈ B. Intuitively, ⟪A ⟫◯ϕ says that the coalition A can co-operate (in one step) to make ϕ true without spending more than b amount b ϕU ψ means that the coalition A can co-operate (in of resources. Similarly, ⟪A ⟫ many consecutive steps) to eventually make ψ true without spending more than b b amount of resources while keeping ϕ true; and ⟪A ⟫ ◻ ϕ says that the coalition
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 • π ∶ 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.
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.
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.
Given a RB-CGS S = (n, Q, Π, π, d, c, δ), we denote the set of infinite sequences of states by Qω as usual. Let λ = q0q1 . . . ∈ 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 denote 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).
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, i ∑j=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.
tion A ⊆ N as a mapping σAc ∶ DA(q) → Q such that σAc(σA) ∈ out(q, σA) for any σA ∈ DA(q). We denote DAc(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}
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 DAc(q). We say a computation λ ∈ Qω is consistent with FAc iff, for all i ≥ 0, λ[i + 1] ∈ out(λ[i], FAc (λ[0, i])). Let us define 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 σA0 ∈ DA(λ[0]), . . . , σAi ∈ DA(λ[i]) such that λj+1 = FAc (λ[0, j])(σAj) for all j = 0, . . . , i and ∑j cost(λ[j], σAj) ≤ b. Let us denote out(q, FAc , b) be the set of all such sequences where q = λ[0].
induction on the structure of ϕ. We ignore the propositional cases, other cases are listed as follows:
b • S, q ⊧ ⟪A ⟫◯ϕ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA),
S, q′ ⊧ ϕ • S, q ⊧ ¬⟪A ⟫◯ϕ iff there exists a co-strategy FAc such that for all λ ∈ b out(q, FA, b), S, λ[1] ⊧∼ ϕ iff there is a co-move σc ∈ DAc(q) such that for all σA ∈ DA(q) and cost(σA) ≤ b, S, σc(σA) ⊧∼ ϕ
b • S, q ⊧ ⟪A ⟫ ◻ ϕ iff there exists a b-strategy FA for any λ ∈ out(q, FA),
S, λ[i] ⊧ ϕ for all i ≥ 0 • S, q ⊧ ¬⟪A ⟫ ◻ ϕ iff there exists a co-strategy FAc for any λ ∈ out(q, FAc , b), b S, λ[i] ⊧ ϕ for all i ≥ 0 3
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. b where p ∈ Φ, b ∈ B∞ and A ⊆ N . We define the ⟪∅ ⟫◯ modality as the dual one of ⟪N b⟫◯, i.e. ⟪∅ ⟫◯ϕ ≡ ¬⟪N b⟫◯ ∼ ϕ. This modality is to say that a system b 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) i is b-consistent with FA iff, for every i ≥ 0, ∑j=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 bstrategy 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)
b • S, q ⊧ ⟪A ⟫◯ϕ iff there exists a b-strategy FA such that for all λ ∈ out(q, FA),
σA ∈ DA(q) such that for all q′ ∈ out(σA), S, q′ ⊧ ϕ • S, q ⊧ ¬⟪A ⟫◯ϕ iff there exists a co-strategy FAc such that for all λ ∈ b out(q, FA, b), S, λ[1] ⊧∼ ϕ. In other words, it is equivalent to say that there is a co-move σc ∈ DAc(q) such that for all σA ∈ DA(q) and cost(σA) ≤ b, S, σc(σA) ⊧∼ ϕ
b • S, q ⊧ ⟪∅ ⟫◯ϕ iff for every b-strategy FN for all λ ∈ out(q, FA), S, λ[1] ⊧ ϕ
b • S, q ⊧ ¬⟪∅ ⟫◯ϕ iff there is a b-strategy FN such that for all λ ∈ out(q, FN ), S, λ[1] ⊧∼ ϕ
b ϕU ψ iff there exists a co-strategy FAc such that for all λ ∈ • S, q ⊧ ¬⟪A ⟫ 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
In this section, we present an axiomatisation system of RBATL∞. We first introduce 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 = ∞ 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: ⟪¬A⟪Ab⟫b◯⟫◯◻◻ϕϕ==⋁⋀b1b+1∞+∞b2b=2b=⟪bA¬b⟪1A⟫◯b1 ⟫⟪◯Ab⟪2A⟫b◻2 ⟫ϕ◻ ϕ
b ¬⟪A ⟫◯ϕU ψ = ⋀b1+∞b2=b ¬b1⟪A⟫◯b1 ⟪Ab2 ⟪A ⟫b◯ϕU ψ = ⋁b1+∞b2=b⟪Ab1 ⟫◯⟪A⟫ϕb2U⟫ϕψU ψ ⟪∅b⟫b◯ ◻ ϕ = ⋀b1+∞b2=b⟪∅ b⟫1◯⟪∅b2b⟫2 ◻ ϕ ¬⟪∅ ⟫◯ ◻ ϕ = ⋁b1+∞b2=b⟪∅ ⟫◯⟪∅ ⟫ ◻ ϕ
respect to a bound b in B∞ as follows, for all i = 1, . . . , ∣r∣ (0¯b)i = 0 if bi =/ ∞ ∞ otherwise
Axioms
b ( ) ¬⟪A ⟫◯
b (⊺) ⟪A ⟫◯⊺ (PL) Tautologies of Propositional Logic (B) ⟪A ⟫◯ϕ → ⟪Ad⟫◯ϕ
b 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 Inference rules b (⟪A ⟫◯-Monotonicity) (⟪∅b⟫◻-Necessitation) ϕ → ψ ⟪Ab⟫◯ϕ → ⟪Ab⟫◯ψ
ϕ ⟪∅b⟫ ◻ ϕ (⟪Ab⟫◻-Induction) θ → (ϕ ∧ (⟪Ab⟫◯ ◻ ϕ ∨ ⟪A0¯b ⟫◯θ)) θ → ⟪Ab⟫ ◻ ϕ (⟪Ab⟫U -Induction) (ψ ∨ (ϕ ∧ (⟪Ab⟫◯ϕU ψ) ∨ ⟪A0¯b ⟫◯θ))) → θ ⟪Ab⟫ϕU ψ → θ
plete.
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
of Θ by Θ∗ and Θω, respectively.
c ∈ N: • x ∈ T • x ⋅ c′ ∈ T for all 0 ≤ c′ ≤ c
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.
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) = kn for all x ∈ T . Then, a 2Π-labeled tree (T, V ) with a fixed degree kn can be considered as the skeleton of a model for RB-ATL formulas. We call a tree with a fixed degree kn as a kn-tree. Informally, each node of T is considered as a state. tForoxm⋅ kenac−h 1st.aWte exc∈anT n,athmeereeaarcehktnratnrsaintisoitniofnros mto xitstosuxcc⋅ecsbsyoras,tnuapmlee(lya1f,ro..m. ,xan⋅0) where 1. 1 ≤ ai ≤ k 2. encode((a1, . . . , an)) = c Where encode ∶ {1, . . . , k}n → {0, . . . , kn − 1} is a bijective function which is defined as
encode((x1, . . . , xn)) = (x1 − 1)kn−1 + (x2 − 1)kn−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 kn-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.
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 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).
kn-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.
and its children.
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.
b b form ⟪A ⟫◯ϕ or ¬⟪A ⟫◯ϕ in cl(ϕ0).
Lemma 1. Let Φ = {⟪Ab11 ⟫◯ϕ1, . . . , ⟪Abkk ⟫◯ϕk, ¬⟪A ⟫◯ϕ} be a consistent set b 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 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.
Definition 5. A tree (T, V, C) is locally consistent if and only if for any interior node t ∈ T :
b
b
Lemma 3. Let Φ be a finite consistenbt set of formulas, Φ◯ the subset of Φ which contains all formulas of the forms ⟪A ⟫◯ϕ or their negations from Φ and k some number where ∣Φ◯∣ < k, there is a simple kn-costed-tree (T, V, C) which is locally consistent such that V ( ) = Φ.
b b and ⟪N b⟫◯ ∼ ϕ, respectively. Therefore, we only considber the case when Φ◯ does not contain formulas of the form ¬⟪N b⟫◯ϕ and ¬⟪∅ ⟫◯ϕ.
Assume that Φ◯ = {⟪Ab11 ⟫◯ϕ1, . . . , ⟪Abmm ⟫◯ϕm}∪ {¬⟪ Be11 ⟫◯ψ1, . . . , ¬⟪Bldl ⟫◯ψl}∪
d1
{⟪∅ ⟫◯χ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}(
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 = (b)i if (b)i =/ ∞ maxi +1 otherwise 11
We construct a tree with a root labelled by Φ and kn 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 ⟪Abpp ⟫◯ϕp ∈ Φ◯ wherein Ap =/ ∅, ϕp is added to V (c) whenever 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 ⟪Abpp ⟫◯ϕ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 ep C(c) = ∑i∈N C( , i, c(i)). Then, for each ⟪∅p ⟫◯χp ∈ Φ , χp is added to V (c) ◯ whenever C(c) ≤ ep.
to V (c). We denote C(c, A) = ∑i∈A C( , i, c(i)). For each c, let Φ−◯(c) = {¬⟪Bd⟫◯ψ ∈ Φ◯ ∣ C(c, B) ≤ d} = {¬⟪Bid1i1 ⟫◯ψi1 , . . . , ¬⟪Bidllcc ⟫◯ψlc } where i1 < i2 < . . . < ilc . Let I = {i ∣ m < c(i) ≤ m + lc} and j = ∑i∈I (c(i) − 1 − m) mod lc + 1. Consider ¬⟪Bidjij ⟫◯ψij : if N ∖ Bij ⊆ I, then ∼ ψij is added into V (c).
we show that all labels are consistent. It is obvious that V ( ) = Φ is consistent.
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 ∈
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). b
proof is trivial as there is only one ∼ ψq ∈ V (c). If there are some ϕp ∈ V (c) where ⟪Abpp ⟫◯ϕp ∈ Φ◯, then for each p, c(i) = p < m for all i ∈ Ap. Hence, all Ap are pair-wise disjoint. This simply shows that the set of ⟪Abpp ⟫◯ϕp ∈ Φ◯ where ϕp ∈ V (c) and ∼ ⟪Bqbq ⟫◯ψq satisfies the conditions of Lemma 1. Therefore, V (c) is consistent.
some negation formula in Φ . ◯ 12 b
proof is trivial as there are only some χq ∈ V (c). If there are some ϕp ∈ V (c) where a⟪lAlbpApp⟫ ◯arϕeppa∈irΦ-w◯isaenddiAsjopi=/nt∅.,Ftohrenanfyorχeqac∈hVp,(cc)(ib)y=spo m<em⟪f∅oerqa⟫l◯liχ∈qA∈p.ΦH◯e,nwcee, have that eq ≥ C(c) ≥ ∑peqbp. This simply shows that the set of ⟪Abpp ⟫◯ϕp ∈ Φ◯ where ϕp ∈ V (c) and ⟪∅q ⟫◯χq satisfies the conditions of Lemma 2. Therefore,
For ⟪Abpp ⟫◯ϕp ∈ Φ◯, it is straightforward that the move σAp where all agents in Ap performs action p < m has cost equal to bp and for any c ∈ out(σAp ), ϕp ∈ V (c).
For ¬⟪Bpdp ⟫◯ψp ∈ Φ◯ and σ being an arbitrary move of agents in Bp of which 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) = {¬⟪Bid1i1 ⟫◯ψi1 , . . . , ¬⟪Bidliclc ⟫◯ψilc } as well as lc. It is obvious that ¬⟪Bpdp ⟫◯ψp ∈ Φ−◯(c), then p = ir for some 1 ≤ r ≤ lc. Let σi 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).
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 =C{o(ni,sjid)e∣r1th≤eif,ojrm≤u6l}a. ⟪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.
max +1 = 3.
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.
the following table where each column (row) corresponds to an action of agent 1
(
AC 11 23 33 43 53 60 2133 {p, {pp→} q} {p {→} q} {p {→} q} {p {→} q} {p {→} q} {p {→} q} 56430333 {p{{{,ppp¬}}}q} {{{{}}}} {{{{}}}} {{{{}}}} {{{{}}}} {¬{{{}}}q}
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 = W{ie∣ c2o<nsci(die)r ≤th2e +ou1t}co=m{e2c}.=T(h3e3r,e6f0o)re,,thaesnNΦ∖ {(1c)} =⊆ {I¬,¬⟪2q2i⟫s ◯incpl}u.dTedheinn lVc (=c1),. I = {i ∣ 2 < c(i) ≤ 2 + 1} = {1}. Therefore, as N ∖ {2} ⊆ I, ¬p is included in V (c).
AC 11 23 33 43 53 60 2133 {p, {pp→} q} {p {→} q} {p {→} q} {p {→} q} {p {→} q} {p {→} q} 54633033 {{pp{{,,pp¬¬}}qq}} {{{{}}}} {¬{{{}}}p} {{{{}}}} {{{{}}}} {{¬¬{{}}qq}}
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 ⟪A ⟫ ◻ ϕ by b the following lemma. We also omit the proof.
14
b ϕU ψ (¬⟪A ⟫ ◻ ϕ) 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 ψ (¬⟪A ⟫ ◻ ϕ) and x ∈ Γ, there is finite b Γ-labeled kn-costed-tree (T, V, C) where: • k = ∣cl(ϕ0)◯∣ + 1 • (T, V, C) is locally consistent • V ( ) = x • If ⟪Ab⟫ϕU ψ ∈ x (¬⟪A ⟫◻ϕ ∈ x) then (T, V, C) realises ⟪Ab⟫ϕU ψ (¬⟪A ⟫◻ b b ϕ)from
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.
• 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 ϕe. i
replace it with the tree (Ty,ϕje , Vy,ϕje , Cy,ϕje ) where j = i + 1 if i < m or j = 0 if otherwise.
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.
ϕ ∈ Vϕ0 (t) then Sϕ0 , t ⊧ ϕ. 5
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 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.
bounded 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.
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.