=Paper=
{{Paper
|id=None
|storemode=property
|title=An Extension of RB-ATL
|pdfUrl=https://ceur-ws.org/Vol-627/lrba_3.pdf
|volume=Vol-627
|dblpUrl=https://dblp.org/rec/conf/mallow/Nga10
}}
==An Extension of RB-ATL==
https://ceur-ws.org/Vol-627/lrba_3.pdf
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