=Paper= {{Paper |id=None |storemode=property |title=Coalitional Games with Priced-Resource Agents |pdfUrl=https://ceur-ws.org/Vol-810/paper-s03.pdf |volume=Vol-810 |dblpUrl=https://dblp.org/rec/conf/cilc/MonicaNP11 }} ==Coalitional Games with Priced-Resource Agents== https://ceur-ws.org/Vol-810/paper-s03.pdf

Coalitional Games with Priced-Resource Agents

Dario Della Monica, Margherita Napoli, and Mimmo Parente

Dept. of Computer Science, Università di Salerno, Fisciano (Italy),
{ddellamonica|napoli|parente}@unisa.it

Abstract. Alternating-time Temporal Logic (ATL) and Coalition Logic
(CL) are well-established logical formalisms particularly suitable to model
games between dynamic coalitions of agents (like e.g. the system and the
environment). Recently, the ATL formalism has been extended in order
to take into account boundedness of the resources needed for a task to
be performed. The resulting logic is known as Resource-bounded ATL
(RB-ATL) and has been presented in quite a variety of scenarios. Model
checking RB-ATL in very general setting is usually undecidable. Nev-
ertheless, model checking procedures for semantically or syntactically
restricted versions of RB-ATL have been proposed. In this paper, we an-
alyze the problem of coalitions of agents that need to perform complex
tasks, by using resources with a variable price. We highlight a certain
number of problems and considerations, based on diﬀerent interpreta-
tions of shortage of resources, leading to diﬀerent scenarios.

1 Introduction
Automated veriﬁcation of multi-agent systems is a signiﬁcant topic in the re-
cent literature in artiﬁcial intelligence [1]. The need of modeling this kind of
systems has inspired logical formalisms, the most famous being the Alternating-
time Temporal Logics [4] and the Coalition Logic (CL) [8,9], oriented towards
the description of collective behaviors.
The idea of such logics is that agents can join together in team (or coali-
tions) and share resources to accomplish a task (or reach a goal). In particular,
Alternating-time Temporal Logics have been introduced in [4], where the full
alternating-time temporal language, denoted by ATL∗ , has been presented, along
with two signiﬁcant fragments, namely, ATL and ATL+ .
In [7], Goranko has studied the relationship between the (expressive power
of the) two formalisms. In particular, he has shown that CL can be embedded
into ATL. Anyway, none of the two logics takes into account the boundedness
of the resources. Approaches towards veriﬁcation of multi-agent systems under
resource constraints can be found in [2,3,5]. In [2], Alechina et al. introduce the
logic RBCL, whose language extends the one of CL with explicit representation
of resource bounds. In [3], the same authors propose an analogous extension for
ATL, called RB-ATL, and give a PTIME model checking procedure mostly based

This is a preliminary work. Ideas and concepts presented in this paper have been
investigated more deeply in [6].
on the one for ATL. In [5], Bulling and Farwer introduce the logics RAL and
RAL∗ . The former represents a generalization of Alechina et al.’s RB-ATL, the
latter is ATL∗ extended with resource bounds. The authors study several syntac-
tic and semantic variants of RAL and RAL∗ with respect to the (un)decidability
of the model checking problem. In particular, while previous approaches only
conceive actions consuming resources, they introduce the notion of actions pro-
ducing resources. It turned out that such a new notion makes the model checking
problem undecidable.
The paper is structured as follows. In the next section, we make some consid-
erations about scenarios proposed in the literature, we illustrate our proposals,
and show that the model checking problem is still decidable. Then, in the last
section, we propose new scenarios for which the model checking problem is under
study.

2 Our scenario
This section contains an epistemic discussion about the formalization of a multi-
agent system in which agents can cooperate to perform a task and are subject to
a limited availability of resources, that is an intrinsic feature of any real-world
system. Our discussion hinges on existing approaches in the literature (see e.g.
[2,3,5]) and represents an attempt to do a further step towards the formalization
of such complex systems.
Formulas of the formalisms proposed in [2,3,5] allow one to assign an en-
dowment of resources to the agents by means of the so-called team operators,
(borrowed from ATL) and to state that a team of agents can perform a task.
Due to the nesting of the team operators in a formula (which reﬂects the fact
that coalitions may change in a game), during the execution of the task, the
agents can be provided with a new endowment of resources to perform subtasks.
This is somehow unrealistic, as it does not take into account issues related to
procurement of resources. In particular, a very signiﬁcant present-day issue is
that resources are available on the market (or in nature) in limited amount, and
the cost for achieving them depends on such an availability.
First improvement. Thus, our ﬁrst proposal is to introduce the notion of
price of resources. Unlike the existing approaches, agents are equipped with an
amount of money instead of an endowment of resources. They can use money for
getting resources. Notice that money cannot be considered as a resource like the
others for at least two reasons. First, according to our aim of assigning, to each
resource, a price that is variable depending on several factors (e.g., the current
availability of the resource on the market), it is necessary to introduce the new
component money with the special ability of “measuring” the value of all the
resources, thus making it possible for the agent to acquire them when needed.
Second, since the money as the special ability of “measuring” the value of the
resources makes sense to consider problems of optimization (e.g., minimization
of the amount of money needed to acquire the resources to perform a task).
Formulas of our logic state that a team of agents is able to perform a given
task provided with a given amount of money. We also introduce a notion of
global availability of resources on the market, the intended meaning being that,
whenever an agent acquires resources from the market, the global availability is
decreased, whenever it produces resources, the global availability is increased.
The price of resources can be any function of the several components into play. In
our approach, prices of resources depend on their global availability, the acting
agent, and the physical location.
Second improvement. Another aspect that has not been fully analyzed in the
literature is the problem of actions producing resources. On the one hand, in
[2,3], actions can only consume resources; on the other hand, in [5], the authors
state that whenever actions can produce resources the model checking problem is
undecidable. In this paper, we show how to constrain the way in which actions
can produce resources, still preserving the decidability of the model checking
problem. The idea is that it is possible, at a given time, for an action to pro-
duce a resource in a quantity that is not greater than the amount that has
already been consumed so far. This implies that, even if actions can produce
resources, the global availability of the market will never be greater than the
initial global availability, that is crucial for the model checking algorithm. Such
a notion makes sense as, in practical terms, it allows one to model signiﬁcant
real-world scenarios, such as, acquiring memory by a program, leasing a car dur-
ing a travel, and, in general, any scenario in which an agent is releasing resources
previously acquired.

2.1 Team and task

So far, we have talked about teams (or coalitions) of agents performing a task.
But we have not clariﬁed yet the two notions of team and task. First of all, a
task is a goal that has to be reached and, for what concerns us, is represented by
a logical formula that has to be satisﬁed. A team of agents is a subset of agents
that act collectively in order to perform a task. To this end, they select a strategy
that univocally determines their behavior in each possible conﬁguration of the
system. Nevertheless, the behavior of the remaining agents, that we collectively
denote as the opponent, is undetermined. Aim of the team is to guarantee that
the task is performed independently of the opponent’s behavior, that is, the task
must be guaranteed for each possible opponent’s strategy.
The formalism that naturally ﬁts our intention is the logic ATL, that allows
one to ﬁx a strategy for the agents of a team and to force an ‘LTL-like’ property,
representing the task, to be true over all the possible executions (or outcomes)
of the system. Obviously, its syntax and semantics will be extended in order to
deal with resource constraints.

2.2 The special resource ‘time’

One can be interested in answering questions of the kind “is it possible for the
team A of agents to complete the task in x time-unit?”. It is clear that the
resource ‘time’ neither can be bought nor rented. It is in a certain sense out of
the control of the agents, as it is only possible to specify that a task should be
executed within some given time constraints, while it is not possible to administer
it. Thus, resource ‘time’ will be treated in a special way with respect to other
resources.

2.3 Game structure
A game structure G is based on a graph whose vertices, called locations, are
labeled by atomic propositions. In each location, each agent can choose among a
non-empty set of actions to be performed. Any possible combination of actions
gives rise to transitions, that are the edges of the graph. In general, actions
consume and produce resources. Each resource has a price that is variable and
depends on, inter alia, the current availability of that resource on the market.
Thus, a transition can be executed if the resources needed to perform the actions
are available and each agent has enough money to acquire them.
Let Z denote the set of integers, N denote the set of non-negative integers, and
let M = (N∪{∞})r . A game structure G is a tuple Q, AP, V, Ag, Σ, ∆, R, t, c, ρ,
where:
– Q is the ﬁnite set of locations, AP is the ﬁnite set of propositional letters,
and V : Q → 2AP is the valuation function;
– Ag = {a1 , a2 , . . . , an } is the ﬁnite set of agents, and Σ is the ﬁnite set of
actions, denoted by α1 , α2 , . . .,
– ∆ : Q×Ag → 2Σ is the action function that deﬁnes the possible actions of an
agent in a given location. By an abuse of notation, we use ∆ also to denote
n
the function from Q to 2Σ deﬁned as ∆(q) = ∆(q, a1 ) × . . . × ∆(q, an );
– R = {R1 , . . . , Rr } is the ﬁnite set of resource types. It contains the particular
resource time, denoted by R1 ;
– t : Q×Σ n → Q is the transition function over the set of locations. It is a par-
tial function deﬁned for any pair (q, α1 , . . . , αn ) such that α1 , . . . , αn ∈
∆(q);
– c : Σ × Ag → Zr is the cost function, assigning a cost to each action per-
formed by an agent. A negative cost represents a resource consumption, while
a positive cost represents a resource production;
– ρ : M × Ag × Q → Nr is the price function, denoting the price of each
resource, depending on the current resource availability, the acting agent,
and the current location. Without loss of generality, we can assume the
price of the resource ‘time’ to be always zero, as it is a resource that cannot
be acquired and thus its price is meaningless.

2.4 A logical formalization: PRB-ATL
We now deﬁne the logic Priced RB-ATL (PRB-ATL). The formulae are given by
the following grammar.
ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | A$ ϕ | A$ 2ϕ | A$ ϕUϕ | ∼ b
where p ∈ AP, A ⊆ Ag, ∼∈ {<, ≤, =, ≥, >}, and b ∈ M. Moreover, $ ∈
(N ∪ {∞})n is a vector representing the availability of money of the agents.
For each agent a ∈ Ag, by $a we denote the availability of money for the agent
a. Intuitively, formulae of the kind ∼ b tests the current availability of resources
on the market. Formulae of the kind A$ ψ, with ψ ∈ {ϕ, 2ϕ, ϕUϕ} state
that the team A has a strategy such that, for every action performed by the
opponent (i.e, Ag \ A), ψ is satisﬁed, and such that the total expenses of each
agent a ∈ A is less than or equal to $a . Without loss of generality, we can assume
$a = ∞ for each a ∈ / A.
In order to give the formal semantics we must ﬁrst deﬁne the following no-
tions. From now on, let G be a generic game structure. We extend the sum op-
eration to sum between vectors component-wise. Additionally, we use the usual
component-wise comparison relations between vectors.

Definition 1 (configuration and computation). A conﬁguration of G is a
pair c = q, m
∈ Q × M. A ﬁnite computation (resp., inﬁnite computation)
over G is a finite (resp., infinite) sequence of configurations (of G) π = c1 c2 . . .,
such that, for each i, if ci = qi , m i and ci+1 = qi+1 , mi+1 , then there exists
a
ntransition t(q i , α
) = qi+1 , with α
= α1 , . . . , αn , such that mi+1 = m i +
j=1 c(αj , aj ).

Given a team A, a move of A, denoted αA , is a vector of actions αa , for all
a ∈ A, representing the action performed by the agents of A. To represent the
possible moves of the team A at any location q, we extend the function ∆ with
|A|
the function ∆ˆA : Q → 2Σ representing the Cartesian product of ∆(q, a), for
all a ∈ A.

Definition 2 (strategy). A strategy FA for the team of agents A is a function
which associates, to each finite computation π = c1 c2 . . . cs , with cs = q, m,
a move αA , such that αA ∈ ∆ ˆA (q). A strategy is said to be memoryless if
FA (π) = FA (π ) for each pair of computations π, π such that π = c1 c2 . . . cs ,
π = c1 c2 . . . cs , cs = q, m, .
cs = q, m

In other words, a strategy FA determines the behavior of the agents in the
team A. Anyway, for each move αA (of the team A) and location q ∈ Q, de-
pending on the move of the opponent, there are several possibilities for the next
location. The set including all such possibilities is called the set of outcomes of
the move αA (of the team A) at location q, denoted by out(q, αA ). As a con-
sequence, given an initial location q1 , a strategy FA corresponds to a tree of
computations, called outcomes of the strategy FA from the location q1 and de-
noted by out(q1 , FA ).
Finally, in order to prevent actions producing resources to cause a reim-
bursement of money to the agent, we deﬁne cons : Σ × Ag → Zr in such a way
that cons(α, a) returns the vector obtained from the vector c(α, a) by replac-
ing the positive components with zeros and the negative components with the
corresponding absolute value.
Let π = c1 c2 . . . ∈ out(q0 , FA ), where ci = qi , m
i for all i, be a computation
and let α i = αia a∈Ag be the move performed by the agents at the conﬁguration
ci for all i.

Definition 3 (consistent computations). The computation π is ($, m
1 )-consistent
for a strategy FA if, for each i ≥ 0, 0 ≤ m
i ≤ m
1 , and a ∈ A
i

j , a, qj ) · cons(αja , a) ≤ $a .
ρ(m
j=1

The semantics of the logic can be deﬁned as usual and we omit it here.

2.5 Model checking

The model checking problem consists in verifying whether a formula ϕ is satisﬁed
in a location q of a game structure G, with an initial resource availability m
∈ M.
The algorithm for model checking our logic is mostly based on the one pro-
posed in [4] and used in [3] for model checking, respectively, ATL and its resource-
bounded extension RB-ATL. Roughly speaking, it works by computing, for each
sub-formula ψ of the formula ϕ to be model checked, the set of states in which
ψ holds. The main diﬃculties when dealing with bounds on resources are the
following. First, the set of sub-formulae must be replaced by an extended set of
formulae (see [3]), that includes, for each sub-formula of the form A$ ψ, all

the formulae A$ ψ for each $ < $. Second, the state does not correspond
anymore to the vertices of the game structure, but to conﬁgurations, that is,
pairs q, m
∈ Q × M. Third, during the analysis of the computations over the
game structure, the algorithm must take into account the resource availability
on the market in order to guarantee that in each instant of the computation all
the resources are still available, as well as to be able to compute the current
prices of resources, that depend also on their availability. Finally, it must be
ensured that, even if actions can produce resources, availability of each resource
may not be higher than the initial availability.
Thus, we now state the main result, without showing the proof in this pre-
liminary version. Full details of both the formalization and the algorithm will
appear in a forthcoming paper.
Let M be the greater component appearing in the initial resource availability
vector m.

Theorem 1. The model checking problem for PRB-ATL is decidable in time
O(M r × | ϕ |r+1 × | G |).

3 Discussion

A further line of research in which we intend to investigate is when, given a
formula in our logic, the coalitions are unknown, that is they are not speciﬁed
and we may ask whether, for each nested sub-formula, there exists a team and
a money endowment such that the formula is satisﬁed. More precisely, given
a formula Ψ where Xi$i are the team operators occurring in it, we want
to compute the coalitions Xi such that Ψ is satisﬁed with minimum expense in
terms of both money and resources. Let us notice that if the minimality condition
is not requested, then the problem can be trivially solved.
Another feature we are investigating is when each agent has a price. In this
scenario, in which agents are themselves resources to be acquired to perform the
task, it makes sense to consider the problem of deciding which team is able to
perform the task at the minimum cost.

References
1. Thomas Ågotnes, Wiebe van der Hoek, and Michael Wooldridge. On the logic of
coalitional games. In AAMAS, pages 153–160, 2006.
2. Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. A logic
for coalitions with bounded resources. In Proc. of the 21st International Joint
Conference on Artificial Intelligence, IJCAI ’09, pages 659–664, 2009.
3. Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. Resource-
bounded alternating-time temporal logic. In Proc. of the 9th International Confer-
ence on Autonomous Agents and Multiagent Systems: Volume 1, AAMAS ’10, pages
481–488, 2010.
4. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time tem-
poral logic. Journal of ACM, 49:672–713, September 2002.
5. Nils Bulling and Berndt Farwer. On the (un-)decidability of model checking
resource-bounded agents. In Proc. of the 19th European Conference on Artificial
Intelligence, ECAI ’10, pages 567–572, 2010.
6. D. Della Monica, M. Napoli, and M. Parente. On a Logic for Coalitional Games
with Priced-Resource Agents. Electronic Notes in Theoretical Computer Science
(ENTCS), 278:215–228, 2011. Proc. of the 7th Workshop on Methods for Modalities
(M4M 2011) and the 4th Workshop on Logical Aspects of Multi-Agent Systems
(LAMAS 2011).
7. Valentin Goranko. Coalition games and alternating temporal logics. In Proc. of the
8th Conference on Theoretical Aspects of Rationality and Knowledge, TARK ’01,
pages 259–272, San Francisco, CA, USA, 2001. Morgan Kaufmann Publishers Inc.
8. Marc Pauly. A logical framework for coalitional eﬀectivity in dynamic procedures.
Bulletin of Economic Research, 53(4):305–324, 2001.
9. Marc Pauly. A modal logic for coalitional power in games. Journal of Logic and
Computation, 12(1):149–166, 2002.