Preferences in Game Logics Abstract
even excluding the possibility that an agent might value op-tions equally. Models of social procedures that do not re-
We introduce a Game Logic with Preferences (GLP),
quire one to completely specify the preferences of agents
which makes it possible to reason about how information
are thus highly desirable. Gal and Pfeffer [9, 10] have also
or assumptions about the preferences of other players can
recognized this problem, and use Networks of Influence
be used by agents in order to realize their own preferences.
Diagrams to model game situations in which agent may
GLP can be applied to the analysis of social protocols such
have different beliefs about which game they are playing. as voting or fair division problems; we illustrate this use of
We take a different approach by starting with one common
GLP with a number of worked examples. We then prove that
game form and use logical assumptions to represent differ-
the model checking problem for GLP is tractable, and de-scribe an implemented model checker for the logic – by us-
One can also model social procedures as distributed or
ing the model checker, it is possible to automate the analy-
interpreted systems [8]. These systems are models for the
sis and verification of social protocols.
options and knowledge that agents have: important proper-ties such as ‘Alice, Bob and Caroline will eventually agree
1. Introduction
on an outcome’ can be verified using temporal logics [4];temporal epistemic logics can be used for knowledge based
We are interested in the formal specification, analysis, and
requirements [8], and coalition (epistemic) logics [17] can
verification of mechanisms for social interaction [15]. Ex-
be used for properties such as ‘Alice knows that on her own
amples of such mechanisms include voting and election
she has no strategy to block Zambia as an outcome’. Unfor-
procedures [5], auction and trading protocols, and solutions
tunately, these approaches do not deal with preferences at
for fair division and dispute resolution [3]. As a simple ex-
all. The assumption in these systems is that agents know
ample, consider the problem of constructing a voting proce-
nothing about other agents’ preferences – and of course
dure for Alice, Bob, and Caroline to decide between three
this is also an unrealistic assumption. In short, this paper
holiday destinations: Xanadu, Yemen, and Zambia. An ex-
presents a logic that is intended to overcome these limita-
ample requirement for this social choice mechanism might
tions. This logic allows us to reason about interactions be-
be that if two people prefer the same choice, then that choice
tween agents with only partial knowledge about their pref-
erences. Specifically, we are interested in the question how
One can model many mechanisms for social interaction
the addition of information about other agents’ preferences
as extensive games [14, 2], and then use game theoretic
influences the strategies of agents and coalitions of agents.
concepts to characterise properties of the protocol. Unfor-
The key assumption we make is that agents reason about
tunately, a game is not just a model for a protocol, it is a
the preferences of other agents, and then make certain
model for the protocol and the preferences of the agents.
strategic decisions. We do not specify how they know it
One would like to model procedures as complete and per-
(it might be by means of communication, espionage, or
fect information games, because this is a simple class of
by studying previous histories of the game); the informa-
games; but then all agents have complete knowledge of
tion about the preferences might even be hypothetically as-
each other’s preferences. This is an unrealistic assumption.
sumed. Reasoning about the preferences of (other) agents
In fact, for the holiday example above, each agent can or-
is interpreted as reasoning about their strategies, because
der the three countries in six possible ways, and therefore
for a rational agent, having a preference implies choos-
one would need to consider at least 216 different games,
ing a strategy that leads to this preference. The knowl-
edge that agents have, based upon their knowledge of other
a tree t = N, T, n0 , with root n0 ∈ N. Given a tree t, we
agents’ preferences, is called strategic knowledge [7]. Al-
define the successor function Succ : N → 2N, yielding for
though our aim is to study strategic knowledge in this pa-
every n ∈ N its set of successors {n ∈ N | (n, n ) ∈ T}.
per, we do this implicitly, since we do not introduce strate-
The function Z(T) = {n ∈ N|Succ(n) = ∅} defines the set
gies as first class citizens of our logic, but rather refer only
of all terminal nodes of the tree: we refer to them as states.
to preferences. We develop a logic GLP (Game Logic withGame Form A game form is a tuple F = Σ, Ag, N, T, n0 , Preferences), which allows us to reason about the conse-
where Σ is a set of agents or players and N, T, n0 is a tree.
quences of the announcement of information about prefer-
The function Ag : N \ Z(T) → Σ assigns an agent to each
ences. Initially, agents know the protocol but do not know
non-terminal node: this agent is thought of as the agent that
other agents’ preferences. The logic enables us to make as-
decides the next action, or, equivalently, what the next node
sumptions about their preferences, and subsequently to ex-
will be. Conversely, the function Ow returns, for every agent
press the consequences of such assumptions. Note that some
i, the set of nodes “owned” by that agent.
simplifying assumptions are made. We assume agents haveperfect information about the current game state, so we do
Game A game is a tuple (F,
not consider imperfect information games. We also assume
: Σ → 2Z(T)×Z(T) is a function that assigns to each
that all agents have the same information about preferences.
The remainder of the paper is structured as follows. Sec-
Preference relations are assumed to be transitive and sym-
tion 2 defines some game theoretic notions that are used
i n means that agent i thinks that n
throughout the paper. The logic GLP for expressing proper-
is at least as good as n . We write n
ties of protocols is defined in Section 3, together with its se-
mantics. The use of GLP is illustrated through some exam-
Game Form Interpretation A game form interpretation is
ple protocols in Section 4. In Section 5, an efficient algo-
a tuple (F, P, π) where F is a game form Σ, Ag, N, T, n0 ,
rithm for evaluating GLP properties is given, and an imple-
P is a finite set of propositions and π : Z(T) → 2P as-
mentation of this algorithm in a Java model checker for GLP
signs to each non-terminal node the set of propositions that
is described. We present some conclusions in Section 6. Game Interpretation A game interpretation is a tuple 2. Extensive Games and Game Forms
(F, , P, π) such that (F, P, π) is a game form interpreta-tion and (F,
Extensive games are defined in several different but essen-tially equivalent ways in the literature: for example as a
Preference We say that agent i has a preference for a set
tree [13], or as a set of runs [14]. We use a definition as a
of outcomes S ⊆ Z(T) in game (F,
tree, but stay close to the notation of [14], and we will sim-
t ∈ Z(T) \ S we have that si t. In this definition, a set S is
ply refer to ‘game’ when we mean ‘extensive game’.
thus preferred over its complement. Note that this is a strong
Informally, a game consists of two components. The
notion of preferences. We can only say that a person prefers
game form F specifies the available actions for each agent,
to have coffee if the worst situation in which it has cof-
fee is better than the best situation in which it does not have
erences. For our formal approach we also need an interpre-
coffee. This strong definition is convenient in a logical ap-
tation, π, which allows us to use propositions for describ-
proach, because it allows one to draw definite conclusions.
ing end states. We do not always need all these components
A notion of preference in which the average value of s ∈ S
at the same time, and therefore we distinguish the follow-
is higher than the average value of an element t /
be applicable within a probabilistic framework. A coalitionof agents Γ prefers a set S if each member i ∈ Γ prefers S. Strategies A pure strategy for agent i in a game form F is
a function PSi : Ow(i) → N such that PSi(n) ∈ Succ(n).
This function prescribes a decision for agent i to each nodeowned by i. A mixed strategy is a function MSNotation Throughout this paper we follow coalition logic
conventions [17] by using Σ to denote a set of agents, Γ
i(n) ⊆ Succ(n). A mixed strategy pre-
scribes a subset of alternatives to each node owned by i. A
for a coalition of agents (so Γ ⊆ Σ), i ∈ Σ for an arbi-
strategy for a coalition Γ, either mixed or pure, is a set of
trary agent, P for a set of propositions and π as an interpre-
strategies, one for each agent in Γ. If S
and n ∈ N with Ag(n) ∈ Γ, then SΓ(n) = SAg(n)(n). We use
Trees The symbol N is used for a finite set of nodes, and
both the notation n ∈ SΓ(n) and SΓ(n) = n when not con-
T ⊆ (N × N) is a binary relation between them, yielding
fusing. For the grand coalition Σ, SΣ is called a strategyprofile. Such a profile s represents a Nash Equilibrium if no
The logic GLP contains all connectives of propositional
agent in Σ can unilaterally deviate from s and improve his
logic and two additional operators. One can be used to intro-
outcome. It is well-known that every two person zero-sum
duce formulas of propositional logic in GLP, and the other
game has such an equilibrium, which can be obtained us-
one is used to express consequences of preferences. Definition 2 Let P be a set of propositions, and Σ a group Strategy Updates A game is often thought of as a set of of agents. Let PL be the language of propositional logic
possible computations or runs. Each path on the game tree
over P. The language for GLP is the smallest language L
then corresponds to a run. Formally, a run of the game form
such that for any formula ϕ0 ∈ PL and ϕ, ψ ∈ L, it is the
Σ, Ag, N, T, n
0 is a sequence n0, n1, . . . , nz where n0 is the
root of T and nz ∈ Z(T) is a terminal node, and for each k it
is the case that (nk, nk+1) ∈ T. If an agent or a coalition of
agents is committed to a certain strategy S, certain runs can
be excluded from consideration because these runs are not
compatible with that strategy. A run n0, n1, . . . , nz is com-patible with a mixed strategy SΓ if for any pair (n
with Ag(nk) ∈ Γ it is the case that nk+1 ∈ SΓ(nk). This
game in which coalition Γ prefers ϕ0, ψ will hold’. The
means that every choice made by an agent from coalition Γ
ϕ0, takes a propositional logic formula ϕ0,
must be made according to SΓ.
which can be interpreted in a specific state, and converts it
We define an update function u for any game form
into a GLP formula: it means that ϕ0 holds for every pos-
F = Σ, Ag, N, T, n
sible outcome. A useful shorthand is the sometimes opera-
0 and strategy SΓ, such that u(F, SΓ) =
Σ, Ag , N , T , n
0, which means that ϕ0 holds for some outcome. It
Γ. To achieve this, we stipulate that Ag is the
restriction of Ag to N ⊆ N which is generated from N by
sible, we omit brackets and commas in the notation of a set
the new T relation, which is defined as
Γ of agents, for example writing [ABC : ϕ0]ψ instead of[{A, B, C} : ϕ0]ψ. T = {(n, n ) ∈ T | Ag(n) ∈ Γ ⇒ n ∈ SΓ(n)}
Sample formulas of this logic, with their reading in the
holiday example from Section 1 are given in the next table.
Note that in this updated model, agents not in Γ still have
The outcomes Xanadu, Yemen or Zambia are indicated by
all of their options open. Only agents that are part of Γ are
propositions x, y and z, while Alice, Bob and Caroline are
now limited to making choices that are compatible with SΓ.
called A, B and C, respectively.
♦x Xanadu is a possible outcome. 3. A Logic for Preferences
[AB : y] y If Alice and Bob prefer Yemen, then Yemen is
In this section we define the syntax and semantics of the
[A : x ∨ y][B : x] ¬z If Alice prefers Xanadu or Yemen,
and Bob prefers Yemen, then they will not go to Zam-
3.1. Syntax of
We find it convenient to define the syntax of GLP in sev-
3.2. A Game-theoretic Semantics
eral stages, beginning with (classical) propositional logic.
We now give the formal semantics of GLP. We begin by
Definition 1 The language PL of propositional logic over a
showing how propositional logic can be used for describ-
set of propositions P is the smallest set L ⊇ P such that for
ing the outcomes of game form interpretations. We then
any ϕ ∈ L and ψ ∈ L we have that ϕ ∨ ϕ ∈ L and ¬ϕ ∈ L.
show how GLP can be evaluated over game form interpre-tations, by using an update function for preferences, and to
We use propositional logic to express properties of the out-
complete our definition we define the update function. The
comes or results of games. An example inspired by football
first and easiest step is defining the interpretation of propo-
is the statement ¬winA ∧ ¬winB, which expresses that nei-
ther team A wins nor team B wins. It is important to realizethat propositional logic is only used for properties of termi-
nal states, not for intermediate states of a game or proto-
In the interpretation of GLP, the logical connectives are de-fined similarly. The operator
all end-states’, and the assumption operator [Γ : ϕ
is defined on game form interpretations M as follows. We then calculate a restricted game form interpreta-
= Up(M, Γ, ϕ0), in which Γ acts as to guar-
antee ϕ0, and we evaluate whether M fulfills ψ. Let
Σ, Ag, N, T, n0, P, π be a game form interpreta-
for all s ∈ Z(T) π, s |= ϕ0
Figure 1. Alice and Bob eat cake
In Section 2, we defined what it means for a coalition to
antees ϕ0 in F . The strategy S∗ = S∗(F, Γ, ϕ0) is the most
prefer a set of outcomes S. We now extend this definition
general sub game perfect strategy for Γ and ϕ0 in F. The
to propositional logic formulas. We say that Γ has a prefer-
ence for ϕ in game interpretation (F,
the set S = {s|π, s |= ϕ}. Thus, a propositional formula is
Up(M, Γ, ϕ0) = u(F, S∗(F, Γ, ϕ0)), P, π
preferred if the set of end nodes in which it is true is pre-ferred. The update function Up(M, Γ, ϕ
where π is the restriction of π to the new set of nodes.
in which the actions of agents in Γ are restricted to actionsthat help them achieve a preferred outcome. We use the no-
4. Examples
tion of a subgame perfect strategy [16]. The behaviour ofagents should be rational in any subgame-form F of the
This section provides some examples that illustrate how
complete game form F. Moreover, the agents should not
GLP can be used in the specification and analysis of social
assume any helpful behaviour from agents outside Γ. Fi-
nally, the model Up(M, Γ, ϕ0) should not be unnecessar-ily restricted: any actions that are rational should be avail-
Alice and Bob eat cake
able to agents in Γ. Below we have formalized when a strat-egy guarantees something, when it is subgame perfect, and
Alice and Bob have a cake, and they have agreed to divide it
when a strategy is more general than another strategy. These
by means of a “cut-and-choose” protocol [3]. Alice has cut
notions are use to define the update function.
the cake and unfortunately one of the pieces is bigger than
A mixed strategy MSΓ for coalition Γ contains a pure
the other. Bob can now choose from three options: he can
strategy PSΓ of coalition Γ iff for all nodes n with Ag(n) ∈
select the big piece, select the small piece, or he can say to
Γ we have that PSΓ(n) ∈ MS(n). A mixed strategy is com-
Alice ‘No, you choose’. If he lets Alice choose, she can ei-
pletely described by the pure strategies it contains. We can
ther choose the big piece or the small piece. Both agents
think of a mixed strategy as giving some information about
have common knowledge of this protocol, and they know
which pure strategy is used. A mixed strategy seen in this
that they neither know the other agent’s preferences (see
way is a description of the information other agents may
Figure 1): proposition a means that Alice gets the biggest
have about the strategy used [1]. One can compare mixed
piece, b that Bob gets the biggest piece, and e means that
strategies using an inclusion operator. For two mixed strate-
something embarrassing has happened, namely that either
gies S1 and S2, both for coalition Γ, we say that S1 is con-
Alice or Bob has chosen the biggest piece. In many cul-
tained in S2, or that S2 is more general than S1 and write
tures this is not polite and in several of the example formu-
S1 ⊆ S2, if and only if for all nodes n with Ag(n) ∈ Γ
las we assume that everyone is embarrassed if this happens.
we have that S1(n) ⊆ S2(n). This provides a partial order-
Using GLP one can express relevant properties of this pro-
tocol. First we will provide several GLP formulas (A stands
Definition 3 A strategy SΓ guarantees ϕ0 in game form F
for Alice, B stands for Bob). iff every outcome s of game form u(F, SΓ) fulfills π, s |= ϕ0.
• [B : ¬e] a If B does not want either of them being im-
We say that Γ can guarantee ϕ0 in F if there exists a strat-
polite, he must take the smallest piece. Our semantics takes
egy SΓ such that SΓ guarantees ϕ0. We say that SΓ is sub-
a pessimistic view, so Bob cannot take the risk of letting A
game perfect for ϕ0 in F if for every subgame F of F such
choose. Figure 2 shows the model Up(M, {B}, ¬e). that Γ can guarantee ϕ0 in F it is the case that SΓ guar-
• [B : ¬e][A : ¬e] a This formula is a consequence of the
Figure 2. Model Up(M, {B}, ¬e) Figure 3. Model Up(M, {A, B}, ¬e)
previous example. It expresses that if B does not want em-
alternatives (x, y, and z). We use this problem to show
barrassment and that A does not want embarrassment, then
how GLP can be used for expressing the requirements of
A gets the biggest piece. This may seem strange, since there
such protocols. Next, we present two example solutions and
is an outcome in which ¬e and b are true. However the or-
show how GLP can express the differences between them.
der of assumptions is important. The formula expresses that
We require a voting protocol P in which exactly one
B wishes to guarantee the absence of embarrassment, inde-
option is chosen and any group of two agents can decide
pendently of what A does. Two possible readings of the for-
on any outcome. This is formalized in the next formu-
mula are that he commits himself to his strategy before he
las. Let Γ ⊆ {A, B, C} and u, v variables over the options
learns that A has the same preference, or that he thinks that
O = {x, y, z}.
this goal is so important that he does not wish to rely on Afor this property.
• [AB : ¬e][B : b] b In this example, A and B com-monly want to avoid embarrassment, and B also prefers
b. If this is the case, B can let A choose and then A will
take the smallest piece. Figure 3 shows the updated model
Up(M, {A, B}, ¬e). Note that, strictly speaking, B cannot
In Figure 4, a protocol P1 is depicted which satisfies
prefer ¬e and b simultaneously, since that would mean that
these requirements – it is in fact a smallest protocol that
the situation with ¬e ∧ ¬b is preferred over the situation
satisfies the requirements, as one can verify by testing all
with e ∧ b and vice versa. However the preference for b ap-
smaller trees. It works in two steps. First, A can say whether
pears in the scope of a preference for ¬e, so one could say
B or C can make a choice. Then, either B or C can indi-
that the agent prefers first ¬e ∧ b, then ¬e and then ¬e ∨ b.
cate which of the three destinations is chosen. The protocol
This does correspond to a single preference relation.
may seem strange because A cannot directly support a cer-
• [A : ¬e][B : ¬e][B : b] b This formula expresses that if A
tain outcome. What is the best action for A depends on what
does not want embarrassment, B does not want embarrass-
B and C will do. In this protocol it is thus important for A
ment, and B prefers the biggest piece then B gets the biggest
to know what the others do, while C and B need no infor-
piece. The behaviour of B is influenced by the fact that he
mation about the other agents. The next GLP formulas illus-
knows that A prefers to avoid embarrassment. In this sce-
trate this peculiarity of protocol P1.
nario A should try to hide the fact that she has good man-
P |= [AB : x] x
ners, because it is not in her advantage if B knows this. P |= [B : x][A : x] x
These examples illustrate that, by using GLP, one can
P |= [A : x][B : x] x
express consequences of ordering goals in a certain way. Similar to the concept of common knowledge in epistemic
There is of course more than one protocol that meets the
logic [8], we have the idea of a common goal, which is dif-
given requirements: Figure 5 shows another solution. In this
protocol, A can vote for any alternative and then B votes forone of the alternatives. If they vote for the same option, then
Voting Protocol
this option is chosen. If they disagree, agent C can choosebetween the two options that A and B voted for. So agent
In the introduction, we already mentioned the problem of
C has only two options. Nine extra propositions are intro-
defining a fair voting protocol. The problem is to design a
duced, to indicate which agent has cast which vote: propo-
voting protocol for three agents (A, B, and C) over three
sition ax means that agent a has chosen option x, and simi-
Figure 4. A voting protocol P1 Figure 5. A second voting protocol y, az, bx, by, bz, cx, cy, cz. In the figure only the left
This protocol also satisfies the requirements. A nice
be reached? In the next table the preference relation of each
property of this protocol is that A can directly indicate a
preference. The extra propositions (ax, bx, . . .) show howone can use propositions in end states to indicate that a cer-
This demonstrates that in finite trees, one can use propo-
sitions in end states for events that one would describe us-
All formulas that are preferred by some coalition are listed
ing intermediate propositions or propositions on transitions
The extra propositions allow one to formulate questions
about strategic voting. An agent votes strategically if it does
not vote for the options it prefers most [11]. In an ideal vot-
ing protocol, agents do not gain anything by strategic vot-
ing. Unfortunately the Gibbard-Satterthwaite Theorem [11]
states that in any voting scheme not completely determined
One can see that there are not many coalition preferences
by a single agent it is possible to benefit from strategic vot-
for this preference relation. The reason is that our definition
ing. With GLP, one can determine for any protocol in which
of a preference is quite strong. One can show that Yemen is
circumstances strategic voting might occur.
a likely outcome of the holiday election according to proto-
First, we list some related properties about the options.
We see that agent A is completely free to vote for x if shewants that, while C is not. On the other hand, C’s vote is
P1 |= [A : x][C : y][AC : x ∨ y] y
always decisive, which is not true for A’s vote.
This formula expresses that given the preferences of A and
C and the protocol, A will say that C may decide and C
will choose for option y. This outcome is a sub-game per-
((cx → x) ∧ (cy → y) ∧ (cz → z))
fect Nash equilibrium of the game (P,
((ax → x) ∧ (ay → y) ∧ (az → z))
tocol, the same outcome can be rationalized by:
An interesting result is that C, under our rationality con-
dition, should not vote for an option it does not prefer. Un-
P2 |= [A : x][C : y][AC : x ∨ y] y
fortunately, this result cannot be shown for A. If A prefersx, but A knows that B and C prefer y, then it is equally ra-
However, other outcomes can be rationalized by making
tional for A not to vote for x, since A knows it will not be
2 |= [B : x ∨ z][C : x ∨ y][A : x]
P |= [B : x][A : x] x
In this case, A votes for x. From the assumption that BP |= [A : x][B : x] x
prefers x or z, everyone can conclude that B will not vote
Suppose we know what the preferences of our agents
y. If B votes x, x is the outcome. Otherwise c will chooses x
are: can one then use GLP to derive which outcome will
over z, and x is also the outcome.
From these examples, it should be clear that it is not
only important who has which preferences, but also which
eval(((Σ, N, T, I), P, π), ϕ)={
preferences one considers. If different preferences are an-
nounced, signaled, or otherwise communicated in some
5. Model Checking GLP
return ¬eval(((Σ, N, T, I), P, π), ψ)
Model checking is the problem of deciding whether a given
formula is true on a given model [4]. A model checking
return eval(((Σ, N, T, I), P, π), ψ) ∨
algorithm for GLP can be used for the automatic verifica-
eval(((Σ, N, T, I), P, π), χ)
tion of multi agent interaction protocols, such as verifying
that the protocols from Section 4 satisfy the stated require-
ments. In this section, we prove that the model checking
u =update(((Σ, N, T , I), P, π), Γ, ϕ0 )
GLP is tractable. Our proof is constructive: Fig-
ures 6 and 7 give a polynomial time model checking al-gorithm for GLP. Formally, we assume that the size of Σis bounded by some constant. The size of a model (|M|)
Figure 6. The GLP model checking algorithm
is defined as the number of nodes it contains, while thesize of a formula (|ϕ|) is the number of connectives, op-
end nodes must be less than |M|, we obtain our intermedi-
erators, and propositions. Let c(X) denote the number of
operations needed to compute the value of expression X.
To complete the proof of the main theorem, we note that
The notation c(X) = O(f (|X|)) means that there is a size
the evaluation function either evaluates its subformulas ϕ
s and a constant g such that, for any input X with |X| > s,
c(x) < g · f (|X|) [6]. Now:
sub|)), or propositional logic formu-
las ϕprop in end nodes (O(|M| · |ϕprop|)), or it updates with
Theorem 1 The problem of determining whether a GLP for-
a subformula ϕsub (O(|M| · |ϕsub|)). Finally, note that ev-
mula holds on a game form interpretation can be solved in
ery part of the formula ϕ is processed only once. time polynomial in the size of the game form and the size of
{x} ∪ {c1(T, y)|(x, y) ∈ T} and c2(N, T) = T ∩ N2. These function remove spurious transitions and nodes, such
c(M |= ϕ) = O(|M| · |ϕ|)
that c1(T, x), c2(c1(T, x), T), x is always a proper tree.
We have implemented a model checking system for
Outline proof: In order to see that this theorem is true, we
GLP which uses this algorithm. The three example pro-
need to establish both that the algorithms in Figure 6 and 7
tocols described in this paper are part of the distribu-
are correct and that the algorithms have the stated efficiency.
tion of the model checker. The program can be found at
The eval algorithm is basically an algorithmic representa-
tion of the semantics of GLP, and its correctness proof fol-lows from induction on the structure of formulae. The up-date2 function of Figure 7 is a modified version of Zer-
6. Conclusion
melo’s algorithm or backward induction [2]. (Instead ofonly returning the value of the game (either −1 or 1) it
What agents do not only depends on their own preferences,
also returns a set of transitions that one should avoid in or-
but also on their knowledge of other agents’ preferences.
der to realize the value). The correctness of Zermelo’s algo-
The logic GLP allows one to analyze multi agent proto-
rithm, we claim, carries over to our algorithm. For the com-
cols making various assumptions on what is known about
plexity bound, we use that checking propositional formulas
agents’ preferences. Besides defining this logic and a suit-
in end nodes takes time proportional to the size of the for-
able interpretation over extensive game forms, we show that
mula: c(π, s |= ϕ0) = O(|ϕ0|). In order to prove the main
the model checking problem for this logic has a low com-
theorem we claim the following about the update function:
putational complexity. We demonstrated how one can spec-
c(Up(M, Γ, ϕ0)) = O(|M| · |ϕ0|). Zermelo’s algorithm tra-
ify interesting social problems and protocols as an exten-
verses the whole game tree without visiting a node twice.
sive game form, and how GLP is useful for understanding
This takes time proportional to the size of M. In each end
node it evaluates propositional logic formulas, which takes
In GLP one can do semantic updates of a specific kind:
time proportional to the size of ϕ0. Since the number of
we assign a preference to a coalition, and since agents act
[12] does not provide a notion of hypothetical reasoning
update(((Σ, N, T, I), P, π), Γ, ϕ)={
would players play such an equilibrium.
let (R, v) :=update2(T, π, n0, x, Γ, ϕ)
An extension of GLP would be a framework in which
return ((Σ, c1(T \ R, n0), c2(c(T \ R, n0), T), I), P, π)
coalitions not only have preferences over outcomes, but
over complete games. Another extension would be to have
update2(T, π, x, Γ, ϕ)={
parallel updates. Another direction is to develop a similar
logic for extensive games with imperfect information. This
would allow us to study a wider class of protocols and prob-
lems in which information is important.
let N := {(x, n)|(x, n) ∈ T}
References
let R := ∅ , R2 := ∅ , v := 1if I(x) ∈ Γ
[1] R. Aumann and A. Brandenburger. Epistemic conditions for
a nash equilibrium. Econometrica, 63:1161–1180, 1995.
(Rn, vn) := update2(T, π, n, Γ, ϕ)
[2] K. Binmore. Fun and Games: A Text on Game Theory. D.
C. Heath and Company: Lexington, MA, 1992.
[3] S. Brahms and D. Taylor. Fair division: from cake cutting toR2 := R2 ∪ {(x, n)}
dispute resolution. Cambridge University Press, 1996.
[4] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Check-ing. The MIT Press: Cambridge, MA, 2000.
[5] V. Conitzer and T. Sandholm. Complexity of mechanism de-
sign. In Proceedings of the Uncertainty in Artificial Intelli-gence Conference (UAI), Edmonton, Canada., 2002.
[6] T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduc-
(Rn, vn) := update2(T, π, n, Γ, ϕ)
tion to Algorithms. The MIT Press: Cambridge, MA, 1990.
[7] S. Druiven. Knowledge development in games of imperfect
information, 2002. University Maastricht Master Thesis.
[8] R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoningabout knowledge. The MIT Press: Cambridge, MA, 1995.
[9] Y. Gal and A. Pfeffer. A language for modeling agents’ deci-
sion making processes in games. In Autonomous Agents andFigure 7. The GLP update function Multi Agent Systems 2003, Melbourne, July 2003.
[10] Y. Gal and A. Pfeffer. A language for opponent modeling in
repeated games. In AAMAS Workshop on Decision-Theoreticand Game-Theoretic Agents, Melbourne, July 2003.
rational with respect to the known preferences, this con-
[11] A. Gibbard. Manipulation of voting schemes: a general re-
straints the coalition’s behaviour. These updates are similar
sult. Econometrica, 41(4), 1973.
to public announcements in dynamic epistemic logic [18],
[12] B. Harrenstein, W. van der Hoek, J.-J. C. Meyer, and C. Wit-
in the sense that all agents learn commonly from the as-
teveen. On modal logic interpretations of games. In Procs
sumption. We believe the assumption that agents have par-
ECAI 2002, volume 77, pages 28–32, Amsterdam, July 2002.
tial knowledge about each other’s preferences is an impor-
[13] H. Kuhn. Extensive games and the problem of information.
tant one. The issue how the strategic knowledge that arises
Contributions to the Theory of Games, II:193–216, 1953.
from this assumption influences agents needs more investi-
[14] M. J. Osborne and A. Rubinstein. A Course in Game Theory.
gation, which this paper starts by looking at strategic knowl-
edge in finite extensive games of perfect information.
[15] M. Pauly. Logic for Social Software. PhD thesis, University
of Amsterdam, 2001. ILLC Dissertation Series 2001-10.
The difference between GLP and a coalition logic like
Reexamination of the perfectness concept for
ATEL is that GLP assumes that once a coalition adopts a cer-
equilibrium points in extensive games. International jour-
tain strategy, this strategy is known to all agents. This as-
nal of game theory, 4:25–55, 1975.
sumption makes sense from a game theoretic and security
[17] W. van der Hoek and M. Wooldridge. Cooperation, knowl-
viewpoint. We believe this difference makes GLP suitable
edge, and time: Alternating-time temporal epistemic logic
for the analysis of adversarial multi-agent systems. Harren-
and its applications. Studia Logica, 75(4):125–157, 2003.
stein et al ([12]) also uses preferences over extensive game
[18] H. P. van Ditmarsch. Knowledge Games. PhD thesis, Uni-
trees, in this case to find modal formulas over such trees,
versity of Groningen, Groningen, 2000.
conceived of as Kripke models, that characterize game the-oretic notions, like that of Nash equilibrium. Unlike GLP,

TerraeTempo_149_152 18/1/10 12:55 Página 59 Eduardo Blanco Amor e A esmorga O cincuenta aniversario d'A esmorga pasou con máis pena que gloria. Que eu saiba, só a Concellaría de Doutor en Filoloxía Románica pola Cultura do Concello de Ourense, en mans Compostela. É autor dunha ampla obra nacionalistas, articulou unha serie de actividades en de investigación e ensaio en

Anti-spam policy van Insite Design/Wmmedia Wat is spam? Spam wordt gedefinieerd als unsolicited bulk e-mail (UBE), oftewel: mail die in grote hoeveelheden (bulk) en ongevraagd (unsolicited) wordt verstuurd. Ongevraagd houdt in dat de ontvanger geen aantoonbare en expliciete toestemming heeft gegeven voor de verzending van de e-mail. Bulk houdt in dat de e-mail onderdeel is van een grotere