Michael Wooldridge

Ulle Endriss
email: ulle.endriss@uva.nl

Sarit Kraus

Jérôme Lang
email: lang@irit.fr

Incentive Engineering for Boolean Games

Boolean games are a natural, compact, and expressive class of logic-based games, in which each player exercises unique control over some set of Boolean variables, and has some logical goal formula that it desires to be achieved. A player's strategy set is the set of all possible valuations that may be made to its variables. A player's goal formula may contain variables controlled by other agents, and in this case, it must reason strategically about how best to assign values to its variables. In the present paper, we consider the possibility of overlaying Boolean games with taxation schemes. A taxation scheme imposes a cost on every possible assignment an agent can make. By designing a taxation scheme appropriately, it is possible to perturb the preferences of agents so that they are rationally incentivised to choose some desirable equilibrium that might not otherwise be chosen, or incentivised to rule out some undesirable equilibria. After formally presenting the model, we explore some issues surrounding it (e.g., the complexity of finding a taxation scheme that implements some desirable outcome), and then discuss possible desirable properties of taxation schemes.

Introduction

The computational aspects of game-theoretic mechanism design have received a great deal of attention over the past decade [START_REF] Nisan | Algorithmic Game Theory[END_REF]. Particular attention has been paid to the Vickrey-Clarke-Groves (VCG) mechanism, which can be used to incentivise rational agents to truthfully report their private preferences in settings such as combinatorial auctions [START_REF] Ephrati | The Clarke tax as a consensus mechanism among automated agents[END_REF][START_REF] Nisan | Algorithmic mechanism design[END_REF]. The key point of interest of the VCG mechanism is that, because it incentivises agents to report their preferences truthfully, it allows us to compute outcomes that maximise social welfare, which would not in general be possible if agents could benefit from misrepresenting their preferences.

Ultimately, the VCG mechanism is a taxation scheme. Taxation schemes are used in human societies for several purposes. First, they are used to incentivise certain desirable behaviours. For example, a government may tax private car ownership with the goal of encouraging the use of environmentally friendly public transport. Second, they are used to raise revenue, typically with the intention that this revenue is then used to fund projects such as education, healthcare, etc. And finally, of course, they may be used for a combination of these purposes. Our aim in the present paper is to study the design of taxation schemes for incentivising behaviours in multiagent systems. It is important to note that our focus in the present paper is not on the design of incentive compatible (truth-telling) mechanisms, and in this key respect, our work differs from the large body of work on computational and algorithmic mechanism design [START_REF] Nisan | Algorithmic Game Theory[END_REF][START_REF] Ephrati | The Clarke tax as a consensus mechanism among automated agents[END_REF][START_REF] Nisan | Algorithmic mechanism design[END_REF]. Rather, our work considers the problem of incentivising agents whose true preferences are known towards certain courses of action. We see our work as complementing the extensive body of work on the VCG mechanism and its variants.

The setting for our study is the domain of Boolean games. Boolean games are a natural, expressive, and compact class of games, based on propositional logic. Boolean games were introduced by Harrenstein et al. [START_REF] Harrenstein | Boolean games[END_REF]. Their computational and logical properties have subsequently been studied by several researchers [START_REF] Harrenstein | Logic in Conflict[END_REF][START_REF] Bonzon | Compact preference representation and Boolean games[END_REF][START_REF] Mavronicolas | Weighted boolean formula games[END_REF][START_REF] Dunne | Cooperative boolean games[END_REF][START_REF] Bonzon | Dependencies between players in boolean games[END_REF][START_REF] Grant | Manipulating boolean games through communication[END_REF][START_REF] Sauro | Dependency in cooperative boolean games[END_REF], and [START_REF] Th | A combination of boolean games with description logics for automated multi-attribute negotiation[END_REF] defines an extension of Boolean games to description logics. In a Boolean game, each agent i is assumed to have a goal, represented as a propositional formula γ i over some set of variables Φ. In addition, each agent i is associated with some subset Φ i of the variables Φ, with the idea being that the variables Φ i are under the unique control of agent i. The choices, or strategies, available to i correspond to all the possible allocations of truth or falsity to the variables Φ i . An agent will try to choose an allocation so as to satisfy its goal γ i . Strategic concerns arise because whether i's goal is in fact satisfied will depend on the choices made by others. While an agent's primary aim is to make choices so that its goal will be achieved, its secondary aim is assumed to be minimising costs. We assume that for every Boolean variable p and every Boolean value b, there is an associated marginal cost, c(p, b), which would be incurred by the player controlling variable p if this player assigned to p the value b.

In the present paper, we introduce the idea of imposing taxation schemes on Boolean games, so that the possible choices an agent can make can be taxed in different ways. Taxation schemes are designed by an agent external to the system known as the principal. The ability to impose taxation schemes enables the principal to perturb the preferences of the players in certain ways: all other things being equal, an agent will prefer to make a choice that minimises his total expense (= marginal costs + taxes). As discussed above, the principal is assumed to be introducing a taxation scheme so as to incentivise agents to achieve a certain outcome; or to incentivise agents to rule out certain outcomes. We represent the outcome that the principal desires to achieve via a propositional logic formula Υ: thus, the idea is that the principal will impose a taxation scheme so that agents are rationally incentivised to make individual choices so as to collectively satisfy the objective Υ. However, a fundamentally important assumption in what follows is that taxes do not give us absolute control over an agent's preferences. To assume that we were able to completely control an agent's preferences by imposing taxes would be unrealistic. For example, suppose your goal is to stay alive: no matter what level of taxes are being proposed, you would surely choose to satisfy this goal rather than otherwise. If we did have complete control over agents' preferences through taxation, then the problems we consider in this paper would indeed be rather trivial. In our setting specifically, it is assumed that no matter what the level of taxes, an agent would still prefer to have its goal achieved than not. This imposes a fundamental limit on the extent to which an agent's preferences can be perturbed by taxation. Such preferences can be qualified as quasi-dichotomous: the agent has a dichotomous utility function induced by her goal, plus a cost associated to her possible variable assignments. Consider the following simple example, intended to illustrate the general setup of Boolean games and the problem we consider in this paper.

Example 1 Suppose we have a game with two players, 1 and 2. There are just three variables in the game: p, q and r. Player 1 controls p, while player 2 controls q and r. For now, we assume all marginal costs are 0. Thus, a player can assign any value it desires to its variables, at no cost. This implies that a player will be indifferent between its choices on the basis of cost: all that a player is concerned about is the satisfaction of its goal. Now, suppose the goal formulae for our players are defined as follows:

player 1: q player 2: q ∨ r Thus player 1 will be satisfied if the game results in an outcome making q true, while player 2 has a slightly weaker goal: he will be satisfied with an outcome that makes formula q ∨ r true. Notice that player 1 is completely dependent on player 2 for the achievement of his goal, in the sense that, for player 1 to have his goal achieved, player 2 must set q = . However, player 2 is not dependent on player 1: he is in the fortunate position of being able to achieve his goal entirely through his own actions, irrespective of what others do. He can either set q = or r = , and his goal will be achieved. What will the players do? Well, in this case, the game can be seen as having a happy outcome: player 2 can set q = , and both agents will get their goal satisfied at no cost. Although we have not yet formally defined the notion, we can informally see that this outcome forms an equilibrium, in the sense that neither player can improve their position by unilaterally choosing to do something else. Now let us change the game a little. Suppose the cost for player 2 of setting q = is 10, while the cost of setting q = ⊥ is 0, and that all other costs in the game remain 0. Here, although player 2 can choose an action that satisfies the goal of player 1, he will not rationally choose it, because it is more expensive. Player 2 would prefer to set r = than to set q = , because this way he would get his goal achieved at no cost. However, by doing so, player 1 is left without his goal being satisfied, and with no way to satisfy his goal. An external principal observes that it is possible to obtain an outcome in which both players get their goal achieved. The principal provides incentives for player 2 so that he will choose the more desirable outcome in which both players get their goal satisfied. The incentives are in the form of taxes: the principal taxes player 2's actions so that setting q = is cheaper than setting r = . Player 2 then chooses rationally, and both players get their goal satisfied. This might seem harsh on player 2, but although he pays taxes that he would not otherwise pay, he still gets his goal achieved. And in fact, as we will see below, there are limits to the kind of behaviour we can incentivise by taxes. In a formal sense, to be defined below, there is nothing we can do that would induce player 2 to set both q and r to ⊥, since this would result in his goal being unsatisfied.

Before proceeding, we should point out the idea of using taxation schemes to manipulate systems is by no means fanciful. In the economics literature, for example, the concept of Tobin taxes has been proposed as a way of stabilising foreign exchange markets [START_REF] Tobin | A proposal for international monetary reform[END_REF]. Proposed by Nobel Laureate James Tobin in 1978, Tobin taxes are intended to provide incentives for foreign exchange traders to avoid excessive speculative transactions, the volume of which seems to have contributed to several crises faced by the international financial markets over the past three decades:

It is increasingly the case that vast quantities of money flow around the global economy on pure speculation, in which the herd instinct often drives speculative waves. Invariably, given the volume of speculative flows, exchange rates overshoot their natural equilibrium, intensifying the distortions created. Such currency movements are a huge destablising force, not just for individual economies but for the global economy as a whole. [27, p.756] Tobin taxes are taxes imposed at the level of individual transactions (also called "spot" taxes). The idea of introducing such taxes is to reduce the incentives for purely speculative transactions, thereby dampening down the overall volume of transactions, and hopefully promoting stability. A key issue in Tobin taxes is what level taxes should be set. Too low and their effect is insufficient; too high and they start to seriously impinge on the economic efficiency of the market [27, p.756]. Although our present work is not concerned with Tobin taxes, there are nevertheless striking parallels between the goals of the work in this paper and the goals of Tobin taxes.

The remainder of this paper is structured as follows:

• We begin in the following section by introducing the key concepts used throughout the remainder of the paper. We start by defining our model of Boolean games. We then define taxation schemes, and using this definition, we introduce preferences, utilities, and Nash equilibria. We then introduce cost-free games. Cost-free games are a simplification of our Boolean game model, which play a useful role in several of our later formal results.

• In section 3, we introduce the implementation problem: the problem of designing a taxation scheme so that, if players then act rationally, they will choose an outcome that satisfies the principal's objective Υ. We introduce two variants of this problem: weak and strong. The weak variant requires that Υ is satisfied in at least one Nash equilibrium, while the strong version requires that Υ is satisfied in all Nash equilibria -and moreover that there is at least one Nash equilibrium. We establish the complexity of the weak implementation problem, and give a purely logical characterisation of positive instances of weak implementation (i.e., situations in which an objective Υ can be weakly implemented). Turning to strong implementation, we again characterise the computational complexity of the problem, and give a logical characterisation of positive instances of the strong implementation problem for an important class of taxation schemes, which we refer to as {0, 1}-taxation schemes.

• In section 4, we consider secondary properties of taxation schemes, relating to social welfare and equity. For example, we consider the problem of implementing Υ while minimising the total tax burden on society.

• In section 5 we study related work, and we conclude in section 6 with a brief discussion and pointers to possible future work.

Although our presentation is self-contained, some understanding of propositional logic, computational complexity [START_REF] Papadimitriou | Computational Complexity[END_REF], and game theory [START_REF] Osborne | A Course in Game Theory[END_REF] would be helpful. Table 1 provides a summary of our main notational conventions.

Boolean Games and Cost-Free Games

In this section, we introduce the game models that we work with throughout the remainder of this paper. We will in fact present two variations of Boolean games. The first model generalises previous models of Boolean games [START_REF] Harrenstein | Boolean games[END_REF][START_REF] Bonzon | Boolean games revisited[END_REF][START_REF] Dunne | Cooperative boolean games[END_REF], in that it explicitly introduces marginal costs for each action. The second model we present is essentially the original model of Boolean games as defined by Harrenstein et al. [START_REF] Harrenstein | Boolean games[END_REF]; there are no costs in this latter model. To distinguish the two frameworks, we will refer to the latter class of games (dichotomous preferences without costs) as cost-free games. Throughout the paper, we make use of classical propositional logic, and for completeness, we thus begin by recalling the technical framework of this logic. First, let B = { , ⊥} be the set of Boolean truth values, with " " being truth and "⊥" being falsity. We will abuse notation a little by using and ⊥ to denote both the syntactic constants for truth and falsity respectively, as well as their semantic counterparts (i.e., the respective truth values). Where b ∈ B, we denote by ¬b the negated value of b (thus if b = then ¬b = ⊥).

Let Φ = {p, q, . . .} be a (finite, fixed, non-empty) vocabulary of Boolean variables, and let L denote the set of (well-formed) formulae of propositional logic over Φ, constructed using the conventional Boolean operators ("∧", "∨", "→", "↔", and "¬"), as well as the truth constants " " and "⊥". We assume a conventional semantic consequence relation "|=" for propositional logic. A valuation is a total function v : Φ → B, assigning truth or falsity to every Boolean variable. We write v |= ϕ to mean that ϕ is true under, or satisfied by, valuation v, where the satisfaction relation "|=" is defined in the standard way. Let V denote the set of all valuations over Φ. We write |= ϕ to mean that ϕ is a tautology, i.e., is satisfied by every valuation. We denote the fact that formulae ϕ, ψ ∈ L are logically equivalent by ϕ ≡ ψ; thus ϕ ≡ ψ means that |= ϕ ↔ ψ. Note that "≡" is a meta-language relation symbol, which should not be confused with the object-language bi-conditional operator "↔".

We also make some use of the framework of Quantified Boolean Formulae (QBFs). QBFs are a well-known extension of propositional logic, which allows for quantification over sets of Boolean variables via expressions ∃X • ϕ and ∀X • ϕ, where X ⊆ Φ is a set of Boolean variables, and ϕ is a formula. The QBF ∃X • ϕ will be true if there is some assignment of values that we

Notation Meaning 2 S
where S is a set, denotes the powerset of S Q the rational numbers

Q ≥ the set {x ∈ Q | x ≥ 0} B = { ,
γ i ∈ L Φ i the Boolean variables under the control of player i ∈ N v i : Φ i → B a choice for player i ∈ N V i the set of all choices for player i ∈ N v = (v 1 , . . . , v n )
an outcome (tuple of choices, one for each player) can give to the variables X such that under this assignment, ϕ is true; the QBF ∀X • ϕ is true if for all assignments of values that we can give to variables X, the formula ϕ is true. We allow nesting of quantifiers. Here is an example of a QBF:

c : Φ × B → Q ≥ a marginal cost function G = N, Φ, c, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n a Boolean game G the set of Boolean games (over N, Φ) τ : Φ × B → Q ≥ a taxation scheme T the set of taxation schemes c i (v i ) the total marginal cost to player i ∈ N of choice v i ∈ V i τ i (v i ) tax levied on player i ∈ N if it chose v i ∈ V i e i (v
∀p • ∃q • [(p ∨ q) ∧ (p ∨ ¬q)] (1)
Formula (1) in fact evaluates to false. (If p is false, there is no value we can give to q that will make the body of the formula true.) Here is another QBF:

∃p • ∀q • [(p ∨ q) ∧ (¬p ∨ ¬q)] (2)
Formula ( 2) is false: whatever value is assigned to p, there is a value that can then be assigned to q so as to falsify the overall formula. We note that the term "QBF" is often understood as referring only to formulae in prenex normal form, i.e., formula of the form

Q 1 x 1 • Q 2 x 2 • • • Q k x k • ϕ(x 1 , . . . , x k )
where each Q i is a quantifier and ϕ(x 1 , . . . , x k ) is a propositional formula (containing no quantifiers) over variables x 1 , . . . , x k . In this paper, we will not require that QBF are in prenex normal form.

Boolean Games

All the games we consider are populated by a set N = {1, . . . , n} of agents -the players of the game. Each agent is assumed to have a goal, characterised by a satisfiable L-formula: we write γ i to denote the goal of agent i ∈ N. The primary aim of a player in a Boolean game is to ensure that their goal is satisfied. Each agent i ∈ N controls a (possibly empty) subset Φ i of the overall set of Boolean variables (cf. [START_REF] Van Der Hoek | On the logic of cooperation and propositional control[END_REF]). By "control", we mean that i has the unique ability within the game to set the value (either or ⊥) of each variable p ∈ Φ i . We will require that Φ 1 , . . . , Φ n forms a partition of Φ, i.e., every variable is controlled by some agent and no variable is controlled by more than one agent: Φ i ∩ Φ j = ∅ for i = j. (Although we do not consider it here, we note that it might be interesting in future work to investigate the possibility of variables being jointly controlled by agents, cf. [START_REF] Gerbrandy | Logics of propositional control[END_REF]).

Where i ∈ N, a choice for agent i is defined by a function v i : Φ i → B, i.e., an allocation of truth or falsity to all the variables under i's control. Let V i denote the set of choices for agent i. Thus V i defines the actions or strategies available to agent i.

An outcome, (v 1 , . . . , v n ) ∈ V 1 × • • • × V n ,
is a collection of choices, one for each agent. We will denote outcomes by v, v 1 , etc. where we do not need to identify or work with their individual components.

Clearly, every outcome v uniquely defines a valuation, and we will often think of outcomes as valuations, for example writing v |= ϕ to mean that the valuation defined by the outcome v satisfies formula ϕ ∈ L. Let ϕ v denote the propositional logic formula that uniquely characterises the outcome v:

ϕ v = ⎛ ⎜ ⎜ ⎝ p∈Φ v|=p p ⎞ ⎟ ⎟ ⎠ ∧ ⎛ ⎜ ⎜ ⎝ q∈Φ v |=q ¬q ⎞ ⎟ ⎟ ⎠
Let fulf ( v) denote the set of agents who have their goal fulfilled by outcome v:

fulf ( v) = {i ∈ N | v |= γ i }.
Intuitively, the actions available to agents correspond to setting variables true or false. We assume that these actions have marginal costs, defined by a cost function:

c : Φ × B → Q ≥ .
Thus c(p, b) is the marginal cost of assigning variable p ∈ Φ the value b ∈ B. Notice that costs are assumed to be positive rational numbers. We use rationals rather than real numbers R simply to avoid the tangential issues of representations for real numbers.

We will say a cost function is uniform if it assigns the same cost to all actions, i.e., if ∃x ∈ Q ≥ such that ∀p ∈ Φ, ∀b ∈ B we have c(p, b) = x. We let c 0 denote the zero cost function, i.e., the uniform function that assigns zero cost to all assignments.

The notion of a cost function represents an obvious generalisation of previous presentations of Boolean games: costs were not considered in the original presentation of Boolean games [START_REF] Harrenstein | Boolean games[END_REF][START_REF] Bonzon | Boolean games revisited[END_REF]; they were introduced by Dunne et al. [START_REF] Dunne | Cooperative boolean games[END_REF], where it was assumed that only the action of setting a variable to would incur a cost (see also [START_REF] Sauro | Dependency in cooperative boolean games[END_REF]). In fact, as we shall see later, costs are, in a limited technical sense, not required in our framework: we can capture the key strategic issues at stake without them. However, it is natural from the point of view of modelling to have costs for actions, and to think about costs as being imposed from within the game, and taxes, (defined below), as being imposed from without.

It may not be obvious at this point why we use costs in our model, so let us pause to reflect on this. Without costs, the only consideration a player has is whether their goal is satisfied or not. Now, suppose a particular player i is in a situation where it believes it has no possibility to get its goal achieved. What should it choose to do? If there are no other factors involved in making this decision other than whether the player's goal is achieved, then it does not matter: any choice for i will be considered equally good. But this does not seem a very realistic reflection of real-world situations. Even an individual's primary goal is not achievable, they will still typically have preferences over their choices; one very natural preference is to minimise costs. By introducing costs in the way that we do here, we can capture such preferences.

As an aside, note that the interpretation of costs that we suggest above (i.e., cost is the marginal cost of an action) is by no means the only interpretation we can give to costs. For example, we may instead interpret costs as being the value required to maintain a variable at some value. However, such interpretations are modelling decisions, and we will not comment on them further here.

Collecting these components together, a Boolean game, G, is given by a structure:

G = N, Φ, c, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n ,
where:

• N = {1, . . . , n} is the set of players;

• Φ = {p, q, . . .} is a finite set of Boolean variables;

• c : Φ × B → Q ≥ is a marginal cost function; • γ i ∈ L is the goal of agent i ∈ N; and
• Φ 1 , . . . , Φ n is a partition of Φ over N, with the intended interpretation that Φ i is the set of Boolean variables under the unique control of i ∈ N.

We will say a game is cost free if it has cost function c 0 .

When playing a Boolean game, the primary aim of an agent i will be to choose an assignment of values for the variables Φ i under its control so as to satisfy its goal γ i . The difficulty is that γ i may contain variables controlled by other agents j = i, who will also be trying to choose values for their variables Φ j so as to get their goals satisfied; their goals in turn may be dependent on the variables Φ i , and so on. For the moment, we will postpone the formal definition of the utility functions and preferences associated with our games. However, intuitively, the idea is that if an agent has multiple ways of bringing about its goal, then it will prefer to choose one that minimises costs; and if an agent cannot get its goal fulfilled, then it simply chooses to minimise costs. Such agents have quasi-dichotomous preferences, or in other terms, lexicographic preferences whose leading criterion is goal satisfaction and whose secondary criterion is the minimization of costs.

Taxation Schemes

A taxation scheme defines additional (imposed) costs on actions, over and above those given by the marginal cost function c. While the cost function c is fixed and immutable for any given Boolean game, an external agent known as the principal is assumed to be at liberty to define a taxation scheme as it sees fit. Agents will seek to minimise their overall expense, and so by assigning different levels of taxation to different actions, the principal can incentivise agents away from performing some actions and towards performing others. The principal is assumed to have an objective that he or she desires to be satisfied. We represent this objective as a propositional formula Υ. If the principal designs the taxation scheme correctly, then agents will be incentivised to choose an outcome v so as to satisfy Υ (i.e., so that v |= Υ).

How exactly should we model taxation schemes? One very general approach would be to levy taxes on the basis of outcomes. We could model such taxes by a function

τ : N × V 1 × • • • × V n → Q ≥
with the intended interpretation that τ (i, v) is the amount of tax that would be imposed on agent i if the outcome v was chosen. However, for the purposes of the present paper, we choose a simpler, additive model of taxes, which is action based rather than outcome based. The idea is that taxes are levied on individual actions, and the total tax imposed on an agent i is the sum of the taxes on individual choices (assignments of truth or falsity to a variable) made in the outcome v i chosen by i.

Formally, we therefore model a taxation scheme as a function

τ : Φ × B → Q ≥
where the intended interpretation is that τ (p, b) is the tax that would be imposed on the agent controlling p if the value b was assigned to the Boolean variable p. The total tax paid by an agent i in choosing a valuation v i ∈ V i will be p∈Φ i τ (p, v i (p)).

To simplify some issues relating to computational complexity we make the additional innocuous assumption the values of taxation schemes can be represented with a space that is bounded by a polynomial in the size of the game (that is, the number of bits needed to represent the control assignment function, the goals, and the the cost function).

We let τ 0 denote the taxation scheme that applies no taxes to any choice, i.e., ∀x ∈ Φ and b ∈ B, τ 0 (x, b) = 0.

We will say τ is a {0, 1}-taxation scheme if for all p ∈ Φ and b ∈ B, we have:

1. τ (p, b) ∈ {0, 1}, and
2. τ (p, b) = 1 -τ (p, ¬b).
Notice that if τ is {0, 1}, then there is exactly one choice for every player that minimises taxes for that player (i.e., the choice where for all variables, the associated tax is 0). Let T denote the set of taxation schemes (over an implicitly assumed game G).

Scenarios

We refer to pairs (G, τ) as scenarios: a scenario is a Boolean game modified by a taxation scheme. We say a scenario

(G, τ) is uniform if ∃x ∈ Q ≥ such that ∀p ∈ Φ, ∀b ∈ B, c(p, b) + τ (p, b) = x.
Note that a scenario can be thought of as inducing a new game, in which taxes are incorporated into the cost function. Formally, let G = N, Φ, c, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n be a Boolean game, and τ be a taxation scheme. Then we can define a new game G τ with cost function c τ defined by

c τ (p, b) = c(p, b) + τ (p, b)
, and all other components of G τ as in G. In this sense, scenarios as pairs (G, τ) are not technically required in the remainder of the paper. Nevertheless, we find it useful to deal with scenarios, as scenarios consider costs (inherent in a game) and taxes (imposed by the principal) as separate entities.

Utilities and Preferences

We will now introduce our formal model of preferences and utilities. What this model aims to capture is that taxation schemes must preserve the quasi-dichotomous nature of preferences:

• an agent prefers all outcomes that satisfy its goal over all those that do not satisfy it;

• between two outcomes that satisfy its goal, an agent prefers the one that minimises total expense (= marginal costs + taxes); and

• between two outcomes that do not satisfy its goal, an agent prefers to minimise total expense.

Examples of such scenarios where agents have dichotomous or pseudo-dichotomous preferences can be found in several previous papers about Boolean games. See for instance Example 2 (kidney exchange) in [START_REF] Bonzon | Effectivity functions and efficient coalitions in boolean games[END_REF]. Likewise, examples of scenarios in robot domains where each robot has a single goal (rescue someone, inspect a location and take pictures, take an object from a location and bring it back) that he should try to reach while minimizing its cost correspond to pseudo-dichtomous preferences.

Notice that taxes play a role in determining an agent's preference relation, but they are not the only factor affecting preferences. An agent's primary concern is to bring about the satisfaction of its goal; expense is a secondary concern. Thus, while taxation schemes can influence the decision making of rational agents, they cannot, ultimately, change the goals of an agent. So, if an agent has a chance to achieve its goal, it will take it, no matter what the taxation incentives are to do otherwise.

Thus the utility an agent i obtains from an outcome v is dependent on three things:

• whether the agent's goal γ i is satisfied by v or not;

• the taxation function τ ; and

• the cost function c.

The cost function and the goals of an agent are given as part of a game, but of course taxation functions are not. It is important to note that the computation of a player's utility cannot be done without a taxation scheme: the utility a player obtains is with respect to a scenario (G, τ) and an outcome v for this scenario. Sometimes, where we want to consider what might happen without a taxation scheme, we will use the zero-cost taxation scheme τ 0 to form a scenario.

To formally define preferences and utilities, we need some more notation. First, with a slight abuse of notation, we extend cost and taxation functions to players and choices as follows:

c i (v i ) = p∈Φ i c(p, v i (p)) τ i (v i ) = p∈Φ i τ (p, v i (p))
So, c i (v i ) is the total marginal cost to player i ∈ N of making choice v i , and τ i (v i ) represents the total tax that would be levied on player i if this player made choice v i . We denote the total expense (= marginal cost + tax) of a choice v i for player i by e i (v i )1 :

e i (v i ) = c i (v i ) + τ i (v i ).
Let v μ i denote the most expensive possible course of action for agent i:

v μ i ∈ arg max v i ∈V i e i (v i ).
Let μ i denote the cost to i of its most expensive course of action:

μ i = e i (v μ i )
Given these definitions, we define the utility to agent i of an outcome (v 1 , . . . , v i , . . . , v n ), as follows:

u i (v 1 , . . . , v i , . . . , v n ) = 1 + μ i -e i (v i ) if (v 1 , . . . , v i , . . . , v n ) |= γ i -e i (v i ) otherwise. (3)
It should be clear that utility for agent i will range from 1 + μ i (the best outcome for i, where it gets its goal fulfilled by performing actions that have no tax or other cost) down to -μ i (where i does not get its goal fulfilled but makes its most expensive choice). An agent will always get utility ≥ 1 if its goal is satisfied in an outcome, and utility ≤ 0 if its goal is not satisfied. Utility functions are defined for the sake of convenience: they provide a convenient numeric representation of preference relations. But note that our framework is purely ordinal: any orderpreserving transformation of our utility functions would work equally well, and the quantitative nature of utility will not play any role in our settings (in particular, utility is not transferable).

Nash Equilibrium

Given this formal definition of utility, we can define solution concepts in the standard gametheoretic way (see, e.g., [START_REF] Osborne | A Course in Game Theory[END_REF]). In this paper, we focus on the concept of (pure) Nash equilibrium. Of course, other solution concepts, such as dominant strategy equilibria, might also be considered, but for simplicity, in this paper we focus on Nash equilibria. We say an outcome

(v 1 , . . . , v i , . . . , v n ) with respect to a scenario (G, τ) is a Nash equilibrium if for each agent i ∈ N, there is no alternative choice v i ∈ V i for i such that u i (v 1 , . . . , v i , . . . , v n ) > u i (v 1 , . . . , v i , . . . , v n ).
We will let NE (G, τ) denote the set of all Nash equilibria of the scenario (G, τ). If we have some outcome v such that v ∈ NE (G, τ) then we say that the outcome v is unstable. An outcome is unstable if some player can benefit by unilaterally deviating from the outcome: the benefit may be either in the form of reduced expense, or in the form of getting a goal fulfilled where it was not otherwise. Where (G, τ) is a scenario and ϕ ∈ L, then we will write NE ϕ (G, τ) to denote the Nash equilibria of (G, τ) that satisfy ϕ:

NE ϕ (G, τ) = { v ∈ NE (G, τ) | v |= ϕ}.
Before proceeding, let us consider some properties of Nash equilibrium outcomes. First, observe that an unsuccessful agent will choose a least-cost course of action in any Nash equilibrium.

Observation 1 If (v * 1 , . . . , v * i , . . . , v * n ) ∈ NE (G, τ) is such that i ∈ fulf (v * 1 , . . . , v * i , . . . , v * n ) then: v * i ∈ arg min v i ∈V i e i (v i ) Proof: Agent i has no choice v i s.t. (v * 1 , . . . , v i , . . . , v * n ) |= γ i , else u i (v * 1 , . . . , v i , . . . , v * n ) > u i (v * 1 , . . . , v * i , . . . , v * n ), in which case (v * 1 , . . . , v * i , . . . , v * n ) ∈ NE (G, τ)
. So, the only way i could profitably deviate would be by making an alternative choice v i that reduced expense compared to v * i . But by definition, v * i minimises i's expense. The following result establishes a sufficient condition for the instability of outcomes; we will use this result later.

Observation 2 Suppose (v 1 , . . . , v i , . . . , v n ) is an outcome for a scenario (G, τ). Then if there is some player i such that i ∈ fulf (v 1 , . . . , v i , . . . , v n ) and ∃v i ∈ V i such that i ∈ fulf (v 1 , . . . , v i , . . . , v n ), then (v 1 , . . . , v i , . . . , v n ) ∈ NE (G, τ). Proof: From (3), we have u i (v 1 , . . . , v i , . . . , v n ) ≤ 0 while u i (v 1 , . . . , v i , . . . , v n ) ≥ 1, so i can benefit by unilaterally deviating from (v 1 , . . . , v i , . . . , v n ).
Notice that this result establishes the instability of an outcome independently of the cost function c and taxation scheme τ of the scenario. These play no part in the choice of the player in this setting: the player will always prefer to unilaterally deviate from an outcome if such deviation results in a goal being fulfilled where it would not otherwise be fulfilled.

The following is an natural decision problem to consider:

NASH VERIFICATION:

Instance: Boolean game G, taxation scheme τ , and outcome v. Question: Is it the case that v ∈ NE (G, τ)?

Proposition 1 NASH VERIFICATION is co-NP-complete.
Proof: Membership is immediate. Hardness is shown by reducing the complement problem (checking that an outcome is not a Nash equilibrium) from SAT. This is the problem of determining whether a given propositional logic formula ϕ is satisfiable, i.e., true under at least one valuation. Given an instance ϕ of SAT over variables x 1 , . . . , x k , define a game G with N = {1}, Φ = Φ 1 = {x 1 , . . . , x k , z} (where z does not occur in ϕ), γ 1 = ϕ ∧ z, and v the valuation that makes all variables false, i.e., v

|= ¬z ∧ ¬x 1 ∧ • • • ∧ ¬x k .
Define all costs and taxes to be 0. Player 1 then has a beneficial deviation from v iff ϕ is satisfiable (in which case the beneficial deviation is to fulfil its goal, making ϕ ∧ z true).

Next, note that while being able to model costs in games explicitly is attractive from a modelling perspective, it is, in a sense, unnecessary from a purely technical point of view: we can always design a taxation scheme that simulates the costs and thus gives rise to the same set of Nash equilibria.

Proposition 2 Let G be a game with cost function c and let τ be a taxation scheme for G. Then there exists a taxation scheme τ such that NE (G, τ) = NE (G , τ ) for the game G we obtain by replacing c with c 0 in G. Moreover, we can show that, for the analysis of Nash equilibria, it suffices to consider taxation schemes that only impose taxes on making a variable true (rather than false). Call a taxation scheme τ positive if τ (p, ⊥) = 0 for all p ∈ Φ. Now consider two zero cost games G and G2 . We call G a variant of G if G is the same as G, except that for some p ∈ Φ all occurrences of p in the agents' goals γ i have been replaced by ¬p (but Υ has not been changed).

Proposition 3 Let G be a zero cost game and let τ be a taxation scheme for that game. Then there exists a variant G of G and a positive taxation scheme τ such that NE (G, τ) = NE (G , τ ).

Proof:

We have to define G and τ with respect to each p ∈ Φ. For all variables p we will have τ (p, ⊥) = 0 (as τ should be positive). So we have to define the values τ (p, ) and we have to specify whether p should occur in the goal formulas in G as in G, or whether p should get flipped (i.e., whether it should get rewritten as ¬p).

1. If τ (p, ) = τ (p, ⊥), then we set τ (p, ) = 0 and we leave p untouched in the game. The crucial feature of this construction is that the difference in tax between making p true or false remains |τ (p, )τ (p, ⊥)| in the new game, and the new taxation scheme still "pushes in the same direction" as before. Therefore, the utility functions for (G , τ ) are identical to those for (G, τ), and thus the Nash equilibria must coincide as well.

Cost-free Games

The model of Boolean games presented above represents the basic model of games that we will work with in this paper. However, we occasionally find it useful to consider a special class of Boolean games which we refer to as cost-free games [START_REF] Harrenstein | Logic in Conflict[END_REF]. A cost-free game is a Boolean game with dichotomous preferences, i.e., with no costs or taxes: a player in a cost-free game is only concerned with whether their goal is satisfied or not. Formally, a cost-free game, H, is given by a structure H = N, Φ, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n with components as in Boolean games, above. Thus, a cost-free game is a Boolean game with no marginal cost function c. Outcomes are defined for cost-free games in exactly the same way as for Boolean games, i.e., an outcome is a tuple of choices, one for each player in the game:

v ∈ V ו • •×V n .
Because no costs or taxes are involved, the definition of utility used for cost-free games is much simpler than that used for our more general model of Boolean games. Formally, (and with a small abuse of notation), the utility for player i ∈ N of an outcome v is denoted by u i ( v), and is defined as follows:

u i ( v) = 1 if v |= γ i 0 otherwise.
With a further abuse of notation, we will write NE (H) to denote the set of Nash equilibria of the cost-free game H.

We will denote by H G the cost-free game obtained from Boolean game G by simply removing the cost function. The following results relate the Nash equilibria of Boolean games and cost-free games, and will be useful later.

Proposition 4

Let G be a Boolean game, and let τ ∈ T be such that scenario (G, τ) is uniform. Then NE (G, τ) = NE (H G ). It follows that for all Boolean games G, there exists a taxation scheme τ ∈ T such that NE (G, τ) = NE (H G ).

Proof:

For each agent i, let u i and u i the utility functions induced respectively by G and (G, τ). Because (G, τ) is uniform, for every i there is a

x i such that c(v i ) + τ (v i ) = x i for all v i ∈ V i . Let v be a valuation. If v |= γ i then u i (v) = u i (v) = 1, and if v |= ¬γ i then u i (v) = -x i whereas u i (v) = 0.
Therefore, for each agent i, u i and u i are comonotonic, from which we conclude that the Nash equilibria of G and (G, τ) coincide. The second item follows immediately.

Proposition 5 For all Boolean games G, and for all τ ∈ T , we have NE (G, τ) ⊆ NE (H G ). Moreover, there exist Boolean games G and taxation schemes τ for which the inclusion is strict.

Proof: For the first part, let G, τ , and H G be as in the statement of the proposition, and suppose v ∈ NE (G, τ). Then no player has a beneficial deviation from v, i.e., no player can unilaterally make an alternative choice that would either reduce costs or lead to the achievement of its goal. But since no player can unilaterally deviate to fulfil its goal, then v ∈ NE (H G ). The second part is immediate: by introducing a taxation scheme, we can eliminate some Nash equilibria.

The Implementation Problem

We now come to the main problems that we consider in the remainder of the paper. Suppose we have an agent, which we will call the principal, who is external to a game G. The principal is at liberty to impose taxation schemes on the game G. The principal will do this for a reason: because it wants to provide incentives for the players in G to choose certain collective outcomes. Specifically, the principal wants to incentivise the players in G to choose rationally a collective outcome that satisfies an objective, which is represented as a propositional formula Υ over the variables Φ of G. We refer to this general problem -trying to find a taxation scheme that will incentivise players to choose rationally a collective outcome that satisfies a propositional formula Υ -as the implementation problem. The implementation problem inherits concepts from the theory of Nash implementation in mechanism design [START_REF] Maskin | The theory of implementation in Nash equilibrium: A survey[END_REF], although our use of Boolean games, taxation schemes, and propositional formulae to represent objectives is quite different.

We define two variants of the implementation problem, as follows:

• In the WEAK IMPLEMENTATION problem, we are given a Boolean game G and an objective Υ, and we are asked whether there exists any taxation scheme τ such that the scenario (G, τ) has at least one Nash equilibrium satisfying Υ.

• In the STRONG IMPLEMENTATION problem, we are given a Boolean game G and an objective Υ, and we are asked whether there exists any taxation scheme τ such that:

1. the scenario (G, τ) has at least one Nash equilibrium; and 2. all Nash equilibria of (G, τ) satisfy Υ.

It is worth noting that the design of a taxation scheme is done by the principal with full knowledge of the game G. In particular, we assume here that the principal knows the goals and possible actions of the players of the game G.

In what follows, we formally define these two variants of the implementation problem, and explore some issues surrounding them.

Weak Implementation

Let WI (G, Υ) denote the set of taxation schemes τ over G such that in the resulting scenario (G, τ), the propositional objective formula Υ is satisfied in at least one Nash equilibrium outcome:

WI (G, Υ) = {τ ∈ T | NE Υ (G, τ) = ∅}.
Given this definition, we can state the first basic decision problem that we consider in the remainder of the paper: WEAK IMPLEMENTATION: Instance: Boolean game G and objective Υ ∈ L. Question: Is it the case that WI (G, Υ) = ∅?

If G, Υ is a positive instance of the WEAK IMPLEMENTATION problem, then we say that Υ can be weakly implemented in G. Let us see an example.

Example 2 Define a game G as follows

: N = {1, 2}, Φ = {p 1 , p 2 }, Φ i = {p i }, γ 1 = p 1 , γ 2 = ¬p 1 ∧ ¬p 2 , c(p 1 , b) = 0 for all b ∈ B,
(v 1 , v 2 ) such that (v 1 , v 2 ) |= p 1 ∧ p 2 , i.e., (v 1 , v 2 ) |= Υ.
Here, agent 2 is not able to get its goal fulfilled, but it can, nevertheless, be incentivised by taxation to make a choice that ensures the achievement of the objective Υ.

So, what objectives Υ can be weakly implemented? At first sight, it might appear that the satisfiability of Υ is a sufficient condition for implementability. Consider the following naive approach for constructing taxation schemes with the aim of implementing satisfiable objectives Υ:

(*) Find a valuation v such that v |= Υ (such a valuation will exist since Υ is satisfiable). Let k be an astronomically large value. Then define a taxation scheme τ such that:

τ (p, b) = 0 if b = v(p) k otherwise.
Thus, the idea is simply to make all choices other than selecting the outcome corresponding to v, which satisfies Υ, too expensive to be rational. In fact, this approach does not work, because of an important subtlety of the definition of utility. In designing a taxation scheme, the principal can perturb an agent's choices between different valuations, but it cannot perturb them in such a way that an agent would prefer an outcome that does not satisfy its goal over an outcome that does: see Observation 2. The following example illustrates the fact that satisfiable objectives cannot always be implemented. So, satisfiability is not a sufficient condition for implementability. But what about tautologies, i.e., objectives Υ such that Υ ≡ ? We might be tempted to assume that tautologies are trivially implementable. This is not in fact the case, however, because for weak implementation, we require that the objective Υ is satisfied in a Nash equilibrium outcome, and it may be that NE (G, τ) = ∅ for all taxation schemes τ . Consider the following example.

Example 4 Define a game

G with N = {1, 2}, Φ = {p, q}, Φ 1 = {p}, Φ 2 = {q}, γ 1 = (p ↔ q), γ 2 = ¬(p ↔ q)
, and c assigns zero cost to all actions. We have NE (G, τ) = ∅ for all taxation schemes τ . This is because for every outcome (v 1 , v 2 ) ∈ V 1 × V 2 some unsuccessful player can deviate to get their goal satisfied. Hence by Observation 2, every outcome is unstable irrespective of the taxation scheme chosen. For example, in the outcome (v 1 , v 2 ) in which v 1 (p) = and v 2 (q) = , agent 2 would benefit by changing its valuation to v 2 (q) = ⊥. (Alert readers will note that this is a Boolean games version of the well-known game of matching pennies.)

Tautologous objectives (i.e., objectives Υ such that Υ ≡ ) might appear to be of little interest, but this is not the case. For suppose we have a game G such that NE (G, τ 0 ) = ∅. Then, in its unmodified condition, before we impose any taxation scheme, this game is unstable: it has no equilibria. Thus, we will refer to the problem of implementing (= checking for the existence of a taxation scheme that would ensure at least one Nash equilibrium outcome), as the STABILISATION problem. The following example illustrates STABILISATION.

Example 5 Let N = {1, 2, 3}, with Φ = {p, q, r}, Φ 1 = {p}, Φ 2 = {q}, Φ 3 = {r}, γ 1 = , γ 2 = (q∧¬p)∨(q ↔ r), γ 3 = (r ∧¬p)∨¬(q ↔ r), c(p, ) = 0, c(p, ⊥) = 1,
and all other costs are 0. For any outcome in which p = ⊥, agent 1 would prefer to set p = , so no such outcome can be stable. So, consider outcomes (v 1 , v 2 , v 3 ) in which p = . Here if (v 1 , v 2 , v 3 ) |= q ↔ r then agent 3 would prefer to deviate, while if (v 1 , v 2 , v 3 ) |= q ↔ r then agent 2 would prefer to deviate. Now, consider a taxation scheme with τ (p, ) = 10 and τ (p, ⊥) = 0 and all other taxes are 0. With this scheme, the outcome in which all variables are set to ⊥ is a Nash equilibrium. Hence this taxation scheme stabilises the system. Now, we know from the work of Bonzon et al. [START_REF] Bonzon | Boolean games revisited[END_REF] that the problem of checking for the existence of pure strategy Nash equilibria in cost-free games is Σ p 2 -complete. It turns out that the WEAK IMPLEMENTATION problem is no harder:

Proposition 6 The STABILISATION problem is Σ p 2 -complete. As a consequence, the WEAK IM- PLEMENTATION problem is also Σ p 2 -complete.
Proof: Membership requires evaluating the following condition:

∃τ ∈ T : ∃ v ∈ V 1 × • • • × V n : [ v ∈ NE (G, τ)].
Notice that checking the inner condition, v ∈ NE (G, τ), is a co-NP problem (Proposition 1), and that the existential quantifiers refer to structures that are of size polynomial in the size of the input. Thus the problem is in Σ p 2 . Hardness follows straightforwardly from the fact that checking for the existence of pure strategy Nash equilibria in cost-free Boolean games is Σ p 2 -complete [3, Proposition 5].

Characterising Weak Implementability

A very natural question to ask is whether we can give a logical characterisation of weak implementability. That is, whether we can obtain a purely logical condition Ψ on games G and objectives Υ (i.e., a condition that depends only on the logical structure of the game, and is independent of taxation schemes and costs), such that Υ can be weakly implemented in G iff property Ψ holds of G and Υ. In this section, we answer this question in the affirmative.

As a warm-up exercise, let us obtain a sufficient condition for weak implementation, as follows. Suppose we can find a valuation that satisfies Υ and the goal of every player i: then the only reason a player would deviate from this valuation would be to reduce costs. But we can eliminate such temptations by fixing the taxation scheme to make any such deviation unprofitable. Formally, we have: Proposition 7 For all games G and objectives Υ ∈ L, if the formula Υ is satisfiable:

Υ = Υ ∧ i∈N γ i then WI (G, Υ) = ∅.
Proof: Assume Υ = Υ ∧ i∈N γ i is satisfiable. Let v be a valuation such that v |= Υ . The basic idea is to use the approach (*), described above, to build a taxation scheme ensuring that the valuation v is a rational choice. For all i ∈ N, p ∈ Φ i and b ∈ B, define:

τ (p, b) = 0 if b = v(p) 1 + k i otherwise.
where k i is the cost of the choice for i that has the highest marginal cost3 ; that is:

k i = max{c i (v i ) | v i ∈ V i }.
Let v be the outcome corresponding to the valuation v. Obviously, v |= Υ. We claim that v ∈ NE (G, τ). For suppose that v is not a Nash equilibrium. Then some agent i can benefit by deviating. Since by construction v |= γ i , then i can only benefit from a choice that would decrease its overall costs. But the construction of τ ensures that any other choice would increase taxes, and hence overall expense, more than any benefit gained by decreasing marginal costs. So, i cannot benefit by changing its choice, and so v is a Nash equilibrium.

We can therefore describe informally our ability to influence behaviour through taxes: we can eliminate through taxation the temptation to deviate from an outcome by reducing costs, but we cannot eliminate the temptation to deviate to get a goal fulfilled. Our characterisation result is thus as follows:

Proposition 8 Let G be a Boolean game and Υ ∈ L be an objective. Then Υ can be weakly implemented in G iff there exists an outcome

(v 1 , . . . , v i , . . . , v n ) ∈ V 1 × • • • × V i × • • • × V n such that: 1. (v 1 , . . . , v i , . . . , v n ) |= Υ; and 2. for every i ∈ fulf (v 1 , . . . , v i , . . . , v n ) there is no v i ∈ V i such that (v 1 , . . . , v i , . . . , v n ) |= γ i .

Proof:

(→) Assume that Υ can be weakly implemented in G, and let τ ∈ T be a taxation scheme that weakly implements Υ. By definition,

∃(v 1 , . . . , v i , . . . , v n ) ∈ NE (G, τ) such that (v 1 , . . . , v i , . . . , v n ) |= Υ. Now suppose for contradiction that ∃i ∈ fulf (v 1 , . . . , v i , . . . , v n ) and ∃v i ∈ V i such that (v 1 , . . . , v i , . . . , v n ) |= γ i . From Observation 2, (v 1 , . . . , v i , . . . , v n ) ∈ NE (G, τ); contradiction. (←) Assume ∃ v = (v 1 , . . . , v i , . . . , v n ) such that v |= Υ and that ∀i ∈ fulf ( v) it is not the case that ∃v i ∈ V i such that (v 1 , . . . , v i , . . . , v n ) |= γ i .
Define a taxation scheme τ as in Proposition 7, so that for every player i, every choice other than choosing v i is strictly more expensive than choosing v i . Then v ∈ NE (G, τ): indeed, assume i has an interest to deviate; since his course of action minimizes the expense (cost + tax) then the only possibility for him to improves his utility is to have v |= ¬γ i and (v 1 , . . . , v i , . . . , v n ) |= γ i , which by assumption is not possible.

Notice that, as in Proposition 2, the condition of Proposition 8 is independent of the cost function c in a scenario. Thus, weak implementability in a Boolean game is equivalent to weak implementability in the induced cost-free game H G : to determine whether Υ can be weakly implemented in G it suffices to determine whether it can be weakly implemented in the cost-free version of G. We obtain: Proposition 9 Let G be a Boolean game and let Υ ∈ L be an objective. Then Υ can be weakly Bonzon et al. were able to give a logical characterisation of the Nash equilibria of (cost free) Boolean games, in terms of the truth of QBFs [6, Proposition 3]. We can adapt this result to give a QBF characterisation of weakly implementable objectives, as follows:

implemented in G iff ∃ v ∈ NE (H G ) such that v |= Υ. Now,
Proposition 10 Let G be a Boolean game and Υ ∈ L be an objective. Then Υ can be weakly implemented in G iff the following QBF is satisfiable:

Υ ∧ i∈N ((∃Φ i • γ i ) → γ i Proof:
The claim follows from Proposition 8. The formula is a direct translation of the two conditions in Proposition 8 into a QBF. The formula is satisfiable iff there exists a valuation that satisfies Υ, and that for that same valuation, it must be the case that any agent who is left unsatisfied by this valuation cannot change her part of the valuation in such a way that the resulting valuation will satisfy her goal.

As an aside, this QBF characterization of weak implementability implies that the complexity of WEAK IMPLEMENTATION can be reduced whenever the complexity of the corresponding QBF problem can be reduced. This holds in particular when all the goals γ i are under Disjunctive Normal Form (DNF). In this case, determining whether ∃Φ i • γ i can be computed in polynomial time, and in this case WEAK IMPLEMENTATION is "only" NP-complete.

Example 6 Suppose we have a game with N = {1, 2, 3}, Φ 1 = {a}, Φ 2 = {b}, Φ 3 = {c}, and

γ 1 = a ∨ b; γ 2 = a ↔ (b ↔ c); γ 3 = (a ∧ ¬b ∧ ¬c) ∨ (¬a ∧ b ∧ c).

Now, we have:

∃Φ 1 • γ 1 = ∃a • a ∨ b ≡ ∃Φ 2 • γ 2 = ∃b • a ↔ (b ↔ c) ≡ ∃Φ 3 • γ 3 = ∃c • (a ∧ ¬b ∧ ¬c) ∨ (¬a ∧ b ∧ c)) ≡ (a ∧ ¬b) ∨ (¬a ∧ b)
We invite the reader to verify that: i

(γ i ∨ ¬∃Φ i .γ i ) ≡ (a ↔ ¬b) ∧ ¬c
And so Υ is weakly implementable if the following formula is satisfiable:

Υ ∧ ((a ↔ ¬b) ∧ ¬c
The logical characterisation of weak implementability given in Proposition 10 shows that WEAK IMPLEMENTABILITY could be solved by a QBF solver.

How Much Taxation Do We Need?

We now show that, if an objective can be implemented, then it can be implemented using only a small amount of taxation. We will first prove a slightly weaker result.

Proposition 11

Let G be a game with a uniform cost function, let Υ ∈ L be an objective, and let ε 1 be any arbitrarily small positive rational number. Then Υ is weakly implementable in G iff Υ can be weakly implemented by a taxation scheme τ such that τ (x, b) ≤ ε for all x, b.

Proof:

(→) Assume τ ∈ WI (G, Υ) and let v = (v 1 , . . . , v n ) ∈ NE (G, τ) be such that v |= Υ. Now,
define a taxation scheme τ * as follows. For each i ∈ N, p ∈ Φ i , and b ∈ B:

τ * (p, b) = ε if v i (p) = b 0 otherwise. We claim that τ * ∈ WI (G, Υ). For consider the outcome (v 1 , . . . , v n ). Since (v 1 , . . . , v n ) ∈ NE (G, τ)
, then from Observation 2, no unsuccessful player i can deviate from v i with an alternative choice v i and thereby achieve goal γ i , so the only possible beneficial deviation for i would be to reduce costs; but the construction of τ * ensures that such a deviation would result in greater taxes for i than choosing v i .

(←) Immediate.

Dependence and Weak Implementation

Example 1 refers to an implicit notion of task exchanges between agents, as in [START_REF] Boella | From social power to social importance[END_REF][START_REF] Grossi | Dependence in games and dependence games[END_REF], or more generally of dependence between agents. In Example 1, for instance, player 1 depends on player 2 for the achievement of her goal. A generalization of this example leads to make the notion of dependence more formal and to exploit it for the weak implementation problem in the following way: if B is a subset of agents; if the agents in B, whatever their internal interdependencies, do not rely on agents outside of B to have their goals achieved, and if their goals form a maximal consistent subset of the set of all goals, then the conjunction of their goals is weakly implementable.

Formally, this calls for a notion of dependence. We reuse the notion of dependence from [START_REF] Bonzon | Dependencies between players in boolean games[END_REF] and [START_REF] Sauro | Dependency in cooperative boolean games[END_REF]: player i depends on player j (for Boolean game G), denoted by iD G j, if some variable controlled by j is relevant to γ i . As in [START_REF] Bonzon | Dependencies between players in boolean games[END_REF] we define a stable set for G as a set B ⊆ N such that for all i ∈ B, every relevant variable for γ i is controlled by an agent in B. Then we have the following result:

Proposition 13 Let G be a Boolean game with costs. If B ⊆ N is stable for G and γ B = {γ i | i ∈ B} is maximal consistent in {γ i | i ∈ N} then γ B is weakly implementable in G. Proof: Assume (1) B ⊆ N is stable for G and (2) γ B = {γ i | i ∈ B} is maximal consistent in {γ i | i ∈ N}. Let v |= γ B (such a v exists because γ B is consistent).
Consider the following taxation function: for all i ∈ B and each variable p controlled by i: if v i |= p then τ (p) = 0 and τ (¬p) = max(0, c(p)c(¬p)) + 1; if v i |= ¬p then τ (¬p) = 0 and τ (p) = max(0, c(¬p)c(p)) + 1; all other taxes are 0. We claim that v is a Nash equilibrium of G + τ . Obviously, no agent in B has an incentive to deviate from v since they have their goal satisfied and pay a zero tax. Suppose an agent i / ∈ B has an interest to deviate from v by playing v i = v i ; let v = (v -i , v i ). Since i pays a zero tax in v, the only reason for him to deviate is to have his goal satisfied in v . Now, since the goals of the agents in B depend only on the variables they control,

v |= γ B implies v |= γ B ; therefore, v |= γ B ∧ γ i , which contradicts the assumption that γ B is maximal consistent in {γ i | i ∈ N}. Therefore v is a Nash equilibrium of G + τ and since s |= γ B , we have shown that γ B is strongly implementable in G.
As a consequence, if γ N is consistent then it is weakly implementable in G -which we knew already from Proposition 9, letting Υ = γ N . More generally, when B = N, B being stable implies that B is powerful enough to have their joint goals achieved -possibly via exchange of favours as in [START_REF] Boella | From social power to social importance[END_REF], but not necessarily.

Note that we need both conditions (1) and ( 2) for the result to hold. Consider the following Boolean G game where (1) is not satisfied: N = {1, 2}, 1 (resp. 2) controls x 1 (resp. x 2 ), γ 1 = x 2 , γ 2 = ¬x 2 ; no costs. {γ 1 } is maximal consistent but not stable; γ 1 is not weakly implementable in G. Consider now the following Boolean game G : N = {1, 2, 3, 4}, i controls x i for i = 1, 2, 3, 4,

γ 1 = x 2 , γ 2 = x 1 , γ 3 = x 3 ↔ x 4 , γ 4 = x 3 ↔ ¬x 4 ; no costs. The set {1, 2} is stable and γ {1,2} is consistent, but not maximal consistent, since {γ 1 , γ 2 , γ 3 } is consistent; G is not stabilisable, a fortiori γ 1 ∧ γ 2 is not weakly implementable in G .

Strong Implementation

The fact that WI (G, Υ) = ∅ is good news for the principal -it says that the principal can impose a taxation scheme such that at least one rational (NE) outcome of the resulting scenario satisfies Υ. However, it could be that there are many Nash equilibria, and only one of them satisfies Υ. If we design taxation schemes appropriately, then we can "steer" players towards outcomes that satisfy Υ in equilibrium, by making other choices too expensive. But nevertheless, the presence of other Nash equilibria, which potentially do not satisfy Υ, is clearly undesirable. This motivates us to consider the strong implementation problem. Strong implementation is similar to the notion of Nash implementation in the mechanism design literature [START_REF] Maskin | The theory of implementation in Nash equilibrium: A survey[END_REF]. With strong implementation, we require not only that the objective Υ is satisfied in some Nash equilibrium outcome, but that it is also satisfied in all equilibrium outcomes.

Let SI (G, Υ) denote the set of taxation schemes τ over G such that:

1. scenario (G, τ) has at least one Nash equilibrium outcome; and 2. all Nash equilibrium outcomes of (G, τ) satisfy Υ.

Formally:

SI (G, Υ) = {τ ∈ T | NE (G, τ) = ∅ & ∀ v ∈ NE (G, τ) : v |= Υ}.
This gives us the following decision problem:

STRONG IMPLEMENTATION:

Instance: Boolean game G and objective Υ ∈ L. Question: Is it the case that SI (G, Υ) = ∅?

It turns out that strong implementation is no harder than weak implementation:

Proposition 14 STRONG IMPLEMENTATION is Σ p 2 -complete.
Proof: Observe that the problem involves evaluating the following condition: is it the case that ∃τ ∈ T : NE (G, τ) = ∅ and ∀ v ∈ NE (G, τ) we have v |= Υ? Expanding out and re-arranging, it can be seen that this is equivalent to asking whether ∃τ ∈ T ,

∃ v ∈ V 1 × • • • × V n , ∀ v ∈ V 1 × • • • × V n , we have v ∈ NE (G, τ) and if v ∈ NE (G, τ) we have v |= Υ. Clearly this is a Σ p 2
predicate. For hardness, we can reduce the STABILISATION problem as in Proposition 6.

How are WI (G, Υ) and SI (G, Υ) related? It turns out that weak and strong implementation are indeed different. It is obvious that for all games G and objectives Υ we have SI (G, Υ) ⊆ WI (G, Υ), but as the following example illustrates, there exist games G and objectives Υ such that WI (G, Υ) ⊆ SI (G, Υ).

Example 7

We give an example of a game and an objective such that the objective can be weakly, but not strongly implemented. Let N = {1, 2}, with Φ = {p, q},

Φ 1 = {p}, Φ 2 = {q}, γ 1 = γ 2 = (p ↔ q)
, with cost function c 0 . Finally, let Υ = p ∧ q. Now, the taxation function τ 0 with zero taxes will weakly implement Υ: there will be two Nash equilibria, one satisfying p ∧ q and the other satisfying ¬(p ∨ q). However, Υ = p ∧ q cannot be strongly implemented, because the outcome satisfying ¬(p ∨ q) will be a Nash equilibrium for all taxation schemes τ . To see this, observe that for it not to be a Nash equilibrium, one agent would benefit by deviating; but by definition of the utility functions, such a deviation would involve an agent moving from positive to negative utility.

Characterising Strong Implementability

Just as we gave a purely logical condition characterising the circumstances under which an objective Υ can be weakly implemented, so we would like to give a logical characterisation of the conditions under which an objective can be strongly implemented. In this section, we give a characterisation result for an important sub-class of the problem: those where the taxation function is {0, 1}. The result requires some more notation and additional intermediate results, and is considerably more involved than the equivalent result for weak implementation. Before presenting the result, we therefore give some intuition behind its structure. Suppose we are given a game G and an objective Υ, and asked whether we can strongly implement Υ in G. In its natural state (i.e., before we impose any taxation scheme), the game G will potentially have some "good" equilibria (i.e., equilibria that satisfy Υ) and some "bad" equilibria (satisfying ¬Υ). What we want to do is find some taxation scheme such that after imposing this scheme, all the bad equilibria are eliminated, while at least one good equilibrium remains. The way we think about this is as follows. By imposing a {0, 1}-taxation scheme on G, we will ensure that some outcome v will have no associated tax, while any choice other than this will start to incur taxes. The outcome v will serve to "tempt" players away from any potentially bad equilibria in the game by ensuring that some player has a beneficial deviation toward v in any potentially bad equilibrium, thus ensuring that such potential bad equilibria are effectively destablised. However, we also require that v does not tempt players away from all "good" equilibria (i.e., satisfying Υ); we need at least one good equilibrium to remain after the taxation scheme is imposed.

First, we have the following readily established result.

Proposition 15

Let G = N, Φ, c, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n , be a Boolean game, let H G be the induced cost-free game, and let Υ ∈ L be an objective. Then Υ can be strongly implemented in G iff it can be strongly implemented in H G .

This result indicates that restricting our attention to cost-free games is not a significant limitation.

Next, where we have a pair of valuations

{v 1 i , v 2 i } ⊆ V i , we denote the distance between v 1 i and v 2 i by δ(v 1 i , v 2 i )
, and define this value as follows:

δ(v 1 i , v 2 i ) = |{v 1 i (x) = v 2 i (x) | x ∈ Φ i }|.
Thus, the distance between two valuations is the number of Boolean variables on whose value the two valuations disagree.

Where

{v 1 i , v 2 i , v 3 i } ⊆ V i , we will write (v 1 i v 2 i v 3 i ) to mean that δ(v 1 i , v 3 i ) ≥ δ(v 2 i , v 3 i ) and (v 1 i v 2 i v 3 i ) to mean that δ(v 1 i , v 3 i ) > δ(v 2 i , v 3 i ).
The key property of this definition is given in the following: Observation 3 Let G be a Boolean game, let τ ∈ T be a {0, 1}-taxation scheme for G, and let v * i ∈ V i be a valuation for some player i in G such that

v * i = arg min v i ∈V i τ i (v i ). Then τ i (v i ) = |{p ∈ Φ i | v i (p) = v * i (p)
}| and for all v 2 , v 3 ∈ V i , we have:

(v 2 i v 3 i v * i ) iff τ i (v 2 i ) > τ i (v 3 i ) ≥ τ i (v * i ).
Observation 3 establishes a link between valuations and taxation functions. Specifically, to compute the amount of tax that i incurs in a choice v i ∈ V i , it suffices to count the number of variables on whose value v i disagrees with the least-cost choice v * i . This link that allows us to establish our characterisation result:

Proposition 16 Let G be a Boolean game with zero cost function and let Υ ∈ L be an objective. Then Υ can be strongly implemented in G with a {0, 1}-taxation scheme iff the following condition on G is satisfied:

∃ v : NoBad( v) & SomeGood( v).
where:

NoBad(v 1 , . . . , v i , . . . , v n ) ≡ ∀(v 1 1 , . . . , v 1 i , . . . , v 1 n ) ∈ NE ¬Υ (H G ) : ∃i ∈ N : ∃v 2 i ∈ V i : (v 1 i v 2 i v i ) & [(v 1 1 , . . . , v 1 i , . . . , v 1 n ) |= γ i ↔ (v 1 1 , . . . , v 2 i , . . . , v 1 n ) |= γ i )] and SomeGood(v 1 , . . . , v i , . . . , v n ) ≡ ∃(v 3 1 , . . . , v 3 i , . . . , v 3 n ) ∈ NE Υ (H G ) : ∀i ∈ N : ∀v 4 i ∈ V i : (v 3 i v 4 i v i ) → ¬[(v 3 1 , . . . , v 3 i , . . . , v 3 n ) |= γ i ↔ (v 3 1 , . . . , v 4 i , . . . , v 3 n ) |= γ i )].
Proof: First note that since the game G in the problem instance has zero costs, the only beneficial deviations for a player can be to either get their goal achieved where it would not otherwise be, or to reduce taxes.

(←) Assume the condition on G holds: we show that this implies Υ can be strongly implemented in G. Let v = (v 1 , . . . , v i , . . . , v n ) be the witness to the outermost existential quantifier. Now, we define a taxation scheme τ that "fixes" the property ϕ (v 1 ,...,vn) , by making all choices other than (v 1 , . . . , v n ) more expensive (cf. the construction in Proposition 8). Formally:

τ (p, b) = 0 if b = v(p) 1 otherwise.
We will first show that no Nash equilibrium of NE (G, τ) satisfies ¬Υ. For suppose that such a Nash equilibrium existed; call it (v 5 1 , . . . , v 5 n ). Then from Proposition 5, (v 5 1 , . . . , v 5 n ) ∈ NE (H G ), and then from the NoBad predicate, we have ∃i ∈ N,

∃v 2 i ∈ V i : (v 5 i v 2 i v i ) such that [(v 5 1 , . . . , v 5 i , . . . , v 5 n ) |= γ i ↔ (v 5 1 , . . . , v 2 i , . . . , v 5 n ) |= γ i )]
. But then player i can benefit from choosing v 2 i instead of v 5 i , since in doing so, this would not change the status of his goal, but he would strictly reduce taxes (Observation 3). But then since some player has a beneficial deviation, then (v 5 1 , . . . , v 5 n ) ∈ NE (G, τ). Hence no equilibrium of (G, τ) satisfies ¬Υ.

It remains to show that some equilibrium of (G, τ) satisfies Υ. For this, consider the SomeGood predicate; take an outcome (v 3 1 , . . . , v 3 n ) satisfying the conditions of the predicate. We claim that (v 3 1 , . . . , v 3 n ) ∈ NE (G, τ). For suppose not; then some player has a beneficial deviation from

(v 3 1 , . . . , v 3 n ). Since (v 3 1 , . . . , v 3 n ) ∈ NE Υ (H G )
, no player can beneficially deviate to get their goal satisfied: the only beneficial deviation could be to reduce taxes. A beneficial deviation v 4 i reducing taxes for player i must satisfy (v

3 i v 4 i v i ). But then from the SomeGood condition, (v 3 1 , . . . , v 4 i , . . . , v 3 n ) |= γ i while (v 3 1 , . . . , v 3 i , . . . , v 3 n ) |= γ i ; but in this case, v 4
i cannot be a beneficial deviation for i, since its goal would be unsatisfied if it chose v 4 i . We conclude that no player has a beneficial deviation from

(v 3 1 , . . . , v 3 n ) i.e., that (v 3 1 , . . . , v 3 n ) ∈ NE Υ (G, τ). It follows that τ strongly implements Υ in G.
(→) Assume that Υ can be strongly implemented in G with a {0, 1}-taxation scheme, but that the condition on games is false. Let τ be a {0, 1}-taxation scheme that strongly implements Υ. Since the condition on games is false, then ∀(v 1 , . . . , v i , . . . ,

v n ) ∈ V 1 ו • •×V i ו • •×V n
one of the following conditions holds:

(C1) ∃(v 1 1 , . . . , v 1 i , . . . , v 1 n ) ∈ NE ¬Υ (H G ) : ∀i ∈ N : ∀v 2 i ∈ V i : (v 1 i v 2 i v i ) → ¬[(v 1 1 , . . . , v 1 i , . . . , v 1 n ) |= γ i ↔ (v 1 1 , . . . , v 2 i , . . . , v 1 n ) |= γ i )] or (C2) ∀(v 3 1 , . . . , v 3 i , . . . , v 3 n ) ∈ NE Υ (H G ) : ∃i ∈ N : ∃v 4 i ∈ V i : (v 3 i v 4 i v i ) ∧ [(v 3 1 , . . . , v 3 i , . . . , v 3 n ) |= γ i ↔ (v 3 1 , . . . , v 4 i , . . . , v 3 n ) |= γ i )].
Obviously, C1 is the negation of NoBad, while C2 is the negation of SomeGood. Now, consider the case where the universally quantified outcome (v 1 , . . . , v i , . . . , v n ) is such that for all i ∈ N we have

v i = arg min v i ∈V i τ i (v i ).
Since τ is {0, 1}, this outcome is unique. We reason by cases:

general, be multiple possible taxation schemes that incentivise the agents in this way, and not all of these taxation schemes will be equally desirable. For example, imposing very high taxes might be undesirable if the same objective can be achieved with smaller taxes. In this section, therefore, we consider different secondary criteria that might be considered by a principal when choosing a taxation scheme; these criteria are secondary because we assume the primary aim of the principal is to ensure the satisfaction of the objective Υ. Our discussion here is somewhat inspired by the literature on welfare economics (see, e.g., [START_REF] Moulin | Axioms of Cooperative Decision Making[END_REF]). We focus on the notions of social welfare and equity.

The general approach we will take is as follows. We assume the principal has some social welfare measure, represented by a function:

f : G × T × V 1 × • • • × V n → Q.
Thus, given a Boolean game G, taxation scheme τ , and outcome v, a social welfare measure f gives a value f (G, τ, v), indicating how good the outcome is according to some social metric. We will assume that the aim is to maximise this function, so larger values of f are preferable. Now, in general, a scenario (G, τ) will have multiple possible outcomes (i.e., multiple possible Nash equilibria). How do we apply the function f (which evaluates individual outcomes) to such situations? The approach we adopt is by now relatively standard: we consider the value of the worst Nash equilibrium [START_REF] Koutsoupias | Worst-case equilibria[END_REF]. Formally, where f is a social welfare measure as above, then we define a two place function f (G, τ), which gives the value of the worst Nash equilibrium of scenario (G, τ) according to f :

f (G, τ) = min{f (G, τ, v) | v ∈ NE (G, τ)} if NE (G, τ) = ∅ -∞ otherwise.
Given a game G, an objective Υ, and a social welfare measure f , an optimal taxation scheme will be a taxation scheme τ * (G, Υ, f ) that has the following properties:

1. τ * (G, Υ, f ) weakly implements Υ in G;

2. τ * (G, Υ, f ) maximises the value of f over all the taxation schemes satisfying [START_REF] Bachrach | The cost of stability in coalitional games[END_REF].

If WI (G, Υ) = ∅, then of course the optimal taxation scheme τ * (G, Υ, f ) is undefined. Formally, given a game G, objective Υ, and social welfare measure f , an optimal taxation scheme τ * (G, Υ, f ) is defined if WI (G, Υ) = ∅, in which case it satisfies:

τ * (G, Υ, f ) ∈ arg max τ ∈WI(G,Υ) f (G, τ).
In the subsections that follow, we will discuss several possible social welfare measures for our setting.

Social Welfare

An obvious first social welfare measure would seem to be the well-known concept of utilitarian social welfare. Utilitarian social welfare is conventionally defined as the sum of the utilities of players in an outcome. However, there is a difficulty when we try to consider utilitarian social welfare in our setting; namely, that utility functions u i (• • •) are defined with respect not just to games G but also with respect to taxation functions, τ . Thus, utilitarian social welfare is, in our settings, somewhat less straightforward then for many other settings. Instead, we will here define a qualitative version of social welfare: the social welfare measure qsw simply counts the number of agents that have their goal fulfilled in a particular outcome:

qsw(G, τ, v) = |{i ∈ N | v |= γ i }|.
Thus, an optimal taxation scheme τ * (G, Υ, qsw) according to this measure will be one that maximises the number of players that have their goal satisfied in the worst case Nash equilibrium.

Another obvious alternative to measuring social welfare is to consider developing a taxation scheme that implements objective Υ while imposing the lowest possible tax burden on society. Broadly, we can think of this approach as minimising the degree of intervention of the principal in the operation of society. Above, we defined the problem of constructing an optimal taxation scheme as a maximisation problem; we therefore express the problem of minimising tax as a maximisation problem. We thus define the social welfare measure tb as follows:

tb(G, τ, (v 1 , . . . , v n )) = - i∈N τ i (v i ).
Thus a taxation scheme τ * (G, Υ, tb), where it exists, will be one that weakly implements Υ in G, while minimising the amount of tax paid in the worst case Nash equilibrium.

It is easy to construct examples showing that minimising the total tax burden may result in outcomes that are undesirable when measured against the social welfare measure qsw, which we considered earlier. But nevertheless, it seems such "least intervention" approaches seem to be relatively popular in human societies.

Equity

It is, of course, well-known that an outcome which maximises (for example) utilitarian social welfare may in fact be extremely undesirable from the point of view of the majority of agents in a system. For example, the social welfare maximising outcome might allocate all the utility in the system to one agent, leaving all others with none. This motivates us to consider a range of possible other notions of equity with respect to taxation schemes, inspired to some extent by the economics literature on taxation [START_REF] Cordes | Horizontal equity[END_REF].

One very obvious (although arguably naive) notion of taxation equity is to simply try to ensure that agents are taxed at broadly the same level, i.e., to minimise the maximum difference in taxes levied on different agents. Formally, the social welfare measure md is defined as follows:

md(v 1 , . . . , v n ) = -max{τ i (v i ) -τ j (v j ) | {i, j} ⊆ N}
Simply aiming to apply the same level of taxes across an entire society may appear to be equitable, but on closer examination, it has some definite drawbacks. In particular, it does not distinguish between agents that have their goals achieved and those that do not. In the literature on taxation, the term horizontal equity is used to describe the idea that those in the same circumstances should be taxed at the same level [START_REF] Cordes | Horizontal equity[END_REF]. One could formalise this notion in several different ways for our model, but we will focus on the following idea: in any outcome, we have two "classes" of agents: those that get their goal achieved and those that do not. Thus, when looking at the differences in taxes paid, we should only compare the taxes of agents that get their goal achieved against other agents that get their goal achieved, and we should only compare agents that do not get their goal achieved against agents that likewise do not get their goal achieved. The social welfare measure he will attempt to ensure that the difference in taxes paid by two agents in the same class is minimised:

he(v 1 , . . . , v n ) = -max({τ i (v i ) -τ j (v j ) | {i, j} ⊆ N & (v 1 , . . . , v n ) |= γ i ∧ γ j } ∪ {τ i (v i ) -τ j (v j ) | {i, j} ⊆ N & (v 1 , . . . , v n ) |= ¬(γ i ∨ γ j )})

Related Work

We now discuss how our work stands in relation to other work, both in game theory and in the multi-agent systems/algorithmic game theory community. First, our work is very closely related to the research area known as implementation in game theory. The basic idea of implementation theory is that we start with a set of outcomes that we want to obtain, and we design a game so that the outcomes will result if the players in the game act rationally. We will first recall the general setting of implementation theory, and then discuss the relationship to the present paper. To keep the presentation straightforward, we will simplify the technical definitions somewhat: see [24, pp.178-180] for a more rigorous formal introduction.

We assume there is a set of game outcomes Ω, a set of players N, (as in our setting), and for each player i ∈ N a set Ac i of strategies/choices. Let A = Ac 1 × • • • × Ac n be the set of action profiles; we denote members of A by a, a , etc. A game form is then a function

g : A → Ω.
Let Γ be a set of game forms. A preference relation for player i is an ordering of outcomes Ω; a collection of preference relations, one for each player, is a preference profile. We denote preference profiles by , 1 , etc. Let P be the set of preference profiles over N, Ω. The components N, Ω, P, Γ are together called an environment.

A solution concept is modelled as a function S : Γ × P → 2 A which for every game form g ∈ Γ and preference profile ∈ P define the set of action profiles S(g, ) that may be the result of the game according to the solution concept S. Now, in implementation theory, a principal is assumed to have an objective defined by a choice rule, f , which associates a set of desirable outcomes f ( ) with every preference profile :

f : P → 2 Ω .
We then say a game form g ∈ Γ S-implements the choice function f if for every preference profile ∈ P we have {g( a) | a ∈ S(g, )} = f ( ).

In other words, the game form g S-implements the choice function f if for every preference profile ∈ P, the outcomes that could result according to solution concept S for the game form g and preference profile coincide with the ones that the principal would choose for this preference profile, according to the choice rule f . We could relax the equality constraint in the last equation, of course, by simply requiring that:

{g( a) | a ∈ S(g, )} ⊆ f ( ).
Expressed as a decision problem, implementation can then be understood as follows:

Given:

• an environment N, Ω, P, Γ ,

• a solution concept S : Γ × P → 2 Ω , and • a choice rule f : P → 2 Ω does there exist a game form g ∈ Γ such that for all preference profiles ∈ P, we have {g( a) | a ∈ S(g, )} = f ( )?

It should be immediately clear that the problems we are studying in the present paper are closely related to implementation problems in the sense we have just described:

• In implementation theory, preferences are given by preference relations i over outcomes.

In our model, first, we make a domain restriction (preference relations are pseudo-dichotomous) and second, we use a compact representation (preferences are defined primarily by goals γ i , expressed as propositional formulae, and secondarily by marginal costs and taxes).

• The actions Ac i in implementation theory correspond to our choices V i . However, in implementation theory, the selection of a set of actions is under the control of the principal, whereas we are assuming this valuations are implicitly fixed as part of the setting.

• In implementation theory, the choice rule f can be understood as playing the role of our objective formula Υ.

• The game forms Γ that the principal may select from in implementation theory correspond to the set T of taxation schemes that we consider in our work. That is, in implementation theory, the principal selects a game form from Γ in order to implement a choice rule f , while in our setting, the principal selects a taxation scheme from T in order to implement an objective Υ. However, in our setting the principal selects a taxation scheme while knowing the goals of players, whereas in implementation theory, a game form is selected by a principal that must induce the choice function for all preference profiles. In addition, in our setting, by selecting a taxation scheme, the principal is able to perturb the preferences of the players, while the "game form" remains unchanged.

One important sub-field of implementation theory is concerned with settings in which the preference relations of players are private (i.e., known only to the players themselves), and the actions of a player corresponds to the declaration of a preference relation by that player. Now, in such a setting, a player can in principle report any preference relation they choose: nothing obliges them to report their own actual private preferences. In this case, one can consider incentive compatible mechanisms: those in which a player is rationally motivated to report their true preference relation. The most important class of incentive compatible mechanisms studied in the literature are Vickrey-Clarke-Groves (VCG) mechanisms. VCG mechanisms have received an enormous amount of attention in the computer science literature over the past two decades [START_REF] Nisan | Algorithmic Game Theory[END_REF]. Our work differs from VCG work in that we are not asking players to declare their preferences: we assume these are known.

Our work relates to a number of other topics in the multi-agent systems community and beyond. Some consideration has been given to how a principal can change the equilibrium strategies of specific games by introducing penalties (a form of taxation) on some actions of the players. Interesting applications include information security [START_REF] Sun | Information Security Game Analysis with Penalty Parameter[END_REF] and analyzing the TCP protocol. In the multi-agent systems community, Monderer and Tennenholtz proposed the notion of k implementation [START_REF] Monderer | K-implementation[END_REF], whereby a principal can make payments to players (negative taxes) to incentivise players to choose certain outcomes. The setting for k-implementation is one of payments, in contrast to the present paper, and our use of Boolean games and logical objectives Υ is rather different. A related idea is discussed in [START_REF] Bachrach | The cost of stability in coalitional games[END_REF], which considers how much compensation would have to be paid to players in a cooperative game in order for certain outcomes to become core stable.

Finally, we should mention some related work on manipulating games through communication. Grant et al. [START_REF] Grant | Manipulating boolean games through communication[END_REF] consider a variation of Boolean games in which players have beliefs about certain variables in the game, and base their decisions about what choice to make on these beliefs. They assume a principal is able to make announcements about the value of variables, and in this way, the principal can influence the choices that players will make. The overall idea (attempting to influence the outcomes of a game) is similar to our setting, although the mechanism through which this is achieved (communication) is quite different.

Conclusions

In the present paper, we have studied the use of taxation schemes to incentivise behaviours in Boolean games: a natural, expressive, and compact class of logic-based games. We showed how a principal could perturb the preferences of agents in a Boolean game by imposing a taxation scheme, and in so doing, how it could, in certain circumstances, incentivise agents to choose outcomes to satisfy an objective Υ, represented as a Boolean formula. However, we saw that while an agent's preferences can be perturbed, they are not completely malleable: no matter what the taxation scheme, an agent would always prefer to get its goal fulfilled than otherwise. This means there are limits on the extent to which preferences can be perturbed by taxation, and hence limits on what objectives Υ can be achieved. We studied a number of questions around the question of implementing objectives Υ via taxation schemes, and also discussed some issues surrounding equitable taxation.

We believe the results of the present paper strongly indicate that there are important and interesting theoretical and practical questions relating to non-incentive compatible taxation schemes. Future work might consider, for example, techniques for the computation of taxation schemes τ for objectives Υ; and the use of taxation schemes to incentivise behaviour in richer settings, beyond the Boolean games considered in the present paper.

Proof:

  Let τ (p, b) = τ (p, b) + c(p, b) for all p ∈ Φ and all b ∈ B. Then the utility functions for (G , τ ) are identical to those for (G, τ), and thus the Nash equilibria must coincide as well.

2 .

 2 If τ (p, ) > τ(p, ⊥), then we set τ (p, ) = τ (p, )τ (p, ⊥) and we again leave p untouched in the game.

3 .

 3 If τ (p, ) < τ(p, ⊥), then we set τ (p, ) = τ (p, ⊥)τ (p, ) and we flip p in the game.

Example 3

 3 Define a game G as follows: N = {1, 2}, Φ = Φ 1 = {p}, Φ 2 = ∅, γ 1 = p, γ 2 = , and c(p, b) = 0 for all b ∈ B. Let Υ = ¬p. Suppose there is a taxation scheme τ such that ∃ v ∈ NE (G, τ) and v |= Υ, i.e., v |= ¬p. So v |= γ 1 and thus u 1 ( v) = -e 1 (v 1 ) = 0. But suppose 1 chose the valuation v 1 with v 1 (p) = . Clearly this choice would satisfy its goal, and would hence represent a profitable deviation from v for 1, so v ∈ NE (G, τ); contradiction.

Table 1 :

 1 Key notational conventions.

	v μ i μ i	i )	total expense (= marginal cost + tax) of choice v i to player i the most expensive choice for player i ∈ N the cost to player i of v μ i
	u i ( v)	utility to player i of outcome v
	(G, τ)	a scenario: a Boolean game together with a taxation scheme
	NE (G, τ)	the (pure) Nash equilibria of scenario (G, τ)
	NE ϕ (G, τ)	the Nash equilibria of (G, τ) that satisfy ϕ ∈ L
	H = N, Φ, γ 1 , . . . , γ n , Φ 1 , . . . , Φ n	a cost-free game (i.e., Boolean game without cost function)
	H G		the cost-free game extracted from Boolean game G
	NE (H)	the Nash equilibria of cost-free game H
	Υ		the principal's objective: Υ ∈ L
	WI (G, Υ)	the set of taxation schemes weakly implementing Υ in G
	SI (G, Υ)	the set of taxation schemes strongly implementing Υ in G

  2 ), which satisfies p 1 ∧ ¬p 2 . Agent 1 gets its goal fulfilled, while agent 2 does not; and moreover (v * 1 , v * 2 ) |= Υ. However, if we adjust τ so that τ (p 2 , ⊥) = 10, then we find a Nash equilibrium outcome

while c(p 2 , ) = 1 and c(p 2 , ⊥) = 0. Define an objective Υ = p 1 ∧ p 2 . Now, without any taxes (i.e., with taxation scheme τ 0 ), there is a single Nash equilibrium, (v * 1 , v *

This is a slight (but harmless) abuse of notation: since expenses depend on the taxation mechanism, they would be more properly denoted by e i (v i , τ). The taxation scheme τ will always be clear from context when we write e i (v i ).

This restriction to games with zero cost is not required, but it does simplify exposition; and we have just seen that for the analysis of Nash equilibria it suffices to consider zero cost games.

Note that the value k i here is not the same as the value μ i defined earlier.

In this section, we will assume we are considering weak implementation, although the definitions are straightforwardly reformulated in terms of strong implementation.

Acknowledgments

This paper has evolved from a paper that was published at the AAMAS-2011 conference [9]; a shorter version of the AAMAS-2011 paper was also published in the "best paper track" at the IJCAI-2011 conference. We thank the anonymous AAMAS and IJCAI referees for their useful and insightful comments. Lang thanks the project ComSoc (ANR-09-BLAN-0305-01). Wooldridge gratefully acknowledges the support of the European Research Council under Advanced Grant 291528 ("RACE").

Now, this result applies to games with a uniform cost function. But intuitively, we can make a game uniform by setting taxes appropriately, to "level out" taxes and costs; by then using the idea of the preceding proposition, we only then need some small additional tax to "fix" the desired outcome.

Proposition [START_REF] Grant | Manipulating boolean games through communication[END_REF] Let G be a game, let Υ ∈ L be an objective, and let ε 1 be any arbitrarily small positive number. Then Υ is weakly implementable in G iff Υ can be weakly implemented by a taxation scheme τ * such that τ * is bounded by the value:

(→) First, define the value t * as follows:

Next, define a taxation scheme τ 1 as follows. For all p ∈ Φ, b ∈ B:

It is clear from construction that the scenario (G, τ 1 ) is uniform. Now, let τ 2 be a taxation scheme that weakly implements Υ in G, and let (v 1 , . . . , v n ) be an outcome such that

is the one we want to "fix", by making all other choices more expensive. To do this, we define a third taxation scheme τ 3 as follows. For all i ∈ N, p ∈ Φ i , and b ∈ B:

We claim that (v 1 , . . . , v n ) ∈ NE (G, τ 3 ), and hence that τ 3 ∈ WI (G, Υ). For suppose that

Then some player can benefit by making a different choice: either to get its goal fulfilled, or to reduce costs. No unsuccessful player can deviate and get his goal fulfilled, for otherwise from Observation 2 we would have

But equally, by construction, no player can reduce costs from deviation.

(←) Immediate. Now, at this point let us return to the assumption we made earlier with respect to the space requirements for taxes: that we are restricting our attention to taxation schemes requiring space polynomial in the size of the game. The preceding proposition shows that if we can weakly implement Υ, then we can weakly implement it with only "small" taxes. However, this does not in itself imply that the space requirement for the "small" taxation scheme is also small: we could conceivably have some small tax value that required a large amount of space to represent it! Nevertheless, it should be clear that if we restrict our attention to games with costs that are given by natural numbers, then essentially the same construction can be used to build taxation schemes that do have small space requirements.

(C1): Suppose condition (C1) holds. Let (v 1 1 , . . . , v 1 i , . . . , v 1 n ) be an outcome satisfying the conditions of (C1); note that

For if it is not a Nash equilibrium of (G, τ), then some player i has a beneficial deviation. Since (v 1 1 , . . . , v 1 i , . . . , v 1 n ) ∈ NE (H G ), then no player can deviate to get their goal fulfilled, so the only possible deviation would be one that would reduce taxes. We know that for all players i ∈ N and for all choices v 2 i such that (v

, because i cannot deviate to have her goal fulfilled. Now, there are two possibilities:

and in this case, v 1 i must be a least cost choice to i, and so player i can have no beneficial deviation.

In this case, we would have

i cannot be a beneficial deviation for i. In either case, no player can have a beneficial deviation from

, and so, because v 1 |= ¬Υ, τ does not strongly implement Υ in G.

(C2): Suppose condition (C2) holds. Assume (v 5 1 , . . . , v 5 n ) ∈ NE Υ (G, τ). We will show that in fact some player has a beneficial deviation from (v We therefore conclude that if Υ can be implemented in G, then the condition on games must be true.

We emphasise that this characterisation is purely logical: the condition on games, given by the predicates NoBad(• • •) and SomeGood(• • •) do not refer to cost functions or taxation functions.

Secondary Criteria for Taxation Schemes

In attempting to design a taxation scheme τ for a Boolean game G, the primary aim of a principal is to design the scheme so that agents are rationally motivated to choose an outcome satisfying the objective Υ 4 . However, if it is possible to incentivise agents to satisfy Υ, then there will, in