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. Nevertheless, model checking procedures for semantically or syntactically restricted versions of RB-ATL have been proposed. In this paper, we analyze 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 different interpretations of shortage of resources, leading to different scenarios.
Automated verification of multi-agent systems is a significant topic in the
recent literature in artificial intelligence [
The idea of such logics is that agents can join together in team (or
coalitions) and share resources to accomplish a task (or reach a goal). In particular,
Alternating-time Temporal Logics have been introduced in [
In [
The paper is structured as follows. In the next section, we make some considerations 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
This section contains an epistemic discussion about the formalization of a
multiagent 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.
[
Formulas of the formalisms proposed in [
First improvement. Thus, our first 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
[
So far, we have talked about teams (or coalitions) of agents performing a task. But we have not clarified 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 satisfied. 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 configuration 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 fits our intention is the logic ATL, that allows one to fix 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
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
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 finite set of locations, AP is the finite set of propositional letters, and V : Q → 2AP is the valuation function; – Ag = {a1, a2, . . . , an} is the finite set of agents, and Σ is the finite set of actions, denoted by α1, α2, . . ., – ∆ : Q×Ag → 2Σ is the action function that defines the possible actions of an agent in a given location. By an abuse of notation, we use ∆ also to denote the function from Q to 2Σn defined as ∆ (q) = ∆ (q, a1) × . . . × ∆ (q, an); – R = {R1, . . . , Rr} is the finite 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 partial function defined for any pair (q, α1, . . . , αn ) such that α1, . . . , αn ∈ ∆ (q); – c : Σ × Ag → Zr is the cost function, assigning a cost to each action performed 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
We now define the logic Priced RB-ATL (PRB-ATL). The formulae are given by the following grammar.
ϕ ::= p | ¬ϕ | ϕ ∧ ϕ |
A$ ϕ |
A$ ϕ |
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 ψ ∈ { ϕ, ϕ, ϕU ϕ} state that the team A has a strategy such that, for every action performed by the opponent (i.e, Ag \ A), ψ is satisfied, 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 first define the following notions. From now on, let G be a generic game structure. We extend the sum operation to sum between vectors component-wise. Additionally, we use the usual component-wise comparison relations between vectors.
Definition 1 (configuration and computation). A configuration of G is a pair c = q, m ∈ Q × M. A finite computation (resp., infinite computation) over G is a finite (resp., infinite) sequence of configurations (of G) π = c1c2 . . ., such that, for each i, if ci = qi, mi and ci+1 = qi+1, mi+1 , then there exists a transition t(qi, α) = qi+1, with α = α1, . . . , αn , such that mi+1 = mi + n 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 the function ∆ ˆA : Q → 2Σ|A| 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 π = c1c2 . . . 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 π = c1c2 . . . cs, π = c1c2 . . . 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, depending 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 consequence, 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 denoted by out(q1, FA).
Finally, in order to prevent actions producing resources to cause a reimbursement of money to the agent, we define cons : Σ × Ag → Zr in such a way that cons(α, a) returns the vector obtained from the vector c(α, a) by replacing the positive components with zeros and the negative components with the corresponding absolute value.
Let π = c1c2 . . . ∈ out(q0, FA), where ci = qi, mi for all i, be a computation and let αi = αia a∈Ag be the move performed by the agents at the configuration ci for all i.
for a strategy FA if, for each i ≥ 0, 0 ≤ mi ≤ m1, and a ∈ A i j=1
ρ(mj, a, qj) · cons(αja, a) ≤ $a.
The semantics of the logic can be defined as usual and we omit it here. 2.5
The model checking problem consists in verifying whether a formula ϕ is satisfied 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
proposed in [
Thus, we now state the main result, without showing the proof in this preliminary 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
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 specified and we may ask whether, for each nested sub-formula, there exists a team and a money endowment such that the formula is satisfied. 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 satisfied 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.