A Strategic Analysis of Multi-Agent Protocols - Text
A Strategic Analysis of Multi-Agent Protocols - Text
Multi-agent Protocols
by
Cover design by Ernst van Rheenen. The cover shows Achilles and Ajax playing
a game during the Trojan war
Printed and bound by Febodruk BV
ISBN: 90–5776–153–x
Contents
Acknowledgments ix
1 Introduction 1
1.1 Multi-agent Protocols . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Protocol Problems . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Outline of this Dissertation . . . . . . . . . . . . . . . . . . . . . 6
1.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2 Logic 9
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2.1 Minimal Propositional Logic . . . . . . . . . . . . . . . . . 11
2.2.2 Full Propositional Logic . . . . . . . . . . . . . . . . . . . 13
2.3 Modal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.1 Epistemic Logic . . . . . . . . . . . . . . . . . . . . . . . . 19
2.3.2 Common Knowledge . . . . . . . . . . . . . . . . . . . . . 21
2.4 Theorem Proving, Satisfiability and Model Checking . . . . . . . 22
2.5 Computational Complexity . . . . . . . . . . . . . . . . . . . . . . 27
3 Game Theory 33
3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.2 Strategic Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3 Extensive Games . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.3.1 Perfect Information . . . . . . . . . . . . . . . . . . . . . . 42
3.3.2 Imperfect Information . . . . . . . . . . . . . . . . . . . . 46
3.4 Existing Work on Logic and Games . . . . . . . . . . . . . . . . . 48
3.4.1 Coalition Logics . . . . . . . . . . . . . . . . . . . . . . . . 49
3.4.2 Power Level Logic and Bisimulation . . . . . . . . . . . . . 52
3.4.3 Alternating-time Temporal Logic . . . . . . . . . . . . . . 52
v
3.4.4 Dynamic Epistemic Logic . . . . . . . . . . . . . . . . . . 54
vi
7.3.3 Russian Cards Problem . . . . . . . . . . . . . . . . . . . . 136
7.3.4 Communication Example . . . . . . . . . . . . . . . . . . . 139
7.4 Computational Complexity . . . . . . . . . . . . . . . . . . . . . . 141
7.4.1 Tractable Variants . . . . . . . . . . . . . . . . . . . . . . 146
7.5 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
7.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150
9 Conclusion 173
9.1 Perfect Information Protocols . . . . . . . . . . . . . . . . . . . . 174
9.2 Imperfect Information Protocols . . . . . . . . . . . . . . . . . . . 174
9.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
Bibliography 179
Index 189
Samenvatting 197
Abstract 199
vii
Acknowledgments
This dissertation has benefited enormously from comments, suggestions and dis-
cussions with other people, and on these pages I would like to mention as many
of these people as I can remember, in a more or less arbitrary order.
Since I started my PhD by moving to Liverpool, it seems appropriate to start
with the people from this city. I am very grateful to my supervisors, Wiebe van
der Hoek and Mike Wooldridge. A special mention should go to Peter McBurney,
who was not only my advisor but has also encouraged and stimulated me contin-
uously. I would like to thank many colleagues who have helped me to find my
way in Liverpool and in research: Hanno Hildmann, Steve Phelps, Dirk Walther,
Ian Blacoe, Laera Loredana, Rafael Bordini, Carmen Pardavilla and of course
my office mates Benjamin Hirsch, Justin Wang, Qin Xin, Claudia Nalon, Mari
Carmen Fernandez-Gago, Mark Roberts and Nivea de Carvalho Ferreira. I feel
greatly indebted to the many people that contributed to the great atmosphere in
the department of Computer Science, including Thelma Williams, Ken Chan and
the other members of the technical staff, Katie Atkinson, Trevor Bench-Capon,
Aiman Badri, Celia Casado-Castilla, Alison Chorley, Andrea Kam, Christian
Guensel, Catherine Atherton, Shaheen Fatima, Tim Miller and Adele Maggs.
I would like to thank Frank Wolter and Mark Ryan for acting as examiners in
my PhD defense.
In Amsterdam I have benefited from support and encouragement from many
sources, and from a great research atmosphere. First of all I would like to give a
special mention to Johan van Benthem for his critical and stimulating comments,
and for giving me the opportunity to work in the ILLC, and my office mates Aline
Honingh, Merlijn Sevenster and Yoav Seginer. I would like to thank Olivier Roy,
Fenrong Liu, Clemens Kupke, Nick Bezhanishvili, Jelle Zuidema, Reut Tsarfaty,
Maricarmen Martinez Baldares, Balder ten Cate, Ulle Endriss, Joost Joosten,
Chiaki Ohkura, Scott Grimm and Eric Pacuit for many pleasant conversations,
not only during lunch time. I wish to thank Peter van Emde Boas, Marjan
Veldhuizen, Igrid van Loon, Rens Bod, Benedikt Löwe and Robert van Rooij for
ix
their support and comments.
I have always enjoyed presenting my work, so I would like to thank the people
who have given me the opportunity to present my work at their institute: Mathijs
de Weerdt, Vincent van Oostrom, Wouter Teepe, Michael Fischer and Boudewijn
de Bruin.
I am grateful for the financial support that I have received from various exter-
nal organisations, which allowed me to visit summer schools, workshops and con-
ferences. First of all I want to thank AgentLink, the European research network
that has initiated many extremely fruitful meetings and initiatives. Without the
support of the International Joint Conferences on Artificial Intelligence, I could
not have attended the ESSLLI summer school in Nancy. The Association for
Computing Machinery has supported my attendance to the AAMAS conference
in the great city of New York.
The discussions in the logic and games reading group in Amsterdam have been
very helpful, and I would like to thank the members I have not already mentioned
above for their input: Paul Harrenstein, Tijmen Daniëls, Floris Roelofsen, Michael
Franke and Yanjing Wang. I hope this reading group will have a long and fruit-
ful existence. I also feel indebted to Valentin Goranko, Marc Pauly, Mark Jago,
Karl Tuyls, Ronald Cramer, Iyad Rahwan, Tero Tulenheimo, Renze Steenhuisen,
Ernst van Rheenen, Hans van Ditmarsch, Barteld Kooi, Alessio Lomuscio, Fran-
cien Deschesne, John-Jules Meyer and the other people from Utrecht, for the
encouragement and criticisms they have given. Geert Jonker and Stefan Leijnen
should be thanked for their contagious enthusiasm. Finally I would like to give a
very special thanks to Marthélise Vervest for reading my work and all the time
we ave spent together in both Liverpool and Utrecht, and to Rutger van Otterloo
and my parents.
x
Chapter 1
Introduction
• Everyone is familiar with the problem of dividing a cake fairly among several
people. Assume that a round birthday cake is to be shared fairly among
a certain number of guests. If ‘fair’ means into equally sized and shaped
parts and one can use ruler and compass, then this becomes a mathematical
problem. One can also see this situation as a social science problem, by using
another notion of fairness. One can require envy-freeness, which means that
nobody should be envious of somebody else. Everyone should judge his or
her own piece at least as good as the other pieces. This is achievable for
two agents by using so-called ‘cut and choose’ protocols: one agent splits
the cake into two parts, the other agent chooses who gets which part. The
fact that both agents play an active role in this protocol makes it easier
for agents to accept this protocol. What makes the protocol fair is the fact
that the cutter has an incentive to cut as fair as possible. In case of larger
sets of agents, more elaborate procedures exist [17].
• Suppose you want to raise money for a good cause, and a sponsor has given
you a car in order to help you to do so. Should you auction this car, or start
a lottery? A lottery is the traditional way to raise money, at least in The
Netherlands. However, auctions of different types have become increasingly
1
2 Chapter 1. Introduction
• On auction websites such as eBay, many buyers prefer to place their bids at
the very last moments. This is called sniping. These snipers choose to bid
in the last minute even when the auction lasts a week [76]. Possibly they
do this in order to avoid bidding wars with other bidders, who in the face of
competition want to spend more money than they originally planned. An-
other explanation is that the snipers somehow enjoy to surprisingly outbid
other people. Either way, some bidders refuse to behave as prescribed by
auction-theory textbooks. To some bidders and sellers sniping seems unfair,
but others feel it is justified by the amount of pleasure they derive from it.
Agents
It is difficult to come up with a universally accepted definition of the word
agent [124]. Nevertheless, every researcher should know the meaning of the words
he or she uses, or risk talking nonsense. I use the word agent to mean a decision
making entity, and thus I accept humans, computer programs or even organisa-
tions as agents. The word has been used in this way within the English language
for centuries, for instance in the following quotation.
1.1. Multi-agent Protocols 3
In a more recent tradition, agents are seen as software programs with artificial
intelligence-like abilities and properties, such as reflexes, mobility, intelligence
and emotions. The English science-fiction writer Douglas Adams for instance
describes how agents might function when a spaceship tries to recover from a
meteorite hit.
I am not concerned with designing or dissecting actual agents, but with proto-
cols for agents. Thus, where other researchers see the construction of agents, or
even ‘intelligent agents’, as a long term, yet unattained research goal, in my view
there are already agents and protocols. The focus is not on the internal work-
ings of these individual agents, but on the way protocols function when used by
agents. Since protocols are formal objects, they can be studied formally, without
experiments or empirical investigations.
Protocols
A protocol is different from an algorithm because it gives agents a choice of
actions. Agents have the freedom to bid whatever they think an item is worth, or
to vote for whatever they think is best. All agents together determine what the
outcome of the protocol is. In an ideal world, the protocol allows all participants
to reach an outcome that is ‘optimal’ in some sense: the protocol should be fair,
efficient, democratic, or otherwise meet some expectation. There are often many
different protocols for a certain problem. One can for instance sell a house by
asking all interested parties to submit a bid in a closed envelop, open all envelops
at the same time, and sell the house to the highest bidder. Alternatively, one
could have an open-cry auction, in which bidding continues until no agent wants
to bid higher than the current bid. Another option would be to have a lottery,
or an essay contest. It is often not immediately obvious which protocol is best.
Selecting the best protocol for a certain task is thus a relevant and sometimes
difficult problem.
game theorists have studied the properties of auctions [63]. Social choice scien-
tists have been working on voting protocols and fair division protocols [17]. These
related fields also have their own traditional applications. Fair division protocols
are can be used for cake cutting, but also for divorce settlements [17]. Economists’
examples are often more trade-oriented or money-oriented. Thus, an opportunity
exists here to take results and insights from computer science, and use them to
get improvements in applications outside the traditional scope of computer sci-
ence. We hope that knowledge about multi-agent protocols can be used to design
better solutions for the example scenarios described in this chapter.
One can distinguish ‘traditional’ approaches from computer science (and AI)
approaches by the fact that the computer scientists emphasise computational
properties. In the traditional approach one determines whether some solution
to a protocol problem exists. The computer scientists are also interested in the
question whether something can be computed efficiently. This emphasis on com-
putation can lead to interesting insights. Even though it has been proven that
no voting scheme is completely immune to manipulation [36], one can show that
in certain schemes it is very hard to compute how one should manipulate the
voting in order to get a required outcome [24]. In these schemes, it is unlikely
that someone can manipulate an election.
In this dissertation computational arguments are also used, but in a different
way. By comparing the complexity of different protocol verification problems,
one can determine what kind of goals are hard for agents to achieve, and which
properties are hard to verify. This leads to more insight into the causes of the
difficulty of protocol verification of design. For instance it is often assumed that
the interaction between agents makes games and protocols difficult. Sometimes
however also models with only one agent can have interesting computational
properties, which is a surprising result.
Logical Approach
In the examples of cake-cutting and charity auctions, it has become clear that the
properties that one wants protocols to have can be very diverse. In the second
example, parents actually wanted to contribute, while in the first example fairness
meant that agents would not choose to swap pieces. In some cases, for example
money-based auctions, one can reduce the quest for the right protocol to a nu-
merical problem: the problem is reduced to computing the optimal parameters,
or finding the right side payments. If this is not possible, for instance because
money is not available in the protocol, one must capture these properties in some
other precise way, before one can test protocols for these properties. Logical lan-
guages are very suitable for this task: one can describe complicated properties
in short logical formulas. Logics are also very expressive: one can state both the
presence and the absence of certain properties. Different logics are thus used as
specification languages: the formulas express what one wants or does not want
1.2. Protocol Problems 5
from a protocol.
Alice needs to buy one box of breakfast cereals every week. Each week
she can either buy Allgrain (A), Barley (B) or Cornflakes (C). She
likes A better than B and B better than C. However, Alice knows
that the shop is watching her shopping behaviour closely, and she
does not want the shop to know for sure what her preferences are.
Therefore, she buys a different brand every day.
The techniques presented in this chapter allow one to calculate the optimal (ran-
dom) strategies that agents should use if they are concerned about keeping their
preferences private.
• Chapter 5 introduces logics that are more expressive than efl. First of all
the logic efls can be used to express more subtle properties involving side
effects of using certain strategies. One way to look at this logic is by saying
1.3. Outline of this Dissertation 7
that it deals with the situation where agents are initially not aware of the
preferences of other agents, a situation that is not normally considered in
game theory. This logic can thus be used to express more properties of
game forms, but has the same model checking complexity as efl.
A second logic introduced in this chapter, called efls, allows one to reason
about agents that want other agents to be able to do something. This is an
example of reasoning about preferences on the whole play of the game, not
just on the outcome. One can apply this logic to reason about polite agents
that want to give other agents the ability to choose. This chapter extends
work presented at the AAMAS 2004 conference in New York [113].
These three chapter can be seen as an attempt to understand game forms using
more and more precise languages. For the logic efl many protocols appear to
be the same. The next two chapters offer logics that give more detailed views, so
that one can discover subtle differences in protocols.
Chapters 7 and 8 deal with the case where agents are not fully aware of all
aspects of the current situation. They have imperfect information about certain
facts. Since information is very important to agents, they might act in order to
get more information. In other situations agents act so that others obtain no
information.
A recurrent theme is this dissertation is the idea that agents can have complex
goals in a protocol, and that nondeterministic strategies can be used for achieving
these goals(see for instance the situation on page 89 where Bob makes Alice unable
to decide, or the quiz master example on page 134 where nature does not favour
the candidate). Normally in game theory agents have preferences over outcomes,
and the goal is to achieve a certain outcome. A complex goal on the other
hand depends on the whole game, including properties of the strategies used and
other outcomes than the actual one. For instance in chapter 5 agents care about
whether other agents can achieve outcomes or not. In knowledge condition games
coalitions act in order to make sure certain knowledge is achieved in the end, and
in chapter 8 agents care about how predictable their strategy is.
It is easiest to use strategies that recommend single best actions for any sit-
uation. These strategies are called pure strategies and are often sufficient for
reaching simple goals. In this dissertation we often use nondeterministic strate-
gies. These strategies can recommend multiple actions and are thus potentially
more powerful. In knowledge condition games and the privacy games of chapter 8,
agents can deliberately use these strategies to become unpredictable. In the logics
efls and efln these nondeterministic strategies are used because in many case
several actions are equally good. One cannot know beforehand which action an
agent will take in this case, so we model this uncertainty using nondeterministic
strategies.
1.4 Conclusion
Multi-agent protocols have not been discovered recently. The term can be used
to describe common situations, such as auctions, voting and cake cutting. These
protocols can be studied from different disciplines, such as game theory, eco-
nomics and social science. Furthermore one can test these protocols for many
different properties, for instance envy-freeness. The different frameworks and
logical languages defined in this dissertation make it possible to formally analyse
these multi-agent protocols, and to test them on many different properties. The
precision of a logical approach makes it possible in principle to use the computer
to find the right protocol for any situation. In this dissertation, it is determined
in which cases this is also practical. This is done by looking at the complexity of
these computing problems.
Chapter 2
Logic
2.1 Introduction
Logic is one of the oldest disciplines of science. It has been studied more or less
continuously from Aristotle to the present day. For example, it was an important
part of the Medieval academic curriculum: together with grammar and rhetoric,
logic formed the ‘trivium’, the relatively simple arts that one should master before
one could move on to the more advanced arts of the Quadrivium (arithmetic,
astronomy, geometry, and music) [122].
Given the rich history of logic, it is not possible to give a complete overview
of the area. The goal of this chapter is merely to provide the necessary defini-
tions of propositional, modal and epistemic logic that will subsequently be used
throughout this dissertation. For readers not so familiar with logic, this chapter
can serve as a concise introduction. For other readers, this chapter introduces
the notational conventions that I use in the remainder of this dissertation. First
propositional logic is defined. Then in section 2.3 modal logic and epistemic logic
are defined. In section 2.4 we discuss the different ways in which theorem proving,
satisfiability and model checking can be used for protocol verification.
A logic typically consists of three elements: the logical language, the semantics
and the proof system. A logical language is a set L of formulas. The semantics
is a relation between formulas and models, that says when a formula is true on
a model. If a formula φ is true on a model M we write M |= φ, otherwise we
write M 6|= φ. We are often interested in formulas that are true in any model,
and these formulas are called valid formulas, validities or tautologies. In order to
indicate that φ is a tautology, we write |= φ. If a formula φ holds in at least one
model, the formula is called satisfiable.
The final typical element of a logic is the proof system. Such a proof system S
consists of axioms and derivation rules and allows one to formally derive formulas.
2.1.1. Definition. Let L be a logical language. A proof system S is a pair
(A, R) where A ⊆ L and R ⊆ L∗ .
9
10 Chapter 2. Logic
The set A is called the set of axioms of S, and R is the set of reasoning rules. If a
proof system S proofs a formula φ, then we write S`φ. The notion of proof that
we use here is that of a finite list of statements S`φ1 , S`φ2 , . . . S`φn such that
each formula φi is either an axiom of S, or (φ( m1 ), . . . , φ( mn ), φi ) is a reasoning
rule of S, with m1 , . . . , mn < i. Thus, axioms count as self-evident, and the
reasoning rules allow one to derive a formula from formulas proven before.
All logics in this thesis make use of a symbol ¬ for negation of a formula. In such
logics, a formula φ is called consistent if its negation cannot be proven: S 6 `¬φ.
In a complete proof system (for a logic where negation is defined in the classical
way), every consistent formula is satisfiable.
Ideally, a proof system should be sound and complete. Furthermore, the
axioms and rules should not be arbitrary sets, but one should be enumerable
in an automatic fashion: a mechanical procedure should be able to generate all
axioms. In practice, this means that the sets of axioms and reasoning rules consist
of a finite number of patterns, so that any formulas can be inserted in the open
places of the pattern. This constraint ensures that one can effectively generate
all proofs, which means that there is a procedure to find all proofs and thus all
theorems.
Table 2.1 lists the languages and proof systems that are defined in this chapter.
sentence proposition
It rains p
It does not rain ¬p
The weather is good q
It rains and the weather is good p∧q
It rains or the weather is good p∨q
If it rains then the weather is good p→q
It rains if and only if the weather is good p↔q
It rains if and only if the weather is not good p∇q
Contradiction ⊥
Parentheses indicate how certain formulas are constructed, and can be used,
for instance, to make a distinction between (p → q) → r and p → (q → r). If no
parentheses are given then the second reading is intended: p → q → r should be
read as p → (q → r).
12 Chapter 2. Logic
This language is interpreted in the following way. A model M for this logic
is a subset of P . The atomic propositions in M are assumed to be true, the ones
that are not in M are false. The next definition determines when M |= φ for any
formula φ.
2.2.2. Definition. Let M ⊆ P be a model. The satisfaction relation |= for
minimal propositional logic is defined recursively by the following three rules:
M |= ⊥ never
M |= p where p ∈ P iff p ∈ M
M |= φ → ψ iff M |= φ implies M |= ψ
Like many logics, propositional logic is closed under uniform substitution.
This means that if one has a valid formula in which p occurs, and one replaces
all occurrences of p for any other formula φ, one again has a valid formula. For
example, since φ = p ∨ ¬p is valid, the formula ψ = ¬q ∨ ¬¬q is also valid. A
formula ψ that is obtained from φ by uniform substitution is called an instance
of φ.
In the remainder of this section we define a proof system Sp for the language
Lp . The next three formulas serve as the axioms for this proof system.
A1 = φ → (ψ → φ)
A2 = (φ → (ψ → ξ)) → ((φ → ψ) → (φ → ξ))
A3 = ((φ → ⊥) → (ψ → ⊥)) → (ψ → φ)
We have defined axioms as sets of formulas, and thus A1 to A3 are sets of formulas.
To be precise, A1 = {φ → (ψ → φ)|φ, ψ ∈ Lp }, but it is hoped that the notation
without set brackets is more readable. We can write φ ∈ Ai to indicate that φ
has the stated form. If φ ∈ Ai we say that φ is an instance of the axiom scheme
Ai .
Suppose that L is a logical language in which → has its usual interpretation.
If both φ and φ → ψ are validities in this logic, then ψ must be a validity as well.
This fact forms the basis of the reasoning rule Modus Ponens. The set M PL that
expresses this rule is the following.
M PL = {(φ, φ → ψ, ψ)|φ, ψ ∈ L}
A more traditional way of presenting this rule is the following.
φ φ→ψ
M PL =
ψ
2.2.3. Definition. The standard proof system Sp for minimal propositional
logic consists of the three axioms A1 , A2 , A3 and the rule Modus Ponens.
The system Sp is sound and complete for minimal propositional logic. A proof
of this claim is beyond the scope of this dissertation, but proofs for similar systems
can be found in logic textbooks, for instance [53].
2.2. Propositional Logic 13
φ ::= p | ⊥ | > | φ → φ | φ ↔ φ | φ ∨ φ | φ ∧ φ | φ ∇ φ
This full language is interpreted in the following way. The model M is again
a subset of the set of all propositions P .
M |= > always
M |= ⊥ never
M |= p where p ∈ P iff p∈M
M |= ¬φ iff not M |= φ
M |= φ ∨ ψ iff M |= φ or M |= ψ (or both)
M |= φ ∧ ψ iff M |= φ and M |= ψ
M |= φ ∇ ψ iff M |= φ or M |= ψ but not both
M |= φ → ψ iff M |= φ implies M |= ψ
M |= φ ↔ ψ iff M |= φ and M |= ψ or neither
It is not hard to show that under this interpretation the following formulas hold
14 Chapter 2. Logic
on any model M .
M |= > ↔ (⊥ → ⊥)
M |= ¬φ ↔ (φ → ⊥)
M |= (φ ∨ ψ) ↔ ((φ → ⊥) → ψ)
M |= (φ ∧ ψ) ↔ ((φ → ψ → ⊥) → ⊥)
M |= (φ ∇ ψ) ↔ ((φ → ψ) → (ψ → φ)) → ⊥)
M |= (φ ↔ ψ) ↔ ((φ → ψ) → (ψ → φ) → ⊥) → ⊥)
One can thus define all other operators in terms of the two connectives ⊥ and →.
Conjunction and disjunction have as a feature that changing the order and
nesting of these operators does not change their truth value: φ ∨ ψ is equivalent
to ψ ∨ φ, and (φ ∨ ψ) ∨ χ is equivalent to φ ∨ (ψ ∨ χ). These properties make it
possible to apply these operators to finite sets. Thus, we define a disjunction of
a set by _
{φ0 , φ1 , . . . , φn } = φ0 ∨ φ1 ∨ . . . ∨ φn
Similarly we define the conjunction of a set as
^
{φ0 , φ1 , . . . , φn } = φ0 ∧ φ1 ∧ . . . ∧ φn
2.2.5.VDefinition.
W A formula φ is in conjunctive normal form iff it has the form
φ = i j ψij , where ψij is of the form ψij = ¬a or ψij = a, for some atomic
proposition a ∈ P .
2.2.6.WDefinition.
V A formula φ is in disjunctive normal form iff it has the form
φ = i j ψij , where ψij is of the form ψij = ¬a or ψij = a, for some atomic
proposition a ∈ P .
Two example propositional logic formulas, one in conjunctive and one in dis-
junctive normal form, are the following.
For logics other than propositional logic, one can also define the notions of
conjunctive and disjunctive normal form in a similar way. For instance for modal
logic (defined in
V the
W next section), a formula is conjunctive form is a formula of
the form φ = i j ψij where ψij is either a or ¬a, for some formula a that is
either an atomic proposition, or of the form 2X φ.
2.3. Modal Logic 15
It is perhaps interesting to remark that this rule preserves logical truth, but not
actual truth. Thus, it is not the case that if φ is true in a situation, then 2X φ is
true in that situation. The theorem only claims that validity is preserved, which
is a weaker statement. This lemma can therefore not be used to introduce an
axiom along the lines of φ → 2X φ, but it can be turned into a reasoning rule.
This rule is called Necessitation.
For each consistent formula φ one can find a maximally consistent set S so
that φ ∈ S [12]. If the proof system S is sound, then for any pointed model M, w,
the set {φ | M, w |= φ} is maximally consistent.
In order to prove the theorem, consider a consistent formula φ with atomic
propositions from the set P . It is necessary to show that there is a model
M such that M, w0 |= φ. Such a model W = (Σ, W, R, P, π) can be con-
structed using maximally consistent sets as the worlds as the model: W =
{w|w is a maximally consistent set}. The relation RX is then defined such that
(v, w) ∈ RX if 3X φ ∈ v for all φ ∈ w, and π(w) = {p ∈ P |p ∈ w}. For w0 one
can take any maximally consistent set that contains φ. This construction defines
one large model M called the canonical model for a logic, such that any consis-
tent formula holds in some world of this model. This technique to use maximally
consistent sets as possible worlds not only works for plain modal logic, but can
often be adapted for modal logics with a different interpretation [12, p.194].
The multi-modal logic presented here is the weakest possible version of a
modal logic with a possible worlds semantics. The next table lists some formulas
that one might expect to hold for certain readings of the 2 operator, but that
cannot be proven in S2 .
The names 4, D and T are the standard names for these axioms [12, p.192]. One
can make these formulas valid by putting constraints on the relations RX . This
idea is used in order to get an epistemic reading in the next section.
It is often important to determine whether two models satisfy the same for-
mulas, and for this purpose the notion of bisimulation can be used. Two Kripke
models are bisimilar if one can find for any world in one model a corresponding
world in the other model. Such a relation between worlds is called a bisimula-
tion. A formal definition of this concept for single-agent modal logic would be
the following.
For logic with more than one agent one has to use a set of relations SX as bisim-
ulation. For simplicity reasons this extension has been omitted.
A bisimulation matches worlds that behave similarly with respect to modal
logic formulas. Thus, if M1 , w1 |= φ and (w1 , w2 ) ∈ S then also M2 , w2 |= φ.
In order to decide whether two models are equivalent one thus has to find a
bisimulation between the models, or prove that no such relation exists.
The next table lists some examples of formulas that hold over epistemic models
M.
|= KX φ → φ Truth
|= KX φ → KX KX φ Positive Introspection
|= ¬KX φ → KX ¬KX φ Negative Introspection
These validities can be used as axioms in a reasoning system for epistemic logic.
T = KX φ → φ
4 = K X φ → K X KX φ
5 = ¬KX φ → KX ¬KX φ
(prop ∪ K ∪ 4 ∪ 5 ∪ T, M P ∪ N ec)
This proof system is again sound and complete with respect to the given semantics
based on epistemic models. A proof can be found in epistemic or modal logic text
books such as [12, p.194]. The common name for this proof system is S5 or S5n
where n is the number of agents. This semantics is widely used because it is simple
and seems realistic for rational agents, but has also received criticism. First of all
there is the omniscience problem: all agents know all tautologies, so every agent
knows all mathematical theorems. This seems unrealistic in the case of human
agents, or artificial agents with a limited computing capacity. There have been
attempts to model knowledge while avoiding omniscience [32]. A second potential
objection is that it is not certain that humans have full introspection over all their
knowledge. Humans do not always know what they know, and especially it seems
doubtful that they have negative introspection. This is for instance stated in
Rumsfeld’s famous remark:
“There are known knowns. These are things we know that we know.
There are known unknowns. That is to say, there are things that
we know we don’t know. But there are also unknown unknowns.
There are things we don’t know we don’t know.” (D. Rumsfeld, USA
secretary of defense, Feb. 12, 2002)[92]
Philosophically there are many arguments against introspection [123]. In the
context of protocols, with a finite number of states and possibilities, it does
not seem to be a problem. It is not unreasonable to assume that agents have
introspection over a small, well-known domain such as the possible outcomes of
a protocol. It does not follow from this assumption that agents know everything
about the whole world, or are completely aware of omissions on their knowledge
in general.
2.3. Modal Logic 21
pq p
A
B B
A
q
Figure 2.2: Rain in Liverpool and Amsterdam: Model M1
one often does want to reason about this higher order knowledge, a stronger
notion of group knowledge is useful. Lewis therefore introduced the notion of
common knowledge [65]. Intuitively something is common knowledge if everybody
knows it, everybody knows that everybody knows it, everybody knows everybody
knows everybody knows it, etcetera. Common knowledge turns out to be a more
powerful notion than ‘everybody knows’. First of all it is hard to obtain, but
on the other hand it can be a necessary condition in order to coordinate [71] or
to make linguistic conventions work [65]. Other phenomena, such as the pricing
of TV commercials, can also be explained by the need of advertisers to achieve
common knowledge instead of plain knowledge [21].
The notation Cφ is used to convey that φ is common knowledge. It can be
defined in the following way. Let ∼C be the smallest equivalence relation such
that for all X we have ∼X ⊆ ∼C . We can interpret Cφ in the following way.
M, w |= Cφ iff ∀v : w ∼C v implies M, v |= φ
The following formulas are valid under this interpretation.
|= Cφ → CCφ
|= ¬Cφ → C¬Cφ
|= Cφ → C(φ → ψ) → Cψ
|= Cφ → Eφ
|= φ → E(φ → Eφ) → Cφ
The common knowledge operator C thus satisfies positive and negative introspec-
tion, which means that it behaves as a knowledge operator.
One can show that if a formula φ holds in every world w of a model M , then φ
is common knowledge in M . Thus, if we present a model of a certain situation in
which there is no state where φ does not hold, then we have implicitly assumed
that φ is common knowledge. In most examples in this dissertation, common
knowledge is not introduced in the language. However, common knowledge of at
least the protocol is assumed everywhere in this dissertation, and in some cases
also the preferences of agents are common knowledge.
protocol model
⇔
property formula
What is meant here is that protocols correspond to models, and properties
with formulas. The double-headed arrow indicates that one can go back and forth
from the informal description on the lefthand side to the formal description of
the situation on the righthand side.
Model checking was first done for properties involving time [22, 10]. One rea-
son that model checking has become popular is the invention of symbolic model
checking [69]. Using this technique the model that is checked is not stored explic-
itly, but represented in a symbolic way, using for example ordered binary decision
diagrams. The model can thus have more states than one can store explicitly in
the memory of the computer that is used. The use of symbolic model checking has
made it possible to check systems with billions of states, instead of only millions
of states. Recent work aims to develop model checking techniques for epistemic
properties [104, 101, 56].
For some logics one can use theorem proving for system verification. This is
possible if one can translate the system into a formal structure (for instance a tree
or a graph) and then describe this structure using a formula φ1 . The property
to be verified is represented by a formula φ2 , and one uses the theorem prover
to prove that `φ1 → φ2 . This results into a proof that any system of the given
structure has the desired property. Schematically one can display this in the
following way.
24 Chapter 2. Logic
protocol φ1
⇔
property φ2
Hence both the protocol and the property correspond to a formula. This
method of verification by theorem proving is only possible for logics in which
one can express the structure of a system. For some logics, such as Pauly’s
coalition logic [85] (discussed in section 3.4), this is possible because the logic has
a modal operator that corresponds to exactly one step in the protocol. Thus,
one can construct, for each game tree T describing a protocol, a formula φ1 that
describes this game tree. For other logics, such as Van Benthem’s logic for process
models [99], also discussed in section 3.4, this is not possible. In this logic game
trees cannot be described in detail, and hence no suitable formula φ1 can be
found.
Another long term goal in computer science is the automatic design of systems.
In this case the user indicates the properties that a system, protocol or program
must have, and the computer constructs a system. One can always use the AI-
heuristic ‘generate and test’ in order to solve this problem, but this heuristic is
not very efficient. In general this problem is more difficult than verification, just
as satisfiability is more difficult than model checking: again one has to construct
something, instead of just computing a yes-no answer.
In economics, the classical name for the problem of finding a suitable auction
or procedure is mechanism design [83]. This problem has been picked up by com-
puter science researchers, and several researchers are now active in the area called
automated mechanism design or computational mechanism design [29, 25]. For
all logics in which models can be seen as representing a system, the mechanism
design problem can be reduced to satisfiability checking. Unfortunately satisfi-
ability checking is often a difficult problem, and hence mechanism design using
logical methods is often hard as well.
2.4.1. Definition. The logic LTL contains formulas φ generated by the follow-
ing rule. In this rule, p is a typical element of P
φ ::= p | ⊥ | φ → φ | φ U φ | fφ
2.4. Theorem Proving, Satisfiability and Model Checking 25
The sequences of states that are considered for LTL are not always finite. There-
fore, it is more convenient to use functions f : N → 2P as sequences. These func-
tions assign subsets of true atomic propositions to each natural number. Such a
sequence is called a history or a run. Each formula φ is interpreted over a pair
f, n where f is such a function, and n ∈ N indicates the current state.
f, n |= ⊥ never
f, n |= p where p ∈ P iff p ∈ f (n)
f, n |= φ → ψ iff f, n |= φ implies f, n |= ψ
f, n |= fφ iff f, n + 1 |= φ
f, n |= φ U ψ iff ∃m : m ≥ nf, m and |= ψ and ∀m > k > n : f, k |= φ
The ‘until’ operator φ U ψ indicates that at some point in the future ψ is true,
and until that time φ holds. The next operator fφ expresses that φ is true at the
next state. A commonly defined shortcut is the ‘sometimes’ operator 3φ = > U φ
that indicates that φ is true somewhere in the future. One can define an ‘always’
operator 2φ that indicates that φ holds forever from now on, with the following
definition: 2φ = ¬3¬φ.
A system to be verified is not modeled as a single run but as a set of runs.
Since these runs can be infinite, such a set must be specified implicitly. The
most common way to do this is to define a labeled graph (V, E, π) where π is a
function from V to 2P . A possible path in this graph is a sequence w : N → V
such that (w(n), w(n + 1)) ∈ E for all n ∈ N. Any possible path w defines a
possible run f : n 7→ π(w(n)). A shorthand notation for this is f = π(w), since
f (n) is constructed by first computing w(n), and then applying π to the result.
Let W be the set of all possible paths, and R the set of all possible runs.
A model checker for LTL takes a description of a system and an LTL formula
φ. From the description it computes a set of possible runs R, and then it checks
whether for all runs r ∈ R it is the case that r, 1 |= φ. If so the model checker re-
turns true, otherwise the model checker returns the run r such that r, 1 |= ¬φ. An
LTL model checker thus returns counter-examples that can be very informative
for system designers. A well-known model checker for LTL is SPIN [51].
2.4.2. Definition. The logic CTL contains formulas φ generated by the follow-
ing rule. In this rule, p is a typical element of P .
φ ::= p | φ → φ | ⊥ | ∀ψ | ∃ψ
ψ ::= 2φ | φ U φ
The formulas φ generated by the grammar rules stated above are called state
formulas because they are interpreted over states. The formulas ψ are called
path formulas, because they are interpreted over paths. As the name indicates
this logic can be interpreted over tree structures, where the nodes of the tree
are states of a system, and the edges indicate how the system can go from one
state to the next. Typically such a tree is constructed by considering all possible
paths through a labeled graph (V, E, π), combined in a set W. Each path w
is a finite sequence w(1)w(2) . . . w(n) or infinite sequence w(1)w(2) . . . of states
w(n). Thus the notation w = v... ∈ W is used to indicate that w is an infinite
path that starts in v. CTL formulas φ can be interpreted over a set of paths
combined with an interpretation function π : V → 2P and a current state v ∈ V .
The path formulas are however interpreted over a set of paths combined with an
interpretation function π : V → 2P and a current path w ∈ W.
W, π, v |= ⊥ never
W, π, v |= p where p ∈ P iff p ∈ π(v)
W, π, v |= φ1 → φ2 iff W, π, v |= φ1 implies W, π, v |= φ2
W, π, v |= ∀ψ iff ∀w = v... ∈ W : W, π, w |= ψ
W, π, v |= ∃ψ iff ∃w = v... ∈ W : W, π, w |= ψ
W, π, w |= 2φ iff ∀n ≥ 1 : W, π, w(n) |= φ
W, π, w |= φ1 U φ2 iff ∃m ≥ 1 : W, π, w(m) |= φ2 and
∀k : m > k ≥ 1 ⇒ W, π, w(k) |= φ1
Both CTL and LTL can be model checked in polynomial time in terms of the
number of states of the system [90]. This makes the verification of systems feasi-
ble. Unfortunately, the number of states of a system can increase exponentially
with the number of components, or the amount of memory cells, that a system
has. The conclusion that model checking is tractable, is thus perhaps somewhat
misleading, since model checking is intractable when the input is measured in the
size of the description of the system. Summarizing and interpreting the current
state of the art, one could say that model checking using LTL and CTL is feasi-
ble, but not (yet) very tractable for real world systems. In practice, techniques
like symbolic model checking and other heuristics can be used to make model
checking for ever larger systems feasible.
2.5. Computational Complexity 27
uses these words as meaning ‘solvable in polynomial time’. The term intractable
means that the problem is not in the class P.
Nondeterministic Computation
There are many decision problems f such that f (d) = 1 if there exists some object
w that satisfies certain criteria. A good example is the problem, for a given
graph, to decide whether this graph has a Hamiltonian cycle. A Hamiltonian
cycle visits each node of the graph, but does not use the same edge twice. In
figure 2.3, Hamilton’s original problem is displayed. In this particular graph
there is a Hamiltonian cycle, and the reader is invited to find one as an exercise
(a possible answer is displayed in figure 2.4 on page 29). The reader will most
likely experience that finding a Hamiltonian cycle is harder than verifying that a
given path is a Hamiltonian cycle.
Suppose that the problem f : Prob → {0, 1} is defined such that f (d) = 1 iff
d is a graph that has a Hamiltonian cycle. Suppose also that we have a problem
g ∈ P that checks whether a path w is a Hamiltonian cycle on d. The relation
between f and g is that f (d) = 1 ⇔ ∃w : g(d, w) = 1.
The Hamiltonian cycle w is called a witness for d, since the existence of a
path w is evidence for the fact that f (d) = 1. We have assumed that g ∈ P, and
hence that we have a polynomial time algorithm for g. A very naive algorithm for
solving f would be the following. Guess some value w, and check whether g(d, w).
If you are very lucky in guessing w, then this algorithm works in polynomial time
as well. If you are not a good guesser, this algorithm is not efficient.
Any problem f for which there exist a polynomial time function g that checks
witnesses, is called solvable in nondeterministic polynomial time [26]. The class
of these problems is called NP . There are many problems that have practical
relevance in this class [35]. A logical example of an NP problem is the proposi-
30 Chapter 2. Logic
This was the first theorem to be proven NP-complete, presented in 1971 [81, p.
176]. The proof contains a general method how a reduction function r can be
found for any NP decision problem that has a verification method g. Such a
general proof has to be given once for each class. In order to prove that another
problem in NP is NP-complete, it suffices to select a known NP-complete problem,
and then give a specific reduction function r from the complete problem to the
next problem.
In many NP-completeness proofs it is convenient not to use the general sat-
isfiability problem in a reduction argument, but to give a reduction from 3-CNF
formulas. A formula φ is in 3-CNF if it is in conjunctive normal form, and each
disjunction contains exactly three literals. Such a formula thus has the following
form. ^
φ = (±ai ∨ ±bi ∨ ±ci )
i
For the class PSPACE, we also use a logical problem in the reduction argu-
ments. We use the satisfiability problem for a quantified boolean formula, since
this problem is PSPACE-complete.
2.5.2. Definition. A quantified boolean formula φ is a formula of the form
The QBF decision problem f is defined such that for any quantified boolean
formula φ we have
f (φ) = 1 if ∅ |= φ
f (φ) = 0 otherwise
The completeness proof for this problem was presented in 1973 [81, p. 487].
The satisfiability problem for propositional logic is of course a special case
of the QBF problem, where we allow only existential quantifiers. Instead of
considering whether p → q is satisfiable, one can consider the QBF problem of
deciding whether ∃p∃q(p → q) holds. Similarly one can consider other restrictions
on the number of quantifier series in a QBF problem. The following table lists a
few variants.
∃p1 . . . ∃pn φq satisfiability, in class Σ1 P or NP
∀p1 . . . ∀pn φq tautology, in class Π1 P or co-NP
∃p1 . . . ∃pn ∀q1 . . . ∀qn φq Σ2 P
∀p1 . . . ∀pn ∃q1 . . . ∃qn φq Π2 P
...
32 Chapter 2. Logic
The classes Σn P and Πn P are defined using oracles. A Turing machine with
an oracle is a machine that is allowed to ask certain difficult questions to a
supernatural being (an oracle). The oracle returns the right answer to these
questions in one time step. The class Σ2 P contains problems that can be verified
by a Turing machine that has an oracle for some NP-complete problem. The
problems given above are again complete for these classes: any Σ2 P problem can
be reduced to a QBF problem of the form ∃p1 . . . ∃pn ∀q1 . . . ∀qn φq [81, p. 428].
Open Problem
Intuitively it seems easier to verify a problem than to solve it. For instance it is
easy to see that the path given in figure 2.4 is a Hamiltonian cycle, whereas it
is less easy to find such a path. It is therefore widely believed [35] that not all
NP problems can be solved in polynomial time, and thus that no NP-complete
problems can be solved in polynomial time. If we assume that this is the case,
then NP-complete problems are intractable, and the same holds for the classes
Σ2 P and PSPACE. Unfortunately whether P 6= NP is one of the most famous
open problems in computer science [26].
In this dissertation we show for several problems that they are NP-complete,
Σ2 P complete or PSPACE-complete, and we use this as evidence for the in-
tractibility of these problems. Of course this is only partial evidence, since it is
still possible that all problems in NP, contrary to popular belief, are tractable.
Chapter 3
Game Theory
3.1 Overview
One can define game theory as the area of mathematics that is about games. In
this case, game theory is older than most people think. In the sixteenth century
the mathematician and physician Jerome Cardano wrote his Book on Games of
Chance [78]. The book opens with a statement describing the various forms that
games can take.
As Cardano indicates, certain games can depend on both skill and luck at the same
time. Nowadays Cardano’s book is classified as being about probability theory,
as opposed to game theory. The reason for this is that his book is concerned
with calculating the probabilities of certain events, but does not consider various
strategies and the influence of an opponents’ strategy.
The origin of game theory is therefore better placed in the first half of the
twentieth century. One of the first mathematical papers that focused on the
strategic aspects of games was Zur Theorie der Gesellschaftspiele by John von
Neumann [118]. The central question of this paper is about the optimal strategies
for players in a parlour game.
John von Neumann also co-authored the first book on game theory, Game
theory and economic behaviour, which appeared in 1944 [74]. The title already
33
34 Chapter 3. Game Theory
indicates that game theory is not merely about recreational games, but can be
applied to economics. Von Neumann and Morgenstern see a game as an optimisa-
tion problem in which multiple parties simultaneously try to optimize their own
outcome. According to them, this is ‘nowhere dealt with in classical mathemat-
ics’ [74, p.11]. This influential book introduced game theory to a wide audience,
summarized results that were ‘already known, but lacked formal proof’ [74, p.6]
and gave many game-theoretic terms their meaning.
The following list contains some of the terms introduced by Von Neumann
and Morgenstern.
A game: A description of a set of interactions between agents. The description
should include which agents can participate, what these agents can do, and
what these agents try to achieve.
A solution: ‘plausibly a set of rules for each participant which tell him how to
behave in every situation which may conceivably arise.’ [74, p31]
The words ‘game’ and ‘play’ still have the same meaning in most of the literature.
The word ‘player’ is nowadays often replaced by the synonym ‘agent’. A possible
reason for this change of terminology is that the word ‘player’ reminds people of
recreational games, whereas game theorists often consider less leisurely situations.
An agent can be a human player, but also an organisation or a computer program.
3.1. Overview 35
The word ‘solution’ should be used with caution. Not every game has a unique
solution, so the phrase ‘the solution of a game’ is misleading. A solution is
always a set of rules for all players. A set of rules for a single player can be called
a strategy, and if it is a good set of rules it can be called an ‘optimal’ or ‘rational’
strategy.
In order to decide what the best set of rules for an agent is, one must take
into account what information the agent has. First of all, it is important to know
whether the agent knows exactly which game it is playing. Even the game of
chess has several variants, and one can imagine a player who is not sure what
the current variant is. Furthermore, in chess an opponent can try to win at all
cost, or an opponent can be trying to draw. These two opponents may require
different strategies. Von Neumann and Morgenstern boldly state that
... we cannot avoid the assumption that all subjects of the econ-
omy under consideration are completely informed about the physical
characteristics of the situation in which they operate and are able
to perform all statistical, mathematical, etc., operations which this
knowledge makes possible. [74, p.30].
should collectively aim for, and how they should split the profits of their collab-
oration. Throughout this thesis it is not assumed that agents can make binding
agreements, and this is called non-cooperative game theory.
The problem of how to treat general games was addressed by John Nash in
1951 [73]. Nash showed that a solution of a game should be a set of strategies
such that when all agents use these strategies, no player has any incentive to use
another strategy. He called such a solution an equilibrium, and nowadays it is
called a Nash equilibrium.
The Nash equilibrium is a solution concept that allows the same game to have
many solutions. A solution concept is a general rule that for each game predicts
which strategies are good. Many researchers have argued that the Nash equilib-
rium allows more solutions than it should. Various refinements have thus been
proposed. One of the first was Selten’s subgame perfect (Nash) equilibrium [79].
This concept makes most sense when applied to perfect information extensive
games. Every decision point of such a game can be seen as the starting point
of some game, and these games are called the subgames of the original game.
Selten argued that a solution should not only be an equilibrium of the original
game, but also of every subgame. All finite perfect information extensive games
have a subgame perfect equilibrium, and this equilibrium can efficiently be calcu-
lated by a procedure named backward induction. The procedure is sometimes also
called Zermelo’s algorithm, since Zermelo applied the same procedure in 1913 to
analyse chess. Other refinements exist, for instance the trembling hand perfect
equilibrium [93], the proper equilibrium [72] and the sequential equilibrium [62].
Even though Von Neumann and Morgenstern limited themselves to the study
of complete information games, it was only a matter of time before incomplete
information games were considered. Harsanyi proved in 1967 that incomplete
information games can in certain cases be reduced to complete, imperfect infor-
mation games [47]. He did not assume that all agents know all other’s preferences.
Instead he assumed that each agents’ preferences depended on the type of the
agent. The number of types was limited, and a probability distribution for the
types should be commonly known. In that case the incomplete information game
can be considered an imperfect information game where in the first move the
types of all agents are determined at random according to the given probability
distribution. After that the game would proceed as normal.
The applications of game theory have not been limited to the economic realm.
Early on it was already realized that game theory could be applied to political and
military conflict situations. An early and influential book applying game theory
to political science is The Strategy of Conflict by Thomas C. Schelling [88]. This
book contains various ideas. First of all Schelling showed using experiments that
people are able to coordinate their actions. They can do this because real world
problems have so-called focal points, even if these points are no longer present in
the abstract models of game theory. For example, Schelling asked people to try to
meet each other on a given day in a given city, without giving them a specific time
3.2. Strategic Games 37
and place, and without allowing them to communicate to each other. One might
expect that this is not possible, since there are so many possibilities. However,
Schelling’s subjects were remarkably successful in meeting each other. Many of
them were able to select the same time and place, by reasoning about which
points were most obvious to the average person. For instance for a meeting in
New York, people often choose to meet at 12.00 at Central Station. Schelling
also discusses the rationality of promises and threats. An equilibrium that is not
subgame perfect, can for instance contain an unreliable threat. In that case a
player threatens to do something in a certain situation, even though it is not
rational to really do this action if the subgame in which the action can be done
is reached.
More surprising applications were found in biology. This may seem strange, as
animals or plants are not usually ascribed rationality or intelligence. The players
are thus not assumed to reason about their strategies, but to repeat behaviour
that has been successful in the past. The Nash equilibrium can also be applied
in these circumstances. In classical game theory attention is focused on the
solutions itself, whereas the process by which a solution is reached is ignored. In
evolutionary game theory it is also studied how certain strategies are replaced
by others, using dynamic systems theory. John Maynard Smith is one of the
originators of this field [68]. Evolutionary game theory is a maturing and popular
research area [37, 120].
The utility function UX takes a strategy for each agent as input, and return a real
number for agent X, which represents that agent’s utility. The notation UX (~s)
38 Chapter 3. Game Theory
denotes the Xth element of the vector U(~s), and thus represents the utility of
agent X when the strategy profile ~s is used. One can see U as a function that
returns a vector of real numbers, one for each agent.
In a strategic game, each agent tries to maximize its utility. They can choose
any strategy from their set of strategies, and these sets can be infinite. One can
combine the strategies that agents have chosen in a so-called strategy vector . A
tuple ~s = (s1 , s2 , . . . , sn ) is a strategy vector for game G if G = (Σ, {S X }X∈Σ , U)
and for all agents X we have sX ∈ S X . In order to manipulate these strategy
vectors, two constructs are needed. The construct s−j denotes the vector s with
the jth element removed. Thus, (a, b, c)−2 = (a, c). The construct [s, x] is used
to denote the vector s with x inserted in an appropriate place.
For example [(a, c), d] = (a, d, c), or [(a, c), d] = (a, c, d), depending on what is
appropriate. Determining what the appropriate place is can be difficult, therefore
the construction [s, x] can only be used if s is of the form s−X for some agent X.
For example [(a, b, c)−2 , d] = (a, d, c). In practice this means that these constructs
can be used to replace one strategy of a strategy vector by another strategy. The
combination [s−j , tj ] or, depending on author’s preferences, (s−j , tj ) is standard
in game theory [79, p. 7].
In many situations, every agent X has a finite number of basic actions mi to
choose from. The total utility of a strategy somehow depends on the payoff of
each action. The number of strategies can still be infinite. The payoff of each
action is typically given in the form of a matrix A. We first present the case for
two agents, and then extend this to an arbitrary number of agents.
The next table shows how a 2 × 3 bi-matrix is usually displayed. This matrix can
be used to define a game where agent 1 has two actions, and agent 2 has three
actions.
1
A (1, 1), A2 (1, 1) A1 (1, 2), A2 (1, 2) A1 (1, 3), A2 (1, 3)
In a pure strategy game, the strategy of both agents consists of a single action.
We can use the bi-matrix A given above to define a pure strategy game G =
({1, 2}, ({1, 2}, {1, 2, 3}, T ), U). The set of agents would be {1, 2}, the strategy
set of agent 1 would be {1, 2}, and the strategy set of agent 2 would be {1, 2, 3},
and the utility function would be defined by U(a, b) = (A1 (a, b), A2 (a, b)).
In a mixed strategy game, a strategy consists of a probability for each ac-
tion. Thus a mixed strategy game G based on the bi-matrix A would be G =
3.2. Strategic Games 39
({1, 2}, (S 1 , S 2 ), U), where S 1 = {(a, b)|a, b ∈ [0, 1], a+b = 1} and S 2 = {(a, b, c)|a,
b, c ∈ [0, 1], a + b + c = 1}. An example strategy for player 1 would be (0.25, 0.75).
If the agent follows this strategy it should take action 1 twenty-five percent of
the time, and action 2 seventy-five percent of the time. The utility function U
returns the expected payoff, and is defined as
Multi-player games
3.2.3. Definition. An m1 × m2 . . . × mn multi-matrix is a function A such that
for each vector a1 a2 . . . an where aY ∈ {1, . . . , mY } for all Y ∈ {1, . . . , n}, and for
each X ∈ {1, . . . , n}, the function A returns a real number AX (a1 i2 . . . an ) ∈ R.
3.2.4. Definition. For any multi-matrix A, agent X and action i, and vector ~s
of mixed strategies sY for each agent Y , we define the expected payoff of action
i for agent X by:
X
AX
i (~
s ) = ((s1 )v1 · · · (sX−1 )vX−1 (sX+1 )vX+1 · · · (sn )vn )AX (~v )
(v1 ...vn )∈ViX
40 Chapter 3. Game Theory
In this definition, the element v1 denotes a possible action for player 1, s1 is the
strategy of player 1, and therefore (s1 )v1 denotes the probability that player 1
will play action 1. Although this definition is hard to read, in practice it is not
hard to see how this expected payoff is computed. To give an example, let A be
again a 2 × 2 multi-matrix, assume that the first player plays action 1 with ninety
percent probability, and that the second player plays the first action with forty
percent probability. Then the expected payoff of action 2 for agent 1 is computed
in the following way.
Recall that the notation UX (~s) denotes the Xth element of the vector U(~s). It
represents the utility of agent X when the strategy profile ~s is used.
The fact that agents can play mixed strategies is explicitly defined in this
definition of a mixed strategy game. We assume that all agents are equipped with
random number generators (coins, dice or whatever) so that they can randomize
their behaviour exactly as specified in their strategy. This definition of a mixed
strategy game is such that each mixed strategy game is in fact a strategic game.
For the next definition we need the function argmax that returns all inputs
that maximize a given function. argmaxx f (x) = {x|¬∃y : f (x) < f (y)} We
use the function argmax to define what a ‘good’ strategy is: A good strategy
is a strategy that returns a maximal utility. The function bX returns the best
response strategies for agent X for a given game and strategy vector.
The set b(~s) thus contains the strategy vectors t such that tX is optimal if all
opponents Y use the strategy sY . We could assume that the strategy of the
opponents is fixed. The set bX (~s) is the set of best decisions for agent X.
When playing a game an agent cannot always predict what strategy the other
agents use, because the other agents might want to change their strategy once
3.3. Extensive Games 41
they learn that X uses a strategy in bX (~s). The notion of a best response is
therefore not a solution concept in itself. One can however search for fixed points
in the best response function, and this is called a Nash equilibrium.
Every mixed strategy game has at least one Nash equilibrium [73]. There has
been some discussion in the literature whether the notion of a Nash equilibrium
needs to be refined. Several refinements have been proposed [72], but none of
them has the appealing simplicity of the Nash equilibrium.
A special class of games for use in logic are the win-loss games. In these
games the utility functions only takes two values, which can be associated with
winning and losing. Typically these values are 1 and 0. The utility function can
then be specified by stating what the winning positions are. These sets can then
be specified by stating a formula, so that a position is winning if it makes the
formula true.
Another special class are the constant-sum games. We define this property
only for games with exactly two players. A game ({A, B}, {S A, S B }, U) is a
constant-sum game if there is a constant c ∈ R such that for any strategy profile
(σA , σB ) it is the case that UA ((σA , σB )) + UB ((σA , σB )) = c. If the constant c is
0 then we call it a zero-sum game. The next bi-matrix A defines a constant-sum
game where the constant is 2.
1, 1 0, 2 2, 0
2, 0 1, 1 0, 2
Examples of strategic games can be found in many game theory text books.
All classical examples can be found in the primer by Osborne and Rubinstein [79],
but more playful examples are given by Binmore [11]. Textbooks on evolutionary
game theory such as Gintis’ [37, 120] also make much use of strategic form games.
In each case the examples of strategic games are often presented in the form of
finite multi-matrices, and this can give readers the false impression that strategic
games are always finite, small and simple. In chapter 8, it is shown that there
are many other strategic games that do match definition 3.2.1, but are not pure
or mixed strategy games.
a b a b b b b b
a b a a a b
a b a b
A game form by itself is often not what one needs. One typically want a game
form with a utility function (if you are a game theorist) or a game tree annotated
with atomic propositions (if you are a logician). In certain cases you might want
both. We use the word ‘interpreted’ to indicate a structure that is labeled with
atomic propositions. If a structure contains utilities it is called an extensive game,
otherwise a game form.
3.3. Extensive Games 43
name contains
(extensive) game form tree
interpreted game form tree, atomic propositions
extensive game tree, utility function
interpreted game tree, utility function, atomic propositions
The word ‘extensive’ emphasizes that we deal with games in which the order of
moves is explicitly present. We omit it if it is not necessary, and thus we speak
of game forms rather than extensive game forms. An extensive game form is
thus synonymous to game form, and so are interpreted extensive game form and
interpreted extensive game.
3.3.3. Definition. An extensive game F is a tuple F = (Σ, H, turn, U), such
that (Σ, H, turn) is a game form and U : Z(H) × Σ → RΣ .
The function U is called a utility function. It returns the utility for each agent
and each agent tries to maximize its utility.
3.3.4. Definition. Let (Σ, H, turn) be a game form. A pure strategy σ for agent
X in game form F is a function σ with domain {h ∈ H|turn(h) = X} such that
σ(h) ∈ A(H, h).
The notion of a strategy can be extended to strategies for coalitions Γ ⊆ Σ. A
pure coalition strategy σΓ for Γ is a function f with domain {h ∈ H|turn(h) ∈ Γ}
such that σ(h) ∈ A(H, h).
The notion of a strategy for a coalition Γ ⊆ Σ can also be introduced for be-
havioural and nondeterministic strategies.
For each game form F , we define SpX (F ) to be the set of pure strategies of
agent X in F , the set SbX (F ) to be the set of behavioural strategies of X in F , and
44 Chapter 3. Game Theory
p(~s, ) = 1
p(~s, ha) = ~s(h)(a) · p(~s, h)
A
i
B
c
c i
1 2 0
2 1 0
The two Nash equilibria of this game are indicated in bold. In the lower left
equilibrium, A ignores the problem and B cleans the room (payoff (2, 1)). In the
other equilibrium B plans to ignore the problem and A cleans the room (payoff
(1, 2)). Are both of these Nash equilibria equally good? Many people tend to say
‘no’. The reasoning is as follows. Each decision node of an extensive game can
be seen as the starting point of a smaller extensive game. Such a game is called
a subgame of an original game. One would expect each agent to act rationally
in each subgame. If an equilibrium has such a property, it is called a subgame
perfect equilibrium.
This definition can be extended to interpreted game forms, games and interpreted
games in a straightforward way. The set of all subgames of a given game is defined
as the set allsub((Σ, H, turn, U)) = {subg((Σ, H, turn, U), h)|h ∈ H}.
The example game of figure 3.3 has one subgame perfect Nash equilibrium in
which agent B cleans the office. The other Nash equilibrium is not subgame
perfect, since it is not optimal for agent B to choose the action ignore if A does
not clean the room.
3.3.11. Theorem (Kuhn). Every perfect information game has at least one
subgame perfect equilibrium in pure strategies [64].
46 Chapter 3. Game Theory
A
y n
B B
B
y y
n n
B C
If the utility function U of a game G is such that for any agent X and history
h ∈ Z(h) we have that h 6= h0 ⇒ UX (h) 6= UX (h0 ) then the optimal action a in
a certain situation is always unique, and thus the subgame perfect equilibrium is
unique.
Examples
Agent C in game form FI does not ave perfect memory. The agent can distinguish
y and n (thus y 6∼C n), but it cannot distinguish yn and nn (hence yn ∼C nn).
In the game form FI , agent B can forget its own action, since yy ∼B yn. Thus
the game form FI does not have the property and hence does not have perfect
recall.
The assumption of perfect recall makes it easier to compute Nash equilibrium
strategies. In fact, for two player constant-sum games with perfect recall, one
can find Nash equilibrium strategies in polynomial time. If perfect recall is not
assumed, the problem is Σ2 P-complete and thus believed to be intractable [57].
48 Chapter 3. Game Theory
completeness results for certain basic semantics. Rescher [86] also developed a
semantic for Von Wright’s language, this time based on the fact that the value
of a formula φ (in a certain model) should be the average of the utilities of all
worlds in the model that satisfy φ. This is certainly an interesting idea, but hard
to characterize in an axiomatic way. Chisholm and Sosa [20] investigated the
philosophical aspects of preference logic further. A recent overview is presented
by Hansson [44, 320].
What these sources have in common is that they use a binary construction
φP ψ in order to express preferences. This is different from the usual modal logic
approach, which is normally based on an unary operator 2φ (see for instance [45]).
The binary approach seems to correspond better with natural language, where
one can say things such as “I prefer coffee over tea”. The sort of relations that
is used to indicate preferences can also be used to express relative likelihood [42].
As a result, the technical results stated in terms of likelyhood can be applied
to preferences. Huang [52] also introduces preference logics, in order to model
agents with bounded rationality.
Another way to combine logic and games is to interpret a formula as a game
between two players, one of which wants to reach a ‘true’ outcome, the other one
a ‘false’ outcome. This idea has been used in the interpretation of independence
friendly logic (IF logic). This logic was introduced by Hintikka with the bold
goal of replacing first order logic as the primary logic of scientific discourse [49].
This idea has not materialized, partly because IF logic is quite complicated, and
has several interesting ‘features’ (that some call ‘bugs’). It has a compositional
semantics but it is not the simplest semantics [50], for this logic the falsity condi-
tions are not the mirror image of the truth conditions [31], and one can question
whether the interpretation of IF is faithful to game theory [94].
φ ::= p | φ → φ | ⊥ | [Γ]φ
Coalition logic is interpreted over general game frames, which combine features
of strategic games and extensive games. A general frame is similar to a tree, but
at each decision node all agents have to select an action, like in a strategic game.
The next state depends on the actions chosen by all agents. This semantics is
described in detail in Pauly’s dissertation [84, p.46]. This class of models is more
general than the interpreted game forms that are used for efl. The interpretation
50 Chapter 3. Game Theory
The following rules define the interpretation of coalition logic formulas over
pointed models M, s, where s ∈ S is a state in the coalition model M
G, s |= ⊥ never
G, s |= p for p ∈ π(s)
G, s |= φ → ψ iff not G, s |= φ or G, s |= ψ
G, s |= [Γ]φ iff φG ⊆ EΓ (s)
where φG = {t ∈ S|G, t |= φ}
This logic does not make a distinction between intermediate states and end states
or outcomes. The internal structure of the protocol can therefore be described in
coalition logic, and one can use satisfiability for protocol verification.
The fact that coalition logic does take intermediate states into account, means
that one should read formulas from efl and coalition logic in a different way. In
chapter 4 we see that the efl formula [A]2p expresses that A can enforce that
a p outcome is reached. Syntactically the closest coalition logic formula is [A]p.
This formula means A can make p true in the next state. If the next state is not
an outcome state, then this formula does not say anything about which outcomes
A can reach. In order to express something about outcomes, one can however
use extended coalition logic. This logic is an extension of coalition logic with
operators [Γ∗ ]φ and [Γ× ]φ. The first operator expresses that φ can eventually be
reached by Γ, and the second operator [Γ× ]φ expresses that Γ can keep φ true in
the entire future. The first operator can be used to refer to outcome states, and
indeed Pauly introduces a special notation to do so.
Proof Theory
There are sound and complete proof systems for several variantes of Coalition
logic. The full details are given by Pauly [85, 85]. Here we present as an example a
sound and complete proof system for coalition models that have a weakly playable
effectivity function.
S
3.4.3. Definition. An effectivity function EΓ : S → 22 is Γ-maximal iff for all
T , if S \ T ∈
/ EΣ\Γ then T ∈ EΓ
3.4. Existing Work on Logic and Games 51
S
3.4.4. Definition. An effectivity function EΓ : S → 22 is superadditive iff
for all T1 , T2 , Γ1 , Γ2 such that Γ1 ∩ Γ2 = ∅, if X1 ∈ EΓ1 and X2 ∈ EΓ2 then
X1 ∩ X2 ∈ EΓ1 ∪Γ1
S
3.4.5. Definition. An effectivity function EΓ : S → 22 is weakly playable if it
/ E(Σ), (2) if ∅ ∈ E(Γ) and Γ0 ⊂ Γ
satisfies the following five conditions: (1) ∅ ∈
then ∅ ∈ E(Γ0 ), (3) If ∅ ∈/ E(∅) then S ∈ E(Γ) for all Γ ⊆ Σ, (4) E is Σ-maximal
and (5) E is superadditive.
These following axioms are sound on coalition models with weakly playable
effectivity functions.
|= ¬[Σ]⊥ (N ⊥)
|= [Γ ∪ Γ2 ]⊥ → [Γ]⊥ (⊥)
|= ¬[∅]⊥ → [Γ]> (>)
|= ¬[∅]¬φ → [Σ]φ (N )
|= ([Γ1 ](φ1 ) ∧ [Γ2 ](φ2 )) → [Γ1 ∪ Γ2 ](φ1 ∧ φ2 ) (S)
where Γ1 ∩ Γ2 = ∅
There are two reasoning rules for coalition logic. The first is Modus Ponens, the
second one is called Monotonicity.
φ↔ψ
[Γ]φ ↔ [Γ]ψ
The proof system consisting of these two rules and the five axioms is sound and
complete on coalition models with weakly playable effectivity functions [84, p.
55].
Coalition logic can be used for reasoning about extensive games. In that case
the following formula, valid on extensive game forms, should be added as an
axiom. _
[Σ]φ → [X]φ
X∈Σ
This formula can be read as saying that if something can be done, it can be done
by one of the agents.
Pauly presents several completeness proofs for different classes of models, and
for a detailed presentation we refer to his dissertation [84, p. 54]. The most
general proof is similar to the standard completeness proof of modal logic based
on a canonical model.
For extended coalition logic, a complete axiomatization is also given, and this
axiomatisation was later used by Goranko [40, 41] to develop a complete proof
system for ATL. These proof systems are more complex than the system given
here for efl, since these proof systems deal with systems with infinite runs. Our
logic efl is only a small fragment of these logics.
52 Chapter 3. Game Theory
M, s |= {G, X}φ ⇔ ∃S : ρX
G s, S ∧ ∀t ∈ S : M, t |= φ
|= {A}{B}φ ↔ {A}φ
Variants on this language, presented in the same paper [99], combine this language
with features of coalition logic.
As explained on page 18, the notion of bisimulation is used in standard modal
logic in order to decide when two models are the same. For the logic described
here, one cannot use the same definition directly. Instead Van Benthem defines
the notion of a power bisimulation.
3.4.6. Definition. Suppose two models M and M 0 with sets of worlds W, W 0
are given. A binary relation E ⊆ W × W 0 is a power bisimulation if the following
conditions hold.
• If (x, y) ∈ E then they satisfy the same atomic propositions
• For any agent X, if (x, y) ∈ E and ρX M xU then there is a set V such that
ρX
M 0 yV and ∀v ∈ V ∃u ∈ U : (u, v) ∈ E
• Vice versa: For any agent X, if (y, x) ∈ E and ρX
M yV then there is a set U
X
such that ρM 0 xU and ∀u ∈ U ∃v ∈ V : (u, v) ∈ E
This definition captures the idea that agents have the same abilities in the models
M and M 0 . Two models that are power bisimilar satisfy the same formulas [99].
φ ::= p | φ → φ | ⊥ | hhΓiiψ
ψ ::= 2φ | φ U φ
The meaning of a formula hhΓiiφ is that the agents in Γ can use a strategy such
that φ holds.
This logic is interpreted over alternating transition systems [6]. These are
defined as tuples (P, Σ, Q, π, δ). As usual P is a set of atomic propositions and Σ
a set of agents. The set Q is a set of states the system can be in, and π : Q → P
Q
adds propositions to these states. The function δ : Q × Σ → 22 assigns to each
agent in each state a set of sets of states. Each agent can choose one set of states,
and the next state of the system will be from that set.
An example would be a system where Q = {0, 1, 2, 3, 4}. Suppose that
δ(0, X) = {{1, 2}, {3, 4}} and δ(0, Y ) = {{1, 3}, {2, 4}}. Agent X can now choose
{1, 2} and Y can choose {2, 4}. They make these choices simultaneously. The
next state of the system will be 2, because that is the only common state in their
chosen sets. It is necessary to put some constraints on δ so that a next state can
always be chosen.
The interpretation of this logic uses the notion of strategy to interpret the
coalition operator hhΓii. A strategy for Γ is any function that makes a choice
σΓ (X, q) ∈ δ(q, X) for any agent X ∈ Γ in any state q ∈ Q. Based on a strategy
σΓ , one can define the set of possible walks W(σΓ ) through Q so that all choices
for agents X ∈ Γ are made as recommended by the strategy. This set of walks is
used in the following interpretation of ATL.
M, q |= ⊥ never
M, q |= p where p ∈ P iff p ∈ π(v)
M, q |= φ → ψ iff M, q |= φ implies M, q |= ψ
M, q |= hhΓiiφ iff ∃σΓ : ∀w = v... ∈ W(σΓ ) : M, w |= φ
The model checker Mocha can be used to verify ATL properties of system speci-
fications [5].
54 Chapter 3. Game Theory
3.4.8. Definition. Assume that finite sets P, Σ are given. A dynamic epistemic
logic formula φ is defined by the following rule. In these rules p ∈ P and X ∈ Σ.
φ ::= p | φ → φ | ⊥ | KX φ | [φ]φ
M, w |= p iff p ∈ π(w)
M, w |= ⊥ never
M, w |= φ → ψ iff M, w |= φ implies M, w |= ψ
M, w |= KX φ iff ∀(w, v) ∈∼X : M, v |= φ
M, w |= [φ]ψ iff M, w |= φ implies M φ , w |= φ
epistemic logic.
At [φ]p ↔ (φ → p)
PF [φ]¬ψ ↔ (φ → ¬[φ]ψ)
Dist [φ](ψ1 ∧ ψ2 ) ↔ ([φ]ψ1 ∧ [φ]ψ2 )
KA [φ]KX ψ ↔ (φ → KX [φ]ψ)
This reduction method can also be used to obtain a complete proof system for
dynamic epistemic logic with common knowledge [61], and for more complicated
actions involving knowledge and beliefs [9].
Chapter 4
Logics for Protocols
4.1 Introduction
In this chapter, the logic efl is presented, that can be used for reasoning about
multi-agent protocols. The acronym efl stands for effectivity logic, because this
logic can be used to express whether coalitions have strategies that are effective
in achieving certain goals. Thus, the logic contains statements such as [X]φ,
meaning that X can achieve φ. The statement [X]φ does not mean that X wants
φ, but rather that X would have a strategy for φ at hand if it would ever need
one.
As an example of how a logical approach can be useful for people inter-
ested in multi-agent protocols, the following informal situation description is used
throughout this chapter.
The goal of this chapter is to capture these requirements in logic, and then to
find protocols that satisfy these requirements.
In this chapter, we give several examples, and we have tried to give the smallest
interesting examples of each phenomenon. The following more basic decision
problems are used for these examples.
57
58 Chapter 4. Logics for Protocols
B C
x y z x y z
In the next section, section 4.2, the language efl is defined. Section 4.3
discusses the model checking problem. Bisimulation is discussed in section 4.4,
and section 4.5 presents a proof system.
In the second part of this chapter, we look at the different ways in which
one can represent protocols. It is shown in section 4.6 that the way in which
protocols are represented influences the model checking complexity. This is done
by specifying a more efficient way of representing protocols, and proving that the
model checking problem becomes harder when this input format is used. Within
this chapter we also present many alternative protocols for the example voting
problem. The last section, section 4.7, contains conclusions.
An example game form that represents a protocol for the voting problem is
displayed in figure 4.1. The outcomes are marked with propositions x, y, z. In this
protocol, A decides whether B or C can decide on the outcome of the protocol.
4.2.2. Definition. Assume that finite sets P, Σ are given. An efl formula φ
is defined by the following two rules. In these rules p ∈ P and Γ ⊆ Σ
φ ::= 2ψ | φ → φ | ⊥ | [Γ]ψ
ψ ::= p | ψ → ψ | ⊥
4.2. Defining Effectivity Logic 59
The second line of this definition defines a typical propositional logic formula ψ.
These propositional logic formulas are not efl formulas. They can only appear
as 2ψ or [Γ]ψ. Thus, formulas such as p ∨ ¬p and p → q are propositional logic
formulas, but are not themselves efl formulas.
Propositional logic is interpreted in the usual way. The logic efl is interpreted
over an interpreted game form F = (Σ, H, turn, P, π). The definition makes use
of pure strategies σΓ and updates with these strategies.
• if h ∈ H 0 and turn(h) ∈ Γ then hσΓ (h) ∈ H 0 , but for all other actions b we
have hb ∈/ H0
F |= ⊥ never
F |= φ → ψ iff not F |= φ or F |= ψ
F |= 2φ iff ∀h ∈ Z(H) : π(h) |= φ
F |= [Γ]φ iff ∃σΓ ∀h ∈ Z(H 0 ) : π 0 (h) |= φ
where (Σ, H 0 , turn 0 , P, π 0 ) = U p(F, σΓ )
F |= 2(x ∨ y ∨ z)
F |= 2¬(x ∧ y)
F |= 2¬(x ∧ z)
F |= 2¬(y ∧ z)
60 Chapter 4. Logics for Protocols
Secondly, one can express that any two agents can enforce any outcome.
It is not hard to verify that the example protocol FV displayed in figure 4.1
indeed satisfies these formulas. Therefore, there exists a suitable protocol for the
example voting problem.
Proof. Suppose that we walk through the game tree using a post-order tree
walk [27, p.245]. At each node h, we can compute v X (h) since either h is a leaf,
or we have already computed the value of all children ha of h, in which case we
take the maximum maxa∈A(H,h) v turn(h) (ha) of all children. This walk takes time
O(kF k).
The value of a game indicates how much payoff agents can expect if they act
optimally. If one knows the value of each node, one also knows which moves are
good. Suppose that h is a nonterminal history and turn(h) = X. Intuitively
an action a is a ‘good’ action iff v X (ha) = v X (h), and thus knowing the value
function helps agents to select the best actions.
4.3.3. Theorem. For a given formula φ ∈ efl and interpreted game form F ,
checking whether F |= φ takes time O(kF k · kφk)
Proof. Assume that a formula φ and a model F = (Σ, H, turn, P, π) are given,
and furthermore assume that F is represented explicitly by listing all elements of
pairs and sets.
Determining for any propositional logic formula ψ and terminal history s
whether π(s) |= ψ can be done in time proportional to kψk. For any formula
4.4. Bisimulation 61
Combining logic and game theory can potentially lead to problems with high
complexity, but the result given here shows that this is not always the case. This
model checking problem is easy due to two factors. First of all the preferences of
agents are expressed by means of propositional logic. In this format one cannot
express complicated, higher order preferences. Secondly, this logic essentially de-
scribes two-player constant-sum games, since one group of agents tries to achieve
something under the assumption that the other agents do not cooperate. Two
player constant-sum games with perfect information are well understood and
computing optimal strategies for such games is not computationally costly.
4.4 Bisimulation
An important question is to decide when two protocols are the same. In general,
this is a complicated question, because one can compare protocols with more or
less scrutiny. One way out of this dilemma is to use logical equivalence as a
deciding factor. Given a suitable logic one can define two protocols to be the
same when their corresponding game forms satisfy the same logical formulas.
This leaves us with the problem of deciding when two interpreted game forms
satisfy the same formulas.
For the logic efl one cannot apply the notion of bisimulation of standard
modal logic directly, because it is not clear what the ‘sets of worlds’ are that
should act as domain of the bisimulation relation. For some logics defined on
extensive games one can define a bisimulation between the sets of histories. Each
position in the game tree of the first model is matched by the bisimulation to an
62 Chapter 4. Logics for Protocols
equivalent position in the other model. For efl this idea does not work, because
efl does not use the structure of the game tree directly in its semantics. Two
models in which agents move in a completely different order can still satisfy the
same efl formulas. Thus, for efl one must use a relation similar to the power
bisimulation discussed on page 52.
4.4.1. Definition. Suppose that the two models F = (Σ, H, turn, P, π) and
F 0 = (Σ, H 0 , turn 0 , P, π 0 ) are given. A binary relation E ⊆ Z(H) × Z(H 0 ) is an
outcome bisimulation if the following conditions hold.
• If (h, h0 ) ∈ E then π(h) = π 0 (h0 )
• For any coalition strategy σΓ there exists a strategy σΓ0 such that the fol-
lowing holds: Let Z be the set of terminal histories of U p(F, σΓ ) and let
Z 0 be the set of terminal histories of U p(F 0 , σΓ0 ). Then ∀z 0 ∈ Z 0 ∃z ∈ Z :
(z, z 0 ) ∈ E
• Vice versa. For any coalition strategy σΓ0 there exists a strategy σΓ such
that the following holds: Let Z be the set of terminal histories of U p(F, σΓ )
and let Z 0 be the set of terminal histories of U p(F 0 , σΓ0 ). Then ∀z ∈ Z ∃z 0 ∈
Z 0 : (z, z 0 ) ∈ E
If two game forms are outcome bisimilar, then they satisfy the same formulas.
This is proven in two steps. Below we define which formulas are called basic and
simple. In lemma 4.4.3 we show that two bisimilar models satisfy the same basic
and simple formulas. Lemma 4.4.5 can then be used to show that if two models
satisfy the same basic and simple formulas, they satisfy the same formulas.
4.4.3. Lemma. Suppose that the two models F = (Σ, H, turn, P, π 0 ) and F 0 =
(Σ, H 0 , turn 0 , P, π 0 ) are given and that E is a bisimulation between F and F 0 .
Then these models satisfy the same basic and simple formulas.
Proof. Suppose that F |= 2φ. The empty coalition has only one strategy σ∅
and this strategy has the property that U p(F, σ∅ ) = F . The same holds for F 0 .
Take Z as the set of terminal histories of F and Z 0 of F 0 . Take any state z 0 ∈ z.
The second clause of the bisimulation tells us there a bisimilar state z ∈ Z.
Since F |= 2φ and π(z) = π 0 (z 0 ) it follows that π 0 (z 0 ) |= φ. Since z 0 was chosen
arbitrarily, it follows that F 0 |= 2φ.
4.4. Bisimulation 63
Suppose that F |= [Γ]φ. This means that there is a strategy σΓ such that
U p(F, σΓ ) |= 2φ. According to bisimulation one can find a matching strategy
σΓ0 . Take Z, Z 0 to be the terminal histories of U p(F, σΓ ), U p(F 0 , σΓ0 ) respectively.
Take any state z 0 ∈ Z 0 . One can find a state z ∈ Z such that (z, z 0 ) ∈ E. Since
π(z) |= φ and π 0 (z 0 ) = π(z) it follows that π 0 (z 0 ) |= φ. Since z 0 was chosen
arbitrarily, we conclude that F 0 |= [Γ]φ.
Since the definition of outcome bisimulation is symmetric, one can repeat the
argument to show that F 0 |= 2φ implies that F |= 2φ, and that F 0 |= [Γ]φ
implies F |= [Γ]φ.
In the next lemma, we use specific formulas instead of simple formulas. These
specific formulas are simple formulas such that no stronger simple formulas exists.
4.4.4. Definition. Take any set S of formulas and suppose that φ1 = [Γ]ψ ∈ S
and φ2 = [Γ]χ ∈ S. The formula φ2 is more specific than φ1 if 2(χ → ψ) ∈ S and
2(ψ → χ) ∈ / S. The formula φ1 is specific if there is no more specific formula in
S.
To give an example of a specific formula, take S = {[A]a, [A]b, 2(b → a)}. In this
case [A]b is the only specific formula in S, because this formula is more specific
than [A]a.
The next lemma tells us that it is enough to check only formulas that are sim-
ple and specific to ensure that two maximally consistent sets are the same. Since
the set of all formulas satisfied by a model is always a maximally consistent set,
one can also use this lemma to show that two models satisfy the same formulas.
4.4.5. Lemma. Suppose that S and T are maximally consistent sets. Let S 0
contain all basic and all specific formulas of S and T 0 all basic and all specific
formulas of T . If S 0 = T 0 then S = T .
Proof. Suppose that S and T are maximally consistent sets. Let S 0 contain
all basic and all specific formulas of S and T 0 all basic and all specific formulas
of T . Suppose also that S 0 = T 0 . Let ξ = [Γ]ψ ∈ S. We have to show that
ξ ∈ T . If ξ is specific, then ξ ∈ S 0 , thus ξ ∈ T 0 and ξ ∈ T . If not, then
there is some ‘more specific’ formula [Γ]χ ∈ S so that 2(χ → ψ) ∈ S . This
formula itself need not be specific, since there might be an even more specific
formula that rules out [Γ]χ. However, since P is finite, there is only a finite
number of non-equivalent propositional logic formulas. This means there must
be a specific formula [Γ]χ ∈ S 0 and 2(χ → ψ) ∈ S. Since S 0 = T 0 we know that
[Γ]χ ∈ T 0 and thus [Γ]χ ∈ T . Since 2(χ → ψ) ∈ S is basic, we can conclude that
2(χ → ψ) ∈ S 0 = T 0 ⊆ T . Using the the validity ([Γ]χ ∧ 2(χ → ψ)) → [Γ]ψ and
the fact that T is maximally consistent, we conclude that [Γ]ψ ∈ T .
It is now proven that S and T contain the same simple formulas. Consider now
a formula of the form ¬[Γ]ψ. If ¬[Γ]ψ ∈ S, the validity of the axiom determined,
64 Chapter 4. Logics for Protocols
proven in the next section, can be used to show that [Σ \ Γ]¬ψ ∈ / S. Since this is
a simple formula, we conclude that [Σ \ Γ]¬ψ ∈ / T . Using determined again we
obtain ¬[Γ]ψ ∈ T .
A useful property of maximally consistent sets is that if φ ∧ ψ ∈ S then φ ∈ S
and ψ ∈ S. Moreover if φ ∨ ψ ∈ S then φ ∈ S or ψ ∈ S (or both). For every
formula φ ∈ S in conjunctive normal form we can conclude that φ ∈ T . Since
every propositional formula is equivalent to a formula in conjunctive normal form,
we may conclude that for any formula φ it is the case that φ ∈ S ⇔ φ ∈ T .
Therefore, S = T .
The notion of outcome bisimulation can thus be used to test whether two
protocols have the same properties.
4.5 Completeness
Using the notations from the previous section, one can determine whether two
protocols are equivalent. In this section the focus is on the more difficult problem
of determining whether there exists a protocol F that satisfies a given property
φ. In order to do so, a proof system SEF L is defined, so that one can prove that
certain formulas hold for any model. If SEF L `¬φ, then there is no model F such
that F |= φ. The proof system we present is complete, and thus the opposite also
4.5. Completeness 65
holds: If SEF L 6 `¬φ, then there exists a model F such that F |= φ. The proof
given is constructive, in the sense that it provides a method for constructing such
a model.
First the validity of the formulas that are used as axioms is proven. Then the
proof system SEF L is defined, and the completeness proof is given.
The next table lists four axioms that can be written without the coalition
operator [Γ]φ. These axioms are thus formulas of ‘normal’ modal logic [12].
For the Greek letter τ one may substitute any instance of any propositional
logic tautology that one can obtain using uniform substitution. For instance
[Σ]p∨¬[Σ]p is an instance of p∨¬p. For all other Greek letters one may substitute
any propositional logic formula.
prop = τ tautology
prop2 = 2τ box-tautology
S = 2φ → 3φ seriality
K = 2(φ → ψ) → (2φ → 2ψ) distribution
All instances of these axioms are valid. For the axiom tautology this follows
from the fact that the connectives ⊥, → are interpreted in the same way as in
propositional logic. For the axiom box-tautology, one can remark that the
definition of 2φ uses the semantics of propositional logic. For the axiom seri-
ality, it follows from the fact that each game form must have a non-empty set
of outcome states. The distribution axiom is the same as the standard modal
logic distribution axiom. Its validity can be shown in the same way. This works
because the operator 2 is also defined as a universal operator: 2φ holds if φ is
true in all reachable states. For efl, the reachable states are all the outcome
states.
These axioms are complete for the fragment of efl in which the construction
[Γ]φ is not used. To give a proof sketch: consider the completeness proof of
standard modal logic [12]. One can adapt the completeness proof so that no
nesting of boxes occurs. In that case, the proof exactly matches the language of
efl without [Γ]φ. The remaining axioms for efl are listed below.
C =([Γ]φ ∧ [Ξ \ Γ](φ → ψ)) → [Γ ∪ Ξ]ψ combination
M =[Γ]φ ↔ ¬[Σ \ Γ]¬φ determined
N =[∅]φ ↔ 2φ nobody
4.5.1. Lemma. All instances of combination, determined and nobody are
valid
follows that there are two strategies σΓ and σΞ such that U p(F, σΓ ) |= 2φ
and U p(F, σΞ ) |= 2(φ → ψ). The two strategies σΓ and σΞ are two functions
with separate domains. One can form a combined strategy σΓ∪Ξ = σΓ ∪ σΞ .
If an outcome state is pruned by either σΓ or σΞ , then it is also pruned by
the combined strategy. Therefore, U p(F, σΓ∪Ξ ) |= 2φ ∧ 2(φ → ψ) and thus
F |= [Γ ∪ Ξ]ψ.
• Take an instance [Γ]φ ↔ ¬[Σ \ Γ]¬φ of determined. One can define a two
player constant-sum extensive game based on the game tree of F between Γ
and Ξ = Σ\Γ so that Γ wins in an outcome s if s |= φ and Ξ wins if s |= ¬φ.
In such an extensive game of perfect information, the two coalitions must
have a winning strategy. Therefore, either F |= [Γ]φ or F |= [Ξ]¬φ.
One property that one can derive is specificity and can be derived using
combination and nobody. Another property is monotonicity, which follows
from box-tautology, combination and nobody.
4.5.2. Definition. The proof system SEF L consists of the seven axioms tau-
tology, box-tautology, seriality, distribution, combination, deter-
mined, nobody given above and the reasoning rule Modus Ponens.
As an example of how this proof system can be used, assume that we have
three agents (Σ = {A, B, C}) and three propositions P = {a, b, c}. We are looking
for a protocol that has the following properties.
1 2(a ∨ b ∨ c)
2 ¬[AB]2c
3 ¬[AC]2b
4.5. Completeness 67
One can use the proof system SEF L to show that from these three properties, it
follows that ¬[A]2¬a. The following derivation proves this property.
4 [C]2¬c 2, determined
5 [B]2¬b 3, determined
6 [BC]2(¬b ∧ ¬c) 4, 5, combination
7 2((¬b ∧ ¬c) → a) 1, box-tautology, K
8 [BC]2a 6, 7, specificity
9 ¬[A]2¬a 8, determined
Proof. In lemma 4.5.1 it is shown that all axioms are sound. On page 12
it is remarked that the rule modus ponens preserves validity. From these facts
it follows that only valid formulas can be derived, which means that the proof
system is sound.
The proof system defined here is also complete, and this is proven below in a
constructive sense. This proof differs from the standard completeness proof for
modal logic, that is sketched on page 17. The proof is a bit more complicated
because the semantics of this logic do not refer to single steps in the game trees,
but on the possible outcomes that agents can effect.
Proof. We have to show that for each consistent formula φ ∈ efl there is a
model F such that F |= φ. Let a consistent formula φ ∈ efl be given. Let S be
a maximally consistent set so that φ ∈ S and let S 0 contain all basic and specific
formulas of S. Below a model F is constructed so that ∀ψ ∈ S 0 : F |= ψ. Lemma
4.4.5 can then be used to conclude that F |= φ.
The model F we are about to construct is defined recursively using a function
f (C, A, r). The outcome of this function depends on a set of basic and simple
formulas C, on a set of active agents A ⊆ Σ and on a representation function
r : Σ → 2Σ . The set r(X) contains the agents that are represented by agent
X. The model F is defined as F = f (S 0 , A0 , r0 ). Initially, all agents are active
agents: A0 = Σ, and each agent initially only represents itself: r0 (X) = {X}.
The function r can also be applied to coalitions of agents. This is defined by
r(Γ) = ∪X∈Γ r(X). The pair A, r can be used to calculate a new set of simple and
basic formulas S(C, A, r) from a given subset C.
The game form f (C, A, r) is defined in the following way. If A contains exactly
one active agent X, then we define a model f (C, A, r) = (Σ, H, turn, P, π) where
H = {, ψ | [X]ψ ∈ C, [X]ψ is specific}. Define turn() = X. If 2ψj ∈ C,
then because of box-tautology 2(ψ → (ψ ∧ ψj )) ∈ C. Using the specificity
property, we conclude [X](ψ ∧ ψj ) ∈ C. Repeating
V this reasoning for any simple
formula ψj ∈ C, we obtain a formula [X](ψV ∧ j ψj ) ∈ C. Let π(ψ) be a set of
atomic propositions such that π(ψ) |= (ψ ∧ j ψj ). One can now show that any
formula χ ∈ C is satisfied by this model.
If A has two or more members, define f (C, A, r) = (Σ, H, turn, P, π) as follows.
Take any agent X ∈ A. Define turn() = X, so that this becomes the acting
agent of the current situation. The set of options A(H, ) consists of two parts:
A(H, ) = E ∪ J. Agent X can thus choose from two different types of actions:
formulas from set E or ‘joining’ an agent from set J.
We must show that f (C, A, r) satisfies all formulas in C. This is done using
induction. The induction hypothesis is that submodels of the current model have
this property. The base case is formed by models with one active agent, and this
has been done with above.
First, consider basic formulas, of the form 2φ ∈ C. These formulas are present
in each set C 0 that is used to construct a subgame. Using the induction hypothesis
we know that all outcomes of all choices satisfy φ, and thus f (C, A, r) |= 2φ.
Consider [Γ]ψ ∈ C with X ∈ / Γ. This formula is also present in any set C 0 and
by induction hypothesis we know that there is thus a strategy in each subgame
for Γ to ensure ψ. We can combine these subgame strategies into a strategy σΓ
for the whole game that guarantees ψ, and thus f (C, A, r) |= [Γ]ψ.
Secondly, consider [Γ]ψ ∈ C with X ∈ Γ. If Γ = {X} then there is some spe-
cific ψe ∈ E so that 2(ψe → ψ) ∈ C. This choice leads to a submodel f (C 0 , A, r).
From ψe ∈ C 0 and the induction hypothesis it follows that there is a strategy σX
0
for this submodel that guarantees ψ. Agent X can now use a strategy σX so that
4.5. Completeness 69
A
y n
B B
y n y n
a, b a b
Figure 4.2: A simple game form F1
In figure 4.2 an example interpreted game form is shown. In this game form agent
A first decides whether a should hold or not. Then agent B can decide whether
proposition b should hold or not. A possible story could be that a indicates that
A dresses in black, and b indicates that B dresses in black. The next table lists
properties that are true for the example F1 .
F1 |= [A]a ∧ [A]¬a
F1 |= [B]b ∧ [B]¬b
F1 |= [B](a ↔ b) ∧ [B](a ∇ b)
One can conclude that agent B, because it goes second, can control more. This
corollary can be illustrated for the example protocol of figure 4.2. According to
the proof there should be an equivalent protocol in which agent B moves first.
This is indeed the case, and the protocol is illustrated in figure 4.3. One can see
that B in this case can choose from four options.
In the construction of the proof, each agent has a choice whether it wants to
use one of its abilities (set E) or whether it wants to join a specific agent (set J). In
order to illustrate these two possibilities, consider the property φ3 = [A]p ∧ [B]p ∧
[AB]¬p. There is only one atomic proposition in this example, so P = {p}. There
are only four distinct formulas that one can express: p, ¬p, ⊥, p → p. Suppose
70 Chapter 4. Logics for Protocols
B A
b A ¬b a↔bAa ∇ b p B
A A B
p p ¬p
a ¬a a ¬a a ¬a a ¬a
ab b a ab a b p
Examples
In this subsubsection we present a few example linear representations
4.6. Linear Representations 71
To start with a simple example, consider the trivial protocol F where agent
A can only chose one action, after which an outcome in which p holds is reached.
Such a protocol F could be described by the linear representation R = A → − {p}.
The set {p} at the end of the representation is the set of propositions that is true
at the end of the protocol. The agent A in front of the arrow indicates that agent
A is the agent that can chose. In this protocol agent A can only chose one action.
It has no real choice, which makes the protocol trivial.
In order to describe more complicated protocols, two additional constructions
can be used. The first one is parallel composition. Suppose that we have two linear
representations R1 = A → − {p} and R2 = A → − {q}. In each of these protocols
agent A can only chose one action, but the two protocols have different outcomes.
We define R3 to be the parallel composition of the two linear representations:
R3 = R1 ||R2 , or:
R3 = (A → − {p})||(A →− {q})
In the protocol described by R3 , agent A can choose two actions, and end up in
either the outcome of pR1 q or the outcome of pR2 q. Thus parallel composition
of protocols gives the starting agents more choice.
The other construction is the use of variables. Take a protocol in which agent
A can choose which of the tree propositions {p, q, r} is true. The agent is allowed
to chose one of these propositions. This protocol can be described by the linear
v∈{p,q,r}
representation R = A −−−−−→ {v}. The symbol v is used here as a variable that
can takes the values p, q or r. The protocol pF q thus has three possible outcomes,
in which either p, q or r holds.
The follow grammar defines how one can form expressions that denote boolean
values, sets, lists and objects. Assume that a set of propositions P = {p0 , p1 , . . .}
and a set of agents Σ = {X0 , X1 , . . .} are given.
All these operators are interpreted in the usual way, except perhaps for {x|φ}.
The x in this example is a concrete object, not a variable. Thus, if pφq holds
then p{x|φ}q = {pxq}, otherwise p{x|φ}q = ∅.
The denotation pEq of an Objct expression E can be computed in polynomial
time, since efficient algorithms for all operations exist. In fact the operations used
are polynomial shrinking (see page 87), which means that the denotation pEq of
an expression E is also not bigger than E: kpEqk ≤ kEk
72 Chapter 4. Logics for Protocols
The next table gives some examples of Objct expressions and their denotations
p∈{P } B s∈{{p},∅}
R3AB = (A −−−→ {p})||(A −
→ B −−−−−→ s)
Note that one can represent the same protocol in different ways. At the start
of this section as example is given where an agent A can choose whether p, q
or r holds. This protocol F was described using variables as F = pRq where
v∈{p,q,r}
R = A −−−−−→ {v}. One can also use parallel composition to describe the same
protocol. Thus F = pR0 q where
R0 = (A →
− {p})||(A →
− {q})||(A →
− {r})
Note that R is a shorter description than R0 . The more concise description R
is often easier to read, and thus preferred over R0 .
In the next two definitions we formally define what we can allow for a repre-
sentation, and how these representations are translated into game forms. Then
we give more example game forms for the voting problem, and give a complexity
result.
4.6. Linear Representations 73
4.6.1. Definition. Assume a set of variables V is defined and that the finite
sets P, Σ are given. The set of all linear representations is defined recursively as
follows.
• If R is a Objct-expression, such that R denotes a set of atomic propositions
pRq ⊆ P , then R is a linear representation
v∈S
• The construct X −−→ R is a linear representation if the following conditions
are met. We demand that X ∈ Σ, that v ∈ V is a variable, that S is a linear
representation such that pSq is a set of objects, and that for all si ∈ pSq
we have that R[v \ si ] is a linear representation.
v∈S v∈S
• If R0 = X −−−→ 0
R00 and R1 = X −−−→ 1
R10 are linear representations and
pS0 q ∩ pS1 q = ∅ then R0 ||R1 is a linear representation.
Using this definition we can now fill in the details in the linear representation of
the independent decision problem given above.
s1 ∈{{a},∅} s2 ∈{{b},∅}
R1 = A −−−−−−→ B −−−−−−→ s1 ∪ s2
Thus, agent A chooses whether atomic proposition a appears in s1 , agent B
chooses whether b appears in s2 , and the final outcome of the protocol is the
union of their respective decisions. If one had 100 agents, then this method of
specification would be much more efficient than a description in tuples and sets.
The next definition defines a function f F that translates linear representations
into interpreted game forms. This function is defined in the following way.
4.6.2. Definition. Assume the finite sets P, Σ are given, Define f F (R) = f1F (, R),
where f1F is the function defined below. Let h be a sequence of actions.
• If pRq ⊆ P then f1F (h, R) = (Σ, {h}, ∅, P, π) where π(h) = pRq.
s∈S
• Assume R = X −−→ R0 is a linear representation. For any si ∈ pSq compute
= f1F (hsi , R0 [s \ si ]).S The result f1F (h, R)Sis defined
(Σ, Hi , turn i , P, πi ) S
F
as f1 (h, R) = (Σ, i Hi ∪ {h}, turn, P, i πi ) where turn = ( i turn i ) ∪
{(h, X)}.
• f1F (h, R0 ||R1 ) = (Σ, H0 ∪H1 , turn 0 ∪turn 1 , P, π0 ∪π1 ) where (Σ, Hi , turn i , P, πi ) =
f1F (h, Ri )
The voting protocol FV has the following linear representation.
X∈{B,C} p∈{x,y,z}
R1A = A −−−−−→ X −−−−−→ {p}
It says exactly what the protocol is : A chooses between B and C, which in turn
chooses his favorite alternative.
74 Chapter 4. Logics for Protocols
4.6.3. Fact. For any linear representation R, f F (R) is an interpreted game form.
Proof. In the proof of theorem 4.3.3 and lemma 4.3.2 it is explained how model
checking efl depends on the ability to do a post-order tree walk. If we can do
such a post-order tree walk in polynomial space, then we can model check efl
formulas in polynomial space. An algorithm for such a walk typically uses a
stack. On this stack a description of the current node is stored, after which the
description of a successor is computed, which is also stored on the stack, etcetera,
until a final node is reached. We therefore show the following facts.
• For a linear description R of a terminal node and a propositional logic
formula φ, one can determine whether pRq |= φ in polynomial time. This
follows immediately from the assumption that one can compute the set
of atomic propositions pRq in polynomial time. A naive polynomial time
algorithm is to compute pRq and then determine whether pRq |= φ. Hence
this takes at most b(kRk + kφk) for some polynomial bound R
• Each linear description of a successor of R is smaller that R itself. This is
easy to see. In the case of R = R1 ||R2 , both R1 and R2 are smaller than
v∈pSq
R. In the case of R = X −−−→ R0 (v), it is also clear that kR0 (v)k ≤ kRk.
Thus, each element on the stack needs as most memory kRk
• The maximal number of descriptions on the stack is also bounded by kRk,
because the maximal depth of the model denoted by R is at most the number
of arrows that occur in R.
From the last two facts one can compute that one needs at most kRk · kRk
memory for the stack. Therefore, the total amount of memory that one needs
to determine whether φ holds on pRq for a linear representation R is less than
kRk2 + b(kRk + kφk), and thus is polynomial.
It remains to be proven that the problem is PSPACE-hard. This can be done
by reducing the QBF problem described on page 31 to the efl decision problem.
4.6. Linear Representations 75
Assume that a QBF formula ∀x1 ∃x2 ∀x3 . . . ∀xn φ is given. We have to con-
struct an equivalent efl decision problem, consisting of a representation R and a
formula φ0 . Let Σ = {X, Y } and P = {xi |0 ≤ i ≤ n}. The atomic proposition x0
is a dummy atomic proposition, since it does not appear in φ. The representation
of the interpreted game form is the following:
v1 ∈{x0 ,x1 } v2 ∈{x0 ,x2 } vn−1 ∈{x0 ,xn−1 } vn ∈{x0 ,xn }
R = X −−−−−−→ Y −−−−−−→ . . . Y −−−−−−−−−→ X −−−−−−→ {v1 , v2 , . . . , vn }
Take φ0 = [Y ]φ. The agent Y thus makes all existential choices (it tries to
pick values for the xi that make φ true), and agent X is used for the universal
choices. If ∀x1 ∃x2 ∀x3 . . . ∃xn−1 ∀xn φ, then f F (R) |= φ0 and vice versa.
B B B
... ...
C C C
x
x x
y z
The new representation format can be used to define more candidate protocols
for the example problem defined in the beginning of this chapter. These new
protocols all satisfy the requirements of the example, while being very different
from protocol FV . Below we define two more protocols, called FV 2 = f F (R2ABC )
and FV 3 = f F (R3x ). Part of the game tree of protocol FV 2 is depicted in figure
4.5.
a∈{x,y,z} b∈P \{a} c∈{a,b} a
R2ABC = A −−−−−→ (B −−−−−→ C −−−−→ {c})||(B →
− {a})
In FV 2 , A and B choose from the three possible outcomes. If they choose the
same outcome, then that is the final outcome. Otherwise C can choose from the
two outcomes they selected.
In our third example FV 3 , the agents A, B, and C vote sequentially for one
of the three outcomes; the outcome that gets the most votes is elected. If A, B
and C disagree then a pre-determined outcome x is elected.
It is not hard to verify that these three protocols satisfy exactly the same
efl formulas. One can thus conclude that these three protocols are equally fair,
and that there is no reason to prefer one of those protocols above the others. This
conclusion seems counter-intuitive, because the protocol R3x seems biased towards
outcome x. If the agents cannot come to an agreement, then outcome x results.
4.7. Conclusion 77
Perhaps efl is the right tool and the bias mentioned for R3x is an irrelevant
detail. It is also possible that the logic efl is not sensitive enough. Both of these
viewpoints are valid, depending on the application one has in mind.
Making more use of the new notation, one can make even more complicated
protocols. Similar to R3x , one can define protocols R3y and R3z , in which y and
respectively z are the default outcomes. One can offer one of the agents the choice
of selecting the default outcome.
d∈{x,y,z}
R4A = A −−−−−→ R3d
The new protocol f F (R4A ) again satisfies the same efl formulas. If one how-
ever thinks that R3x is biased towards x, then one must conclude that R4A is skewed
towards A. The word skew is used here to express that a certain agent is treated
differently in a significant way from other agents, whereas bias means that an
outcome is treated in a different way than the other outcomes. To give another
example of how one can make more subtle protocols, consider the case where
agent A chooses whether B or C selects the default outcome.
S∈{B,C}
R5A = A −−−−−→ R4S
The result is that there are indeed many different protocols for the example
problem. Many of these can be elegantly described using a linear representation,
even when it would have been very hard to draw a picture of the game tree. For
efl however all these protocols are equivalent.
4.7 Conclusion
The logic efl is a high level logic for reasoning about multi-agent protocols. In
this chapter, the problem of finding a good voting protocol has been used as a
motivating example for the construction of such logic. Different protocols have
been presented and modeled as game forms. Using efl we have shown that the
candidate protocols indeed satisfy the requirements of the problem. Using an
effectivity logic such as efl one can thus reason about the powers of agents and
coalitions in protocols.
In order to efficiently discuss multiple protocols, one needs a good way of
representing different protocols. The naive way, as a tuple of sets and functions,
is rather cumbersome. Another option is to specify protocols by means of a
picture of a game tree. However this is also only practical for small protocols. In
this chapter, a new input format is defined, called the linear representation. The
idea behind this format is that one can specify a protocol by describing a typical
execution of the protocol. For the example voting problem, one can elegantly
describe many protocol variants using the linear representation.
78 Chapter 4. Logics for Protocols
5.1 Introduction
Like the previous chapter, this chapter is concerned with reasoning about game
forms, which are seen as models for multi-agent protocols. In this chapter we
extend the logic of the previous chapter. It is assumed that each agent that
participates in a protocol has some private preferences about the outcome of the
protocol. The word ‘preferences’ is used here in a very loose sense, as a synonym
for ‘goal’ or ‘desire’. It is also assumed that these preferences are not determined
by the protocol. Agents can want whatever they want to want. In voting protocols
it is clear that the agent can have its own, private, preferences over outcomes. In
an auction this is less clear: auctions are often analysed under the assumption
that each agent wants to win at the lowest cost. We assume a more general
setting, where agents can also play to lose, or to maximize the amount they pay.
One of the goals of this chapter is to investigate verification of more com-
plicated properties than only the ability to enforce a certain outcome. Three
complications that are being discussed are the following.
• Groups of agents can have coalition preferences. One can express in the
logical languages that A and B together want φ. This means that they try
to reach a certain goal together and are able to cooperate.
• Agents may be interested in nested abilities: an agent can have the ability to
enable another agent to achieve something, or to make sure another agents
is not able to do something. The wish to give other people the chance
to make a decision, is often associated with politeness, we use the phrase
‘reasoning about politeness’ as an informal name for these nested ability
goals.
• We are not only interested in knowing what agents can achieve, but also in
what way they achieve it. Thus, we would like to know whether an agent
79
80 Chapter 5. Politeness and Side Effects
has to spend all his money to win an auction, or whether an agent should
vote for the candidate it like best. Thus, the side effects of acting in a
certain way are also important.
In this chapter, different logical languages are defined, so that we can determine
how considering nesting and side effects affects the analysis of protocols. In total
four languages are defined. The next table lists the languages and their features.
logic nesting side effects
efl
efls
efln
eflns
Chapter Structure
The structure of this chapter is the following. First the logic efls is defined
in section 5.2, and examples for this logic are given in section 5.3. The next
section, section 5.4, contains a theorem stating that for logics of a certain form,
the model checking problem is tractable. It is shown that this theorem can be
applied to efls. Then the question is posed whether there are more expressive
or detailed logics based on efl and efls. In section 5.5, first the language efln
for reasoning about nested abilities is introduced, and we determine the model
checking complexity of this logic. Then a more expressive language eflns is given
for reasoning about both politeness and side effects. The last section, section 5.6
is the conclusion.
φ ::= p | φ → φ | ⊥
ψ ::= [Γ : φ]ψ | 2φ | ψ → ψ | ⊥
This language can be seen as an extension of efl, in the following way. An efl
formula [Γ]φ is equivalent to the efls formula [Γ : φ]2φ.
A formula [Γ : φ]ψ should be read as saying ‘Assume that Γ uses a strategy
that is supporting φ. Then ψ follows’. It is assumed that all agents are aware of
strategies that are used. The strategy that an agent uses can be said to be ‘visible’
to other agents. If one wants to express this idea in the most extreme form, one
could say that we assume that strategies are visible in the same way as people
5.2. Defining EFLS 81
can see what clothes other people are wearing on a certain day. In many real life
settings, finding out what strategies are used in a strategic setting will probably
take a bit more effort, but is not impossible. This visibility assumption is inspired
by the assumption of complete information in game theory, and is compatible with
the idea of a Nash equilibrium. Indeed if one, as a game theorist or as a strategic
consultant, intends to publish books and papers about good strategies (whether
these are chess strategies, marketing strategies, strategies for penalty taking, or
strategies for generating secure random numbers) then such strategies must work
even when public. Even if one does not wish to publish strategies, people can
often observe what action you take and deduce your strategy from this. Thus it is
known what playing styles professional chess players prefer and how professional
football players take penalties. Many professional keepers, including Hans van
Breukelen, for instance relied on Jan Reker’s booklet for this information [117].
The visibility assumption is also inspired by insights from security and cryp-
tography. One can see the definition of specification of a cryptographic algorithm
as a protocol, and the implementation details as a strategy within such protocol.
For instance the protocol for RSA key generation requires one to choose two prime
numbers p and q. An agent has many ways to do this, and common strategies in-
clude using the current time and some keyboard input for generating these prime
numbers (See Schneier [89] for a dicussion of RSA and implementation details).
The implementation details are often public information, since for many security
programs one can obtain the source code.
The effectiveness of an implementation should not lie in the fact that its inner
details are secret (Thus, one should avoid trying to obtaining security through
obscurity [89]). In order to prove that a strategy or algorithm is ‘good’ or ‘safe’,
one should assume that it is known to all opponents that the strategy is used,
and then consider how effective the strategy is. For instance if Microsoft decides
to use a certain encryption mechanism in its web server software, then anybody
with harmful intentions can buy and study the software, and find out what mea-
sures have been taken against attacks. Typically in security one wants to prove
that opponents remain ignorant of private data. If they are ignorant even when
they know the strategy used, they are certainly ignorant when they do not know
the strategy used. This assumption can also be made in the case of imperfect
information games, and indeed a similar argument is given on page 132.
The idea that strategies are ‘visible’ makes the act of deciding to use a strategy
similar to publicly announcing that you use the strategy. In complex statements,
this idea of an announcement can be used informally when reading formulas. The
following examples illustrate how formulas of this logic can be read.
[A : q]2p
This example formula expresses that if A is trying to achieve q, then as a side
effect p will hold for every possible outcome.
[A : q][B : r]2r
82 Chapter 5. Politeness and Side Effects
This example formula can be read as expressing that, assuming after A has de-
cided that it wants q, then B can select a strategy such that r becomes true. The
order of operators in the formula indicates that B knows the strategy of A, and
can use this in its selection of a strategy for r.
The next formula seems to contain contradictory assumptions.
[A : q][A : ¬q]2(¬q)
This formulas expresses that if A wants q, and then it wants ¬q, then ¬q is
guaranteed. In order for this formula to hold on a model F , it must be the
case that A cannot make q true, otherwise it would choose to do so in the first
assumption.
For the interpretation of this logic the following definitions are used.
5.2.2. Definition. Let F = (Σ, H, turn, P, π) be an interpreted game form and
h ∈ H. The reduced model r(H, h) is defined as r(H, h) = (Σ, H 0 , turn 0 , P, π 0 )
where H 0 = {h0 |h · h0 ∈ H} and turn 0 , π 0 are restrictions of the corresponding
elements of F to H 0 .
The next definition redefines the update function U p so that it works on nonde-
terministic strategies. The intuition is that in the updated model U p(F, σΓ ), the
agents in Γ only take actions that are recommended by σΓ .
5.2.3. Definition. Let F = (Σ, H, turn, P, π) be an interpreted game form and
σΓ a strategy for Γ. Define U p(F, σΓ ) = (Σ, H 0 , turn 0 , P, π 0 ) where H 0 is the
greatest subset of H such that ha ∈ H 0 implies h ∈ H 0 and turn(h) ∈ Γ ∧ ha ∈ H 0
implies a ∈ σΓ (h). The functions turn 0 , π 0 are identical to turn, π but restricted
to H 0 .
The next definition defines a strategy σΓe (φ) that is intended to be the least
restrictive, or most general, strategy that Γ can use to achieve φ.
5.2.4. Definition. Let F = (Σ, H, turn, P, π) be an interpreted game form,
Γ ⊆ Σ and φ ∈ Lp . A history j is a φ-effective position (for Γ) iff there is a
strategy σΓ such that for each terminal history h in U p(r(H, j), σΓ ) it is the case
that π(h) |= φ. The most general φ-effective strategy σΓe (φ) is now defined by
e {a|ha is a φ-effective position for Γ} if this set is non-empty
σΓ (φ)(h) =
A(H, h) otherwise
The definition above spells out what we consider a rational strategy σΓe (φ) for a
coalition Γ that wants to achieve φ. The strategy is defined such that it selects
actions a that lead to winning positions. If that is not possible, it selects all
actions. The idea is that coalition Γ tries to guarantee φ in all positions where
it can guarantee φ. This is similar to the notion of a subgame-perfect strategy.
In the definition below we use this strategy for interpreting the logic. Let F =
(Σ, H, turn, P, π) be an interpreted game form. For any formula φ ∈ efls the
relation F |= φ is defined as follows.
5.3. Examples 83
A
b, e a
a, e b
F |= ⊥ never
F |= φ → ψ iff not F |= φ or F |= ψ
F |= 2φ iff ∀h ∈ Z(H) : π(h) |= φ where (Σ, H, turn, P, π) = F
F |= [Γ : φ]ψ iff U p(F, σΓe (φ)) |= ψ
5.3 Examples
5.3.1 Alice and Bob eat Cake
Alice and Bob have a cake, and they have agreed to divide it by means of a “cut-
and-choose” protocol [17]. Alice has cut the cake and unfortunately one of the
pieces is bigger than the other. Bob can now choose from three options: he can
select the big piece, select the small piece, or he can say to Alice ‘No, you choose’.
If he lets Alice choose, she can either choose the big piece or the small piece. Both
agents have common knowledge of this protocol. The interpreted game form
protocol corresponding to this situation is displayed in figure 5.1. Proposition a
means that Alice gets the biggest piece, b that Bob gets the biggest piece, and
e means that something has happened that is embarrassing to Alice and Bob,
namely that either Alice or Bob has chosen the biggest piece. In many cultures
this is considered impolite. Using efls one can express relevant properties of
this protocol. First we will provide several efls formulas (A stands for Alice, B
stands for Bob).
84 Chapter 5. Politeness and Side Effects
• [A : ¬e][B : ¬e][B : b]2b This formula expresses that if A does not want
embarrassment, B does not want embarrassment, and B prefers the biggest
piece then B gets the biggest piece. The behaviour of B is influenced by the
fact that he knows that A prefers to avoid embarrassment. In this scenario
A should try to hide the fact that she has good manners, because it is not
in her advantage if B knows this.
This example illustrates that, by using efls, one can express consequences
of ordering goals in a certain way. There are several interesting side effects men-
tioned in the above formulas.
5.3. Examples 85
A
a
B
p A A
p p ¬p
p
In figure 4.4, on page 70, an interpreted game form F3AB is given in which two
agents jointly decide whether p should hold or not. If either agent wants to have
p it should hold, otherwise p is rejected. In figure 5.4 another protocol is given
that satisfies the same efl formulas. In this protocol, the roles of B and A are
reversed. It seems reasonable to assume that agents care who has to give its
opinion first, and therefore one would like to have a logic that can distinguish
these protocols.
The following statements show that efls is such a logic.
The reason the formula does not hold in the second model is that B, because
it moves first in the protocol F3BA , has an informational disadvantage. When it
has to decide it does not know what A will do, and therefore it is not clear that
letting A choose helps towards achieving its goal. The logic efls is thus more
expressive than efl.
86 Chapter 5. Politeness and Side Effects
5.4.1. Definition. Suppose that M and N are given, and assume that n1 ∈ N1
and n2 ∈ N2 . The update language Lf g consists of formulas ψ generated by the
following rules.
ψ ::= [n1 ]ψ | n2 | ψ → ψ | ⊥
This language is called an update language, because one can interpret this logic
using updates. The function f is used to compute a new model from the current
model. The next definitions captures the idea of an update semantics. In the
next definitions, M ∈ M is a model, n1 ∈ N1 , n2 ∈ N2 and ψ, ξ ∈ Lf g .
M |= ⊥ never
M |= ψ → ξ iff not M |= ψ or M |= ξ
M |= n2 iff g(M, n2 )
M |= [n1 ]ψ iff f (M, n1 ) |= ψ
These axioms can be compared to the reduction axioms stated for dynamic epis-
temic logic stated on page 55. The axioms are not identical, and these two axioms
5.4. Model Checking EFLS 87
are not sufficient to eleminate all update operators, but they do help to simplify
formulas.
This semantics is a generalisation of the semantics of efls. For efls, the
set N1 consists of pairs (Γ, φ), but in this general semantics one can update with
anything. The set N2 consists, in the case of efls, of the formulas N2 = {2φ|φ ∈
Lp }. The question is whether such a semantics can be evaluated in polynomial
time. If so, then the model checking problem is tractable, and thus this logic can
be used in practice for protocol verification.
Whether model checking is tractable, depends on the function f . This function
should be easily computable, but it should also not create bigger and bigger
models. If a function f has these two properties, it is called polynomial shrinking.
5.4.2. Definition. A function f is polynomial shrinking iff kf (a, b)k < kak+kbk
and f can be computed in polynomial time.
This theorem can be used to show that update logics that are based on an update
function f with the right properties, have a tractable model checking problem.
In the next theorem it is shown that the efls update function indeed behaves
well (i.e. that it is polynomial shrinking).
5.4.4. Theorem. The function f : (M, (Γ, φ)) 7→ U p(M, σΓe (φ)) is polynomial
shrinking
A simple model checking program for efls has been implemented. The program
can be found at www.csc.liv.ac.uk/~sieuwert/glp.
The preceding theorem and its proof suggest that one can construct many
logics that can be model checked in polynomial time. Should we not search for
a more expressive logic than efls? At the same time one can wonder whether
polynomial shrinking is indeed a necessary requirement for the construction of
a polynomially model checkable logic. In order to investigate these issues, two
conceivable extensions of efl and efls are defined. The first one, efln, is an
5.5. Extensions of EFL 89
extension of efl that allows one to form nested abilities. This logic allows one
to express interesting properties, but has a very high model checking complexity.
The next logic, eflns, is an extension of efls that is supposed to capture
both nesting and side effects. This logic seems intuitive, but it is hard to give a
proper semantics for this language.
A b A ¬b a↔bAa ∇ b A
a a ¬a ¬a
ab a b
Figure 5.5: A’s strategy for letting B decide
The objective of a QBF problem is to decide for a given formula of the form
∀x1 ∃x2 ∀x3 . . . ∃xn−1 ∀xn φq whether this formula holds. The formula φq is a propo-
sitional logic formula with only propositions from the set {xi |0 < i ≤ n}. Assume
that a QBF formula ∀x1 ∃x2 ∀x3 . . . ∃xn−1 ∀xn φq is given. We have to construct an
equivalent efln decision problem.
First we construct an interpreted game form F = ({X}, H, turn, P, π). Define
Pq to be the old set of atomic propositions: Pq = {xi |0 < i ≤ n}. The set
P = {q + , q − |q ∈ Pq } contains twice as many atomic proposition: for every old
proposition q there is a positive occurrence q + and a negative one q − . The set
H is defined as H = {, p|p ∈ P }. Each terminal run thus consists of one atomic
proposition. Naturally, turn() = X and π(p) = {p}.
We can thus construct the required formula φ in the following way. Suppose
that φq is in conjunctive normal form. Define a function f in the following way.
f (¬p) = 3p−
f (p) = 3p+
f (φ ∧ ψ) = f (φ) ∧ f (ψ)
f (φ ∨ ψ) = f (φ) ∨ f (ψ)
This function converts a propositional formula φ into an efln formula. It is
used in order to convert the propositional part φq into efln. The next definition
defines an efln formula ξi that expresses that all propositions xj with j < i have
been assigned a value, whereas the propositions xj with j > i do not have been
given a value yet.
^ ^
− −
ξi = ((3x+ j ) ∇ (3x j )) ∧ ((3x+
j ) ∧ (3xj ))
j≤i j>i
The idea used here is that a nondeterministic strategy for the constructed model
can be seen as a truth value assignment for the original QBF problem. If the
−
strategy includes x+i then xi is true in the corresponding assignment, and if xi is
included in the strategy then xi is false in the corresponding assignment. The part
−
(3x+ j ) ∇ (3xj ) expresses that exactly one of those two actions must be possible,
and thus ensures that the assignment is consistent. The formula ξi expresses that
−
for j > i, both actions must still be possible: (3x+ j ) ∧ (3xj ). This is necessary
because this choice has to be made later.
Next a function g is defined so that F |= g(∀x1 ∃x2 ∀x3 . . . ∃xn−1 ∀xn φq ) iff
the QBF statement ∀x1 ∃x2 ∀x3 . . . ∃xn−1 ∀xn φq holds. The function g is defined
recursively, so that agent X can at each step pick the truth value of exactly one
propositional variable xi .
g(φq ) = f (φq ) if φq ∈ Lp
g(∃xi φ) = [X](ξi ∧ g(φ))
g(∀xi φ) = ¬[X](ξi ∧ ¬g(φ))
92 Chapter 5. Politeness and Side Effects
X
p+ p− q + q −
p+ p− q+ q−
Figure 5.6: The model Fpq
The length of the formula g(φ) is quadratically bounded: kg(φ)k ≤ kφk2 . Thus,
for a given QBF problem, we have constructed an equivalent efln model check-
ing problem in polynomial time.
To give an example of how the proof works, consider the QBF problem
∀p∃q(p ∨ ¬q) ∧ (¬p ∨ q). The model Fpq of the corresponding model checking
problem is pictured in figure 5.6. As explained at the end of the proof, the corre-
sponding formula φ is rather long, so it is broken down in parts, called ξ0 , ξ1 and
ψ.
One can verify that Fpq |= φ, and thus the QBF problem ∀p∃q(p∨¬q)∧(¬p∨q)
has a positive answer. It is interesting to see in this example that one agent alone
makes things hard for itself, by denying itself certain rights. Since there is only
one agent, this is arguably not even game theory but decision theory. In this
framework the way single agents influence their own abilities is the cause of the
complexity. The extension to multiple agents comes for free.
5.5.3. Definition. Suppose that Σ and P are finite sets (of agents and atomic
propositions), with typical elements Γ ∈ Σ and p ∈ P . The language eflns
consists of formulas ψ generated by the following rules.
φ ::= p | φ → φ | ⊥
ψ ::= [Γ : ψ]ψ | 2φ | ψ → ψ | ⊥
The official reading of a formula [Γ : φ]ψ is that if Γ wants φ, then ψ holds. The
background assumption is again that if Γ forms a certain plan or adopts a certain
strategy, all agents know this strategy immediately (strategies are visible, one
might say).
This language is not literally an extension of all logics presented before, but
one can easily translate efl, efls and eflns formulas into this language. The
efl formula [Γ]φ translates to [Γ : 2φ]2φ. The efls formula [Γ : φ]ψ translates to
the eflns formula [Γ : 2φ]ψ, and the efln formula [Γ]φ translates into [Γ : φ]φ.
These translations preserve the intuitive meaning of each formula.
We would like to define a semantics for this logic on interpreted game forms
M , that is consistent with the semantics of efl, efls and efln. Thus, if for some
model M it holds that M |= [Γ]φ (using the efln semantics), then M |= [Γ : φ]ψ
under the eflns semantics. Another item on the wish list is that the semantics
is an update semantics.
This section contains two results related to possible interpretation of eflns.
First we give a possible interpretation that is consistent with the semantics of
efln, and show that under this semantics the new logic is not more expressive
than efln. Secondly, we show that there is no reasonable update semantics for
this language that is consistent with the semantics of efln. From these results
one can conclude that defining a logic for reasoning about politeness and side
effects at the same time is not trivial.
The main drawback of this semantics is not that it is unreasonable, but that
it does not bring us more expressivity than we already had. Everything one can
say in eflns is under this semantics equivalent to something one could already
express using an efls formula.
5.5.4. Theorem. For every formula φ ∈ eflns one can find a formula ψ ∈
efln such that for any interpreted game form F the following holds
F |= φ ⇔ F |= ψ
Proof. This claim is proven using induction over the structure of the formula
φ ∈ eflns. The base case is provided by formulas φ = ⊥ and φ = 2φ1 . Both
these constructs appear in both languages and are interpreted in the same way,
so one can take ψ = φ.
For φ = φ1 → φ2 , one can take ψ = ψ1 → ψ2 , where ψ1 , ψ2 ∈ efln are
formulas that are equivalent to φ1 , φ2 respectively. The induction hypothesis
guarantees that these formulas exist.
The difficult case is thus the new construct [Γ : φ1 ]φ2 . This formula holds on a
model F if Γ has a strategy that satisfies both φ1 and φ2 . This can be expressed in
efln using the formula ψ = [Γ](ψ1 ∧ ψ2 ). Again ψ1 , ψ2 ∈ efls are formulas that
are equivalent to φ1 , φ2 respectively. The induction hypothesis again guarantees
that these formulas exist.
Second Interpretation The previous result shows that if one does not use an
update semantics based on a unique ‘rational’ strategy, it becomes difficult to
express side effects. Saying that some strategy for φ has ψ as a side effect is not
the same as saying that the best or most rational strategy for φ has ψ as a side
effect.
In order to make this last statement, one would like to have is an update
semantics based on an update function f . This function f should return the
model f (F, Γ, φ) that one gets when Γ uses the rational or most obvious strategy
for obtaining φ.
The next theorem shows that one cannot easily find such an update semantics
for eflns. To be precise we show that there is no non-arbitrary update semantics
that is consistent with the interpretation of efls. Any update semantics would
have to make arbitrary choices about which strategies it considers rational.
5.5.5. Fact. There is no reasonable update semantics for the language eflns
that is consistent with the interpretation of efln.
5.5. Extensions of EFL 95
1 2
p q
Proof. An update semantics for eflns would have the following form. As a
model we again use an interpreted game form F = (Σ, H, turn, P, π). The symbol
f is used for the update function.
F |= ⊥ never
F |= φ → ψ iff not M |= φ or M |= ψ
F |= 2φ iff ∀h ∈ Z(H) : π(h) |= φ
F |= [Γ : φ]ψ iff f (F, Γ, φ) |= ψ
F6 |= [A](2p ∇ 2q)
Under the given update semantics for the language eflns the following transla-
tion of this formula should hold.
F6 |= [A : 2p ∇ 2q](2p ∇ 2q)
Since this is an update semantics, one can apply the following validities for update
semantics, that were already stated in section 5.4.
F6 |= [A : 2p ∇ 2q]2p ∇ [A : 2p ∇ 2q]2q
96 Chapter 5. Politeness and Side Effects
And thus exactly one of the following two formulas must hold.
F6 |= [A : 2p ∇ 2q]2p
F6 |= [A : 2p ∇ 2q]2q
In the model F6 , the propositions p and q play a symmetric role. All previous
logics have a semantics that does not depend on irrelevant properties such as the
ordering of propositions or actions. Therefore, one would expect a reasonable
semantics not to treat the propositions p or q differently. Any choice for one of
the two similar formulas would be arbitrary, and would thus be unreasonable.
The word reasonable used in the previous fact is of course a vague word. The
word has been interpreted in the proof as meaning that any semantics should
behave similar in symmetric situations.
The proof is based upon the fact that there are two incompatible strategies
for bringing about A’s goal 2p ∇ 2q. In the interpretation of efln, the idea of
using the most general strategy was used to solve such dilemmas. Such a strategy
would leave the agent with the most freedom, and thus it would be rational for
the agent to use such a strategy. Unfortunately, for the example goal 2p ∇ 2q
neither effective strategy is more general than the other.
5.6 Conclusion
This chapter defines three new languages efls, efln and eflns that are richer
variants of the logic efl. Using these richer languages one can distinguish pro-
tocols that are equivalent for efl. These languages are thus useful for choosing
between protocols.
To illustrate this conclusion with some examples, consider again the following
two problems.
Both problems can be described in efl, and different protocols for both problems
exist. From the viewpoint of efl, all these protocols are equivalent. In this
chapter, we have seen that the logic efls can be used to distinguish two protocols
for the joint decision problem.
The logic efln on the other hand can distinguish the two solution for the
independent decision problems. Thus, the added expressibility of both logics
allows us to answer more detailed questions about protocols.
5.6. Conclusion 97
For each of these logics one can determine the complexity of the model check-
ing problem, which indicates whether the language can be used for verification in
practice. The next table lists these results.
P
efln
PSPACE-complete
eflns
PSPACE-complete
This chapter is based on joint research with Olivier Roy and Johan van Ben-
them.
6.1 Introduction
The logic efl presented in chapter 4 provides a high level view of protocols. It
can distinguish some protocols, but many protocols that somehow feel different
are equivalent according to the logic efl. One explanation for this result is that
agents, according to efl act without knowledge of the plans of other agents.
They search for strategies that lead to success no matter what the other agents
do. This approach is in stark contrast with the usual assumptions of game theory.
Under the assumption of complete information, agents know the preferences of
other agents. Therefore, agents can predict what other agents do, and use this
to their advantage. In order to provide a logical model that does recognize the
importance of agent preferences, we introduce in this chapter a logic based on
preference logic.
Consider the two protocols in figure 6.1. In these games, two agents A and
B are faced with the problem of a dirty shared desk. The value of a clean desk
is 2 for each agent, but the task of cleaning is valued at utility −1. The game
A B
2 B 2 A
1 1
1 2 1 2
1 2 0 2 1 0
2 1 0 1 2 0
99
100 Chapter 6. Preference Logics in Extensive Games
on the left models the situation where Alice arrives first at the office. She can
decide to clean the desk, which gives her utility 1. She can also ignore the dirty
desk. When Bob arrives and the desk is clean, he experiences utility 2. If Alice
has not cleaned the desk, Bob can clean the desk. This gives him utility 1 and
Alice utility 2. Bob’s other option is to ignore the problem, in which case both
agents experience utility 0.
The game on the right is very similar, except that in this game Bob is the first
agent to arrive at the office. The roles of the two agents are thus reversed. The
central question about these two games is whether these games are equivalent. If
that is the case, then apparently either mechanism is a fair way for both agents
to jointly decide whether to clean. If however these games are not equivalent,
then one agent might have an advantage over the other agent.
The assumption of complete information that is common in game theory tells
us that agents are not only aware of their own preferences, but also of each other’s
preferences. Thus, both agents do not only know that they want a clean desk, but
they also know that the other agent wants exactly the same. This information
can be used by agents to their advantage. The agent that arrives first, Alice in
the left game, knows that the other agent prefers a clean desk. If she does not
clean the desk, then it is best for Bob to do the cleaning. Since she knows this,
she decides to ignore the problem. The rational outcome of the left game is thus
that Bob cleans the desk. The rational outcome of the right game is that Alice
does the cleaning. Both games are thus not equivalent for the agents, and each
agent is motivated to arrive first.
The outcomes of both games that are predicted above are subgame perfect
equilibria: The first agent reasons what will happen in the subgame where she
does not clean the desk, and uses this information to decide whether she should
clean. Such a subgame perfect equilibrium can be computed using a procedure
called backward induction, and these terms are considered synonyms here. In this
chapter, a logic is presented that can capture this reasoning. Since it seems that
this preference logic might be interesting in its own right, a completeness proof
for this logic is also given.
The structure of this chapter is the following. We define the language of
preference logic in section 6.2. In this section we define a semantics for this
language, a notion of bisimulation and a proof system. Since this language is
defined in what one can call a non-modal-logic style, the competeness proof of the
defined proof system is rather hands-on. Therefore, the next section, section 6.3,
is used to define what one can call a modern variant of preference logic. For this
logic, a completeness proof using standard modal logic techniques can be given.
Section 6.4 combines preference logic with a logic for reasoning about game trees.
This combined logic is used in section 6.5 to characterize the backward induction
solution concept.
6.2. Preference Logic 101
6.2.1. Definition. Suppose the finite sets Σ and P are given, and let X ∈ Σ and
p ∈ P be typical elements. Preference logic LP consists of formulas φ generated
by the following rule.
φ ::= p | φhPref iX φ | φ → φ | ⊥
A logic for reasoning about preferences with a very similar syntax was already
proposed in 1963 [119]. However our interpretation for this language is original.
One can introduce other operators by definition in terms of the given operators.
Besides the usual logical connectives, one can define the following.
def
EX φ = φhPref iX φ
def
AX φ = ¬EX ¬φ
def
φ[Pref ]X ψ = ¬(ψhPref iX φ)
Whether the principle expressed by this formula holds for a given relation,
depends of the constraints that we put on such relation. Three properties of
relations turn out to be important. A relation R is total if ∀xy : x 6= y ⇒ (xRy ∨
yRx). It is reflexive if ∀x : xRx, and anti-symmetric if ∀xy : (xRy ∧ yRx) →
x = y. The strict version Rs is the relation Rs = {(a, b)|aRb ∧ ¬bRa}. A relation
R is strict-transitive if ∀xyz : xRs y ∧ yRs z → xRs z. In normal circumstances
one would expect a preference relation to be total, strict-transitive and reflexive.
These properties reflect reasonable properties that one would expect from a
preference relation. If one assumes that preferences follow from an underlying
utility relation, these properties should hold. Indeed these three properties are
used in the definition of a preference model, defined below.
q
r
p
s
M, w |= ⊥ never
M, w |= p iff p ∈ π(w)
M, w |= φhPref iX ψ iff ∃(w 0 , w 00 ) ∈X : M, w 0 |= φ and M, w 00 |= ψ
M, w |= φ → ψ iff not M, w |= φ or M, w |= ψ
Let M be the model displayed in figure 6.2 and let wp be the world where p holds.
Then we can show the following.
M, wp |= p ∧ (phPref iX s) ∧ (qhPref iX r)
In standard modal logic, an accessibility relation is used in the interpretation
of modal operators. The truth conditions of the modal operator only depend on
accessible worlds. The preference operator hPref iX looks at all worlds, so one
might say it uses the universal accessibility relation, in which any world is related
to any world. Such an operator is called a global operator. In the following
lemma it is shown that such an operator can be used to define the operator Eφ
that expresses that a world satisfying the formula φ exists.
6.2.5. Lemma. Let M = (W, Σ, {}Σ , P, π) be a minimal preference model
M, w 0 |= EX φ ⇔ ∃w ∈ W : M, w |= φ
6.2.1 Bisimulation
In this section we define a notion of bisimulation for preference models, and prove
that two models are bisimilar if and only if they satisfy the same preference logic
formulas.
104 Chapter 6. Preference Logics in Extensive Games
• all pairs of related worlds (w, w 0 ) ∈ R satisfy the same atomic propositions:
π(w) = π 0 (w 0 ) and
We say that two pointed models M, w and M 0 , w 0 are bisimilar , iff there exists a
bisimulation R between M and M 0 such that (w, w 0 ) ∈ R. Two pointed models
M, w and M 0 , w 0 are equivalent iff they satisfy exactly the same formulas: ∀φ :
M, w |= φ ↔ M 0 , w 0 |= φ. The next theorem relates these two notions.
6.2.7. Theorem. Let P be finite and let M, w = (W, Σ, {}X∈Σ , P, π), w and
M 0 , w 0 = (W 0 , Σ, {0 }X∈Σ , P, π 0 ), w 0 be two pointed models. The models M, w and
M 0 , w 0 are bisimilar iff they are equivalent .
p
q p q
p
Figure 6.3: Two bisimilar models
Using this notion, one can determine whether two models satisfy the same for-
mulas. In figure 6.3 two bisimilar models are displayed. In the right model, two
equally good states are displayed, one of them is labeled with proposition p, the
other one with proposition q. The left model has three states that are not equally
preferred by the single agent of this model. The left p state is better than the q
state, which is better than the right p state. (Again the preferences are indicated
by the vertical position of the states.)
E − intro φ → EX φ
The reasoning rules for this proof system are Modus Ponens and Necessitation
for AX . These two rules are listed below.
φ φφ→ψ
AX φ ψ
The following rules can be derived in this system.
The first rule OrDist1 can be derived using the following instance of AndDist1 :
l(⊥) =0
l(p) =0
l(φ → ψ) = max(l(φ), l(ψ))
l(φhPref iX ψ) =1 + max(l(φ), l(ψ))
The language of preference logic allows for nested preference operators, but it is
not clear what such nested formulas express. Does it make sense to say that “to
prefer φ over ψ is at least as good as χ”? Someone who holds that such sentences
are meaningless may decide to exclude them from the logic by restricting the
language to L≤1P = {φ ∈ LP |l(φ) ≤ 1} where nesting of operators is not allowed.
We have decided to keep our approach as general as possible on this point, so we
did not use this restriction. But, interestingly enough, using axioms AndConv1
and AndConv2 one can show that we can always ‘unnest’ a nested formula: a
formula of nesting l > 1 is always equivalent to a formula of nesting (l − 1). This
is proven in the next lemma. This equivalence plays a role in the completeness
proof, and it shows that even if we can nest preference formulas, such nesting
does not add to the expressivity of the language.
6.2.8. Lemma. For all formulas φ ∈ LP with l(φ) > 1 there is a formula χ such
that SP `φ ↔ χ and l(χ) = l(φ) − 1
Proof. We prove that the theorem holds for φ = ψhPref iX ξ. For other formulas
φ it follows by an induction argument.
6.2. Preference Logic 107
ψhPref iX ξ
⇔ P rop, N ecA , K1,2
[dnf (ψ)]hPref iX [dnf (ξ)]
⇔
1 2 1 2
[∨m ∧j ±(ψmj hPref iY ψmj )) ∧ ψ p ]hPref iX [∨k ∧l ±(ξkl hPref iY ξkl )) ∧ ξ p ]
⇔ OrDist1,2
1 2 1 2
∨m ∨k [∧j ± (ψmj hPref iY ψmj ) ∧ ψ p ]hPref iX [∧l ± (ξkl hPref iY ξkl ) ∧ ξ p]
⇔ AndConv1,2
1 2 1 2
∨m ∨k (∧j ± (ψmj hPref iY ψmj )) ∧ (∧l (ξkl hPref iY ξkl )) ∧ [ψ p hPref iX ξ p ]
def
= χ
One can see that l(χ) = l(φ) − 1 by noting that l(χ) = max(l(ψ), l(ξ)) and
l(φ) = 1 + max(l(ψ), l(ξ)).
• (Exist) Suppose M, w |= φhPref iX ψ. This means that there are two worlds
w 0 and w 00 such that w 0 w 00 , and these worlds satisfy M, w 0 |= φ and
M, w 00 |= ψ. Since the relation Y is reflexive for all agents Y , we obtain
108 Chapter 6. Preference Logics in Extensive Games
• (K1 - K2 ). It is not hard to see that AX φ is true iff φ holds in every world
of the model.
Suppose that M, w |= AY (φ → ψ) and M, w |= φhPref iX χ, for arbitrary
agents X and Y . This means that there are w1 , w2 ∈ W such that w1 X w2 ,
M, w1 |= φ and M, w2 |= χ. Furthermore for all worlds w 0 ∈ W we have
M, w 0 |= (φ → ψ). In particular, this last fact implies that M, w1 |= φ →
ψ, from which we get M, w1 |= ψ. Since w1 X w2 , we have M, w |=
ψhPref iX χ. The argument for K2 is similar.
equivalent maximally consistent formulas are exactly equal. Let S prop consist of
all propositional logic formulas in S, and let S max = {φm hPref iX ψ m ∈ S|φm , ψ m
are maximal propositional conjunctions}. The proof now proceeds as follows. We
first construct a model M such that there is a state w in M so that M, w |= φ for
all φ ∈ S prop and such that every state in M satisfies all formulas in S max . Then
we show that M, w satisfies all formulas in S.
The model M = (W, Σ, , P, π) is defined in the following way. Let W =
{φm |(Eφm ) ∈ S max }. So W contains maximal propositional conjunctions. Σ is
the set of agents mentioned in S, and this set is finite because only a finite number
of agents can be mentioned in a finite formula. We define π(φm ) = {p| SP `φm →
p}. The preference relation is defined by φm X ψ m ⇔ (φm hPref iX ψ m ) ∈ S max .
This relation is reflexive: If (φm hPref iX ψ m ) ∈ S max then, because of Exist, we
know EX φm = φm hPref iX φm ∈ S max . Similarly for ψ m .
The world w that we need can be found in the following way. Suppose that
φ ∈ S prop for a maximal propositional conjunction φm . This implies, using
m
An induction argument over the level of nesting in sets S can be given to show
that φ ∈ S iff M, w |= φ for any formula φ with l(φ) ≤ 1. To show that this is
also the case for higher level formulas, with nested preferences, we can use lemma
6.2.8 to find for any formula φ a formula ξ such that SP `φ ↔ ξ and l(ξ) ≤ 1.
If φ ∈ S then ξ ∈ S, and since l(ξ) ≤ 1 we can find a model M, w such that
M, w |= ξ. It now follows that M, w |= φ, and we have shown that the given
110 Chapter 6. Preference Logics in Extensive Games
6.2.12. Theorem. T otal is a sound and complete axiom scheme for the set of
reflexive frames with total preference relations.
Proof. Suppose that M = (W, Σ, {X }X∈Σ , P, π) is a model such that all
relations X are total and let w ∈ W . Assume that M, w |= EX φ ∧ EX ψ. This
means that there are two worlds x, y ∈ W such that M, x |= φ and M, y |= ψ.
From totality we know that either x X y or y x. In the first case, we have
M, w |= φhPref iX ψ and in the second case M, w |= φhPref iX ψ. Either way this
leads to M, w |= (φhPref iX ψ ∨ ψhPref iX φ). Thus, T otal is sound for reflexive
frames with total preference relations.
For the second part assume that (W, Σ, {X }X∈Σ ) is a non-total reflexive
frame. This means that for some X and x, y ∈ W it is the case that neither
x X y nor y X x. Define P = {p, q} and π(x) = {p}, π(y) = {q} and for
all remaining worlds z : π(z) = ∅. Let M = (W, Σ, {X }X∈Σ , P, π). This model
satisfies M, x |= (EX p ∧ EX q). However, M, w |= (phPref iX q ∨ qhPref iX p) does
not hold. Thus, M, x |= (EX p ∧ EX q) → (phPref iX q ∨ qhPref iX p) does not hold.
Therefore, T otal is complete for the class of total reflexive frames.
6.2.13. Theorem. T otal are sound and complete axioms for the set of reflexive
frames with strict-transitive, total preference relations.
Proof. Note that the transitivity axiom implies totality: Take φ = ξ. Thus, if
we add the axiom T rans then T otal is derivable.
First we prove the soundness of T rans on strict-transitive, total reflexive
frames. Suppose that M = (W, Σ, {X }X∈Σ , P, π) is a model such that all
relations X are total and strict-transitive, and let w ∈ W . Assume that
M, w |= (EX ψ ∧ φhPref iX ξ). This means that there are three worlds x, y, z ∈ W
such that M, x |= φ, M, y |= ψ, M, z |= ξ and x X z. In order to obtain a
contradiction, assume that M, w |= ¬(φhPref iX ψ) ∧ ¬(ψhPref iX ξ). Since the
6.3. An Alternative Preference Logic 111
p r
6.3.1. Definition. Suppose the finite sets Σ and P are given, and let X ∈ Σ and
p ∈ P be typical elements. Alternative preference logic L2P consists of formulas φ
generated by the following rule.
φ ::= p | 3X φ | Eφ | φ → φ | ⊥
In this logic, the operator φhPref iX ψ can be defined as E(φ ∧ 3ψ). Intuitively
the meaning of 3X φ is that there is a state better for X than the current state,
in which φ holds. The construct Eφ means that somewhere in the model a state
exists in which φ holds. For this logic we define the operators 2X φ = ¬3X ¬φ
and Aφ = ¬E¬φ. These operators are thus duals for the two primitive operators.
This logic is interpreted in the following way. Let M = (W, Σ, , P, π) be a
preference model.
M, w |= ⊥ never
M, w |= p iff p ∈ π(w)
M, w |= Eφ iff ∃w 0 ∈ W : M, w 0 |= φ
M, w |= 3X φ iff ∃(w, w 0 ) ∈X : M, w 0 |= φ
M, w |= φ → ψ iff not M, w |= φ or M, w |= ψ
The operator 3X is interpreted in the standard modal logic fashion using the
relation X . The operator Eφ also has a standard interpretation, but based on
the universal relation. All worlds are accessible to this operator.
6.3.2. Fact. Alternative preference logic L2P is strictly more expressive than
preference logic LP .
Axioms for 3
K 2X (φ → ψ) → (2X φ → 2X ψ)
4 3 X 3X φ → 3 X φ
T φ → 3X φ
Axioms for E
KE A(φ → ψ) → (Aφ → Aψ)
4E EEφ → Eφ
TE φ → Eφ
BE φ → AEφ
Incl 3X φ → Eφ
Tot (Eφ ∧ Eψ) → (E(φ ∧ 3X ψ) ∨ E(ψ ∧ 3φ))
The reasoning rules for this logic are Modus Ponens, Necessitation for 2X φ and
necessity for Aφ. These three rules are listed below.
φ φ φ φ→ψ
2X φ Aφ ψ
6.3.3. Theorem. The proof system L2P is sound and complete for the language
L2P on minimal preference models with transitive preference relations.
Proof. It is clear that the axioms are sound and that the reasoning rules pre-
serve validity: they are all standard axioms. The logic is complete with respect to
the class of reflexive and transitive frames, see [12, p.417]. To see that the logic
is complete with respect to the class of reflexive, transitive and linear frames,
just notice that Lin, the axiom for linearity, is a Sahlqvist formula. Applying
the algorithm of the Sahlqvist Correspondence Theorem [12, p.165] one sees that
it corresponds to the first order expression of linearity: ∀x, y(x y ∨ y x).
Furthermore, by the canonicity of Sahlqvist formulas, [12, p.322], we know that
the canonical model for L2P is linear, and so that L2P is complete with respect to
the class of reflexive, transitive and linear frames.
6.4.1. Definition. Suppose the finite sets Σ and P are given, and let X ∈ Σ and
p ∈ P be typical elements. Finite tree logic LT consists of formulas φ generated
by the following rule.
6.4.2. Definition. Let {RX }X∈Σ be S an indexed set of relations RX , one for
each agent X ∈ Σ. We define R = {RX }X∈Σ as the union of all relations in
{RX }X∈Σ and R+ as the transitive closure of R.
The worlds W \ W T are not related by the relation R to any other worlds. These
so-called ‘loose worlds’ are not reachable by actions, but are important in the
preferences of agents.
We define the set of terminal nodes Z(W, R) by Z(W, R) = {w ∈ W |¬∃w 0 :
wRw 0 }. The reach function reach(R, w) is the set of points reachable from w and
can be defined by stating that reach(R, w) is the smallest set S such that w ∈ S
and x ∈ S ∧ xRy ⇒ y ∈ S.
6.4.5. Definition. A preference tree model M is a tuple M = (W, Σ, {RX }X∈Σ , {X
}X∈Σ , P, π) such that (W, Σ, {RX }X∈Σ , P, π, ) is a tree model and for each agent
X ∈ Σ the relation (X ) ⊆ Z(W, R) × Z(W, R) is a reflexive, strict-transitive,
total relation.
M, w |= ⊥ never
M, w |= p iff p ∈ π(w)
M, w |= φ → ψ iff M, w |= φ implies M, w |= ψ
M, w |= hXiφ iff ∃w 0 : wRX w 0 such that M, w 0 |= φ
M, w |= hΣiφ iff ∃X, w 0 : wRX w 0 such that M, w 0 |= φ
M, w |= hΣ+ iφ iff ∃w 0 : wR+ w 0 such that M, w 0 |= φ
M, w |= φhPref iX ψ iff ∃(u, v) ∈ (X ) such that M, u |= φ and M, v |= ψ
6.4. Finite Tree Logic 115
As an example of how this logic can be used, consider the protocol displayed
in figure 4.1 on page 4.1. This protocol can be described as a preference tree
model M1 , if we indicate what the preferences of the agents are. One possible set
of preferences has therefore been indicated in the next table.
Agent Most to least preferred outcomes
A x, y, z
B y, x, z
C z, x, y
It is assumed here that the utility that an agent attaches to a certain outcome,
only depends on the atomic propositions that hold on a certain outcome. This is
a reasonable assumption, since these atomic propositions are supposed to encode
the relevant properties of each outcome. Thus, according to the table, A prefers
both x outcomes above both y outcomes, and both y outcomes over both z
outcomes. The first two formulas describe the structure of the game, and the
last formula refers to the preferences. Let wA be the root of model M1 , and let
φ⊥ = [Σ]⊥. The formula φ⊥ holds in terminal states.
6.4.6. Definition. The proof system ST for finite tree logic consists of the rule
Modus Ponens and the following axioms.
The following formula is known in dynamic predicate logic as the induction prin-
ciple.
φI = ([Σ]φ ∧ [Σ+ ](φ → [Σ]φ)) → [Σ+ ]φ
This formula scheme is valid for finite tree logic. Here we show that this axiom
can be derived from the other principles.
6.4.7. Theorem. The induction principle can be derived in finite tree logic:
ST `φI
116 Chapter 6. Preference Logics in Extensive Games
Proof. Define α as the negation of φI : α = ([Σ]φ ∧ [Σ+ ](φ → hΣiφ)) ∧ ¬[Σ+ ]φ.
The Löb axiom L can be formulated as
ST `[Σ+ ]([Σ+ ]φ → φ) → [Σ+ ]φ
and axiom trans can be expressed equivalently as
ST `[Σ+ ]φ ↔ ([Σ]φ ∧ [Σ+ ]φ)
Using this formulation of the trans axiom, one can show that
ST `α ↔ ([Σ]φ ∧ [Σ+ ](φ → [Σ]φ)) ∧ ¬[Σ](φ ∨ [Σ+ ]φ)
This can be simplified, because [Σ]φ appears twice in this formula.
ST `α ↔ ([Σ]φ ∧ [Σ+ ](φ → [Σ]φ)) ∧ ¬[Σ][Σ+ ]φ
And one can bring the negation inside:
ST `α ↔ ([Σ]φ ∧ [Σ+ ](φ → [Σ]φ)) ∧ hΣi¬[Σ+ ]φ
Using trans again and Modus Ponens gives
ST `α ↔ ([Σ]φ ∧ [Σ][Σ]φ ∧ [Σ][Σ+ ](φ → [Σ]φ)) ∧ hΣi¬[Σ+ ]φ
One can now derive three implications from this formula.
ST `α → [Σ][Σ]φ
ST `α → [Σ][Σ+ ](φ → hΣiφ)
ST `α → hΣi¬[Σ+ ]φ
These three statements combine to the following conclusion
ST `α → hΣi([Σ]φ ∧ [Σ+ ](φ → [Σ]φ)) ∧ ¬[Σ+ ]φ)
This statement is the same as ST `α → hΣiα
Using contraposition this leads to ST `[Σ]φI → φI
From trans one can derive that ST `[Σ+ ]φI → [Σ]φI
And these can be combined into ST `[Σ+ ]φI → φI
The necessitation rule can be used to derive ST `[Σ+ ]([Σ+ ]φI → φI )
From L now follows ST `[Σ+ ]φI
and thus (with Modus Ponens) ST `φI
This proof system is complete, and the proof for this fact is given below in
several steps. It is a straightforward adaptation from Blackburn and Viol [13],
except that we have translated notations where necessary. Blackburn and Viol
introduced this logic for the finite binary trees that are used in linguistics as parse
trees. Our adaptation shows that this logic can also be used for game trees.
6.4. Finite Tree Logic 117
6.4.8. Definition. The closure cl(Φ) of a set of formulas Φ is the smallest set
S such that the following hold.
If Φ is a finite set, then cl(Φ) is finite. From now on we assume that Φ is a finite
set.
Proof. Suppose that ST `¬(φ ∧ hΣ+ i¬φ). Using necessitation one can derive
that ST `¬hΣ+ i(φ ∧ hΣ+ i¬φ). The Löb axiom can now be used in contra positive
form (thus ¬b → ¬a instead of a → b). This gives us ST `¬φ. Another way to put
118 Chapter 6. Preference Logics in Extensive Games
this is to say that if φ is consistent (ST 6 `¬φ), then (φ ∧ hΣ+ i¬φ) is consistent:
ST 6 `¬(φ ∧ hΣ+ i¬φ).
Suppose now that A and B together form a partition of At(Φ): All atoms
appear in A or B but not in both. One can V show using W the result
V of the previous
+
paragraph that there is an Ai ∈ A such that Ai ∧[Σ ]( Bj ∈B Bj ) is consistent.
The proof for this observation is the following.
W V W V
TheWdisjunction Ai ∈A Ai is consistent and therefore (observation 1) ( Ai ∈A Ai )∧
[Σ+ ]¬ Ai ∈A Ai is consistent. Since A and B form a partition of a set At(Φ) of
V
all maximally W V subsets, ifWno setVin A is satisfied then a set of B must
consistent
be satisfied: ¬ Ai ∈A Ai implies Bj ∈B Bj . This leads to the conclusion that
( Ai ∈A Ai ) ∧ [Σ+ ]( Bj ∈B Bj ) is consistent and thus for some Ai ∈ A we have
W V W V
the set Si and At(Φ) \ Si form a partition of At(Φ). This proves the observation.
We can use the observation that we have just proven to see that if Li+1 exists,
then it is non-empty. Every level i the set Si thus gets bigger. Since At(Φ) is a
finite set, eventually Si = At(Φ) and every atom has been assigned to a certain
level. For the proof of the lemma, suppose A ∈ Li and hXiφ ∈ A. It is clear that
i > 0 and thus Si−1 exists. To obtain a contradiction, suppose that V there isVno
atom B ∈ Si−1 such that ARX B, thusV that for all B
V the formula
V A ∧ hXi B
is inconsistent. This means that ST ` A ∧ [X]¬( B∈Si−1 B). As a shortcut,
define B = B∈Si−1 B. Since A ∈ Li , we have that A ∧ [Σ+ ]B is consistent.
V V V
V V V
Since we canV rewrite [Σ] as Y [Y ], we know that A ∧ Y [Y ]B is consistent and
thus that A ∧ [X]B is consistent. This yields a contradiction. Thus, there must
be an atom B ∈ Si−1 such that ARX B.
This concludes the preparations for the completeness proof, and we can prove the
completeness theorem.
Proof. We can construct a model for any formula φ. Take Φ = {φ}. Choose
A ∈ At(Φ) such that φ ∈ A. Let W0 = {A}. We call a pair (w, hXiφ) of w ∈ Wn
an unsatisfied demand if hXiφ ∈ w but there is no w 0 ∈ Wn such that wRk w 0 and
φ ∈ w 0 . As long as there are unsatisfied demands, pick one unsatisfied demand
(w, hXiφ) and take a world w 0 ∈ Lm in a set Lm such that wRX w 0 and φ ∈ W .
The world w 0 must have a lower level than w: if w ∈ Li then i < m. Lemma 6.4.11
guarantees that such a w 0 exists. Define Wn+1 = Wn ∪ {w 0 }. The construction
process must terminate after a certain number of steps, because we add worlds
with strictly lower levels every time. Thus, for some sufficiently large m, there is
a world Wm that has no unsatisfied demands.
Let the proto-model C Φ = (At(Φ), Σ, {RX }X∈Σ , P, π) be defined as before.
0
Define the following model M = (Wm , Σ, {RX }X∈Σ , P, π 0 ) where {RX
0
}X∈Σ , π 0 are
6.5. Backward Induction: An Application 119
the restrictions of {RX }X∈Σ , π to Wm . One can use induction on the structure of
the formula φ to prove that M, w0 |= φ.
It remains for us to define a preference relation over Wm . The axiom AG
establishes that all worlds that are involved in the actions, are used in the pref-
erence relation. All other axioms only deal with preferences or only with actions.
Since we have proven the preference logic to be complete, any consistent set of
preference formulas can be satisfied by a model. This model contains exactly
one state for each maximally consistent propositional formula, but we can mul-
tiply these states to obtain a bisimilar model in which we have a correspondence
between the outcomes of the action relation and the preference worlds. If some
world of the preference model cannot be mapped on the action model, a ‘loose
world’ can be created that does not form part of the game tree: Our definition of
a tree model allows for worlds that only play a role in the preference model.
Not every game has a unique backward induction relation. Take for instance
any game in which all agents value all outcomes equally. In such a game, any
relation that chooses one move for each node is a backward induction relation.
If the preference relation is anti-symmetric however, then there is exactly
one backward induction relation. Otherwise there might be more. Thus, if no
agents values a pair of nodes equally, then there exists a unique subgame perfect
equilibrium.
Below we extend finite tree logic with operators 3sol φ and 3∗sol φ that refer
to recommended moves. This new logic is called solved game logic because it is
interpreted over solved models.
6.5.1. Definition. Suppose the finite sets Σ and P are given, and let X ∈ Σ
and p ∈ P be typical elements. Solved game logic Lsol consists of formulas φ
generated by the rule
The construction 3sol φ means that one can use a recommended moved to reach a
state where φ holds. Similarly, 3∗sol φ means that one can use only recommended
moves to reach an outcome where φ holds.
This logic can be interpreted over solved models. These models are similar to
preference tree models, but contain an extra relation that describes a solution to
the game.
Note that the operator 3∗sol is interpreted such that it refers to outcome states
only. This is done because only outcome states have preferences.
In order to be able to characterize backward induction, we have to put an
extra constraint on the models that we consider. In the following definition we
define when we call a preference relation functional (with respect to a given
interpretation function π).
6.5.3. Definition. Consider a preference relation X in the context of a model
with some interpretation π. The relation X is functional if there is a function
fX : 2P → R such that for all worlds v, w we have that v X w implies fX (π(v)) ≥
fX (π(w)).
We call preference models, tree models and solved models functional if all pref-
erence relations that occur in these models are functional (with respect to the
interpretation function π of the model). If a model is function, it means that
the atomic propositions encode all properties that agents use in their preferences.
Thus, in functional models the atomic propositions are all that agents care about.
The right model in figure 6.3 is functional, but the left model is not.
The following four formulas characterize the backward induction solution con-
cept, at least for functional models. This means that all functional models on
which all instances of the following four formulas hold, have the backward in-
duction solution concept as their solution. One can thus say that the concept of
backward induction is described by the logical formulas.
In fact the first four properties hold on any solved model, because of the
constraints we have put on the solution relation. Therefore, one could say that
the fourth property characterizes backward induction. The formula B5 expresses
what kind of reasoning can be used to motivate the backward induction solution
concept, and can thus be used to explain this concept. This way of using logic
to characterize solutions concepts gives more insight in the ideas or assumptions
behind these concepts [30].
Proof. Suppose that M, w is a solved model, and that the relation Rsol is indeed
the backward induction relation BI. For each instance of formula Bi we show
that it holds in this model.
• Suppose that M, w |= hΣi>. This means that w is an internal node. From
krz(W, BI, w)k = 1 it follows that there must be a next BI move, and
therefore M, w |= 3sol >.
• Suppose that M, w |= 3sol φ, which means there is a state w 0 such that
(w, w 0 ) ∈ BI and M, w 0 |= φ. Since BI ⊆ R, it holds that (w, w 0 ) ∈ R and
thus M, w |= hΣiφ.
From krz(W, BI, v)k = 1 for all nonterminal nodes v, it follows that there
is only one state w 0 with (w, w 0 ) ∈ BI. Therefore, for any state w 0 with
(w, w 0 ) ∈ BI it is the case that M, w 0 |= φ and thus M, w |= 2sol φ.
• Suppose that M, w |= 3∗sol φ, which means there is an outcome w 0 ∈
rz(W, BI, w) so that M, w 0 |= φ. If w is an outcome itself, then w 0 = w
and M, w |= ([Σ]⊥ ∧ φ). Otherwise there is a w 00 with (w, w 00) ∈ BI and
M, w 00 |= 3∗sol φ and thus M, w |= 3sol 3∗sol φ.
• Suppose that M, w |= 3sol φ, which means that there is a state w 0 such that
(w, w 0 ) ∈ BI and M, w 0 |= φ. In the definition of a solved model it is stated
that this world w 0 is unique, and hence there are no other worlds w 00 such
that (w, w 00 ) ∈ BI. Therefore, M, w |= 2sol φ.
• Finally, assume M, w |= (3sol 2∗sol φ ∧ hXi2∗sol ψ). Thus, there is a state
w1 with (w, w1 ) ∈ BI and M, w1 |= 2∗sol φ. There is also a state w2 such
that (w, w2 ) ∈ RX with M, w2 |= 2∗sol ψ. Hence ∃v1 ∈ rz(W, BI, w 0 ) with
M, v1 |= φ and ∃v2 ∈ rz(W, BI, w2 ) with M, v2 |= ψ. The definition of the
BI relation now tells us that v1 is possibly at least as good as v2 , and thus
v1 X v2 , and therefore M, w |= φhPref iX ψ.
Proof. Suppose that a solved model M, w has preferences that are functional:
Outcomes w, w 0 with π(w) = π(w 0 ) are equally preferred. Assume that all in-
stances of B4 hold on M, w.
6.5. Backward Induction: An Application 123
B C
x y z x y z
M, wA |= x[Pref ]A y ∧ y[Pref ]A z
M, wA |= y[Pref ]B (x ∨ z)
M, wA |= z[Pref ]C (x ∨ y)
If the solution of this solved model is the backward induction relation, then it
follows from y[Pref ]B (x ∨ z) that M, wB |= 3sol y. Similarly, M, wC |= 3sol z.
Since one can derive from the first line that M, wA |= ¬(zhPref iA y), it follows
from B5 that not M, wA |= 3sol 2∗sol z and hence M, wA |= 2∗sol y. Therefore, the
indicated solution relation is indeed the backward induction solution.
After considering more different preference assumptions, one can show that
agents B and C have the best ‘chance’(assuming all different preference relations
are equally likely) to get the options they prefer most. Agent A on the other
hand is least likely to get the option it prefers least. Thus, using preference logic
one can give advice to agents which role they should take in this voting problem,
which was not possible based on efl. Agents that strongly prefer one option
should take the role of agent B or C, whereas agents that strongly dislike one of
the options are better of as agent A.
6.6 Conclusion
In this chapter, the focus has not been on model checking but on proof theory.
A language LP for reasoning has been presented and a complete proof system
for this language is given. We have also developed a more modern language for
6.6. Conclusion 125
preferences L2P , and shown that this language is more expressive than LP , while
having a proof system with a simpler completeness proof.
In section 6.4, we have used preference logic in combination with a logic for
reasoning about finite trees. This allows one to reason about extensive games.
Again a proof system for this logic has been defined, using techniques that are
standard in modal logic. The logic can be used for characterising the backward
induction solution concept. An analysis of the example voting problem of chapter
4 shows that this logic is more expressive than efl.
The most important conclusion that can be drawn from this chapter is that
modal logic, because so much is known about it, is a suitable tool for model-
ing game-theoretic reasoning. Possible future work would be to analyse other
solution concepts as well, such as iteration of dominant strategies, and the (not
subgame-perfect) Nash equilibrium. A more challenging project would be to
analyse imperfect information games. One such attempt already exists in the
form of ATEL [102], also discussed in section 7.5. Recent ATEL research has
shown that reasoning about imperfect information games is a challenging prob-
lem [3, 54, 55, 109]. It would be interesting to compare the ATEL approach, with
the more direct modal logic approach used in this chapter.
Chapter 7
Knowledge Condition Games
7.1 Introduction
In the previous chapters, we have looked at protocols that can be modelled as per-
fect information game forms. In such protocols all agents are aware of all previous
events, and therefore no aspects of the current situation are unknown. In this
chapter the focus is on protocols that can be modelled as imperfect information
game forms. Such protocols are interesting for at least two reasons:
• The knowledge that agents do and do not have of the current situation can
be used in the definition of the game. Having certain knowledge can be the
goal of an agent or a coalition of agents.
In order to study these two aspects of multi-agent protocols, we define a new class
of games, called knowledge condition games. In a knowledge condition game, two
coalitions of agents enact a protocol. One coalition strives to reach a certain
knowledge situation, and the other coalition tries to prevent the first coalition
from reaching its goal. In other words, one coalition “wins” if it is able to force a
certain condition to hold in the world, where this condition relates to the know-
ledge (and absence of knowledge) of the agents in the game. Formally, we specify
the goal situation (i.e., the condition that the agents strive to achieve) using epis-
temic logic, and protocols are modeled as interpreted game forms with imperfect
information.
After defining these games and illustrate using various examples, we focus
on the computational complexity of determining who wins a knowledge condi-
tion game under various assumptions. Specifically the following questions are
answered.
127
128 Chapter 7. Knowledge Condition Games
The complexity results also allow one to see whether reasoning about knowledge in
strategic situations is indeed a complex problem. The fact that we have collected
in this chapter many different complexity results shows that this is indeed the
case.
The structure of this chapter is as follows. In the next section, section 7.2
we have collected all necessary definitions. Section 7.3 provides four examples of
knowledge condition games. The first example shows how knowledge properties
are important in a voting protocol. The second example involves a more playful
quiz problem. It shows how signaling can enter into reasoning about knowledge.
The third example, the Russian Cards problem, is larger than the previous two
and hence the corresponding knowledge condition game is not easily solved by
hand. In the last example the use of a multi-step strategy for a coalition of
three agents is demonstrated. Section 7.4 presents four results relating to the
complexity of knowledge condition games. We prove the complexity of deciding
a knowledge condition game in which strategies are known, first for the restricted
case without opponents, then with opponents. We then do the same for knowledge
condition games in which strategies are unknown. Section 7.5 discusses some
related work, and section 7.6 presents some conclusions.
where:
7.2. Defining Knowledge Condition Games 129
A
1 2
p B
7.2.1 Strategies
Strategies are an important part of every game. Informally a strategy σΓ is a
function that tells all agents in coalition Γ what to do next in the histories they
control. We use nondeterministic strategies for our agents. These strategies have
been defined in definition 3.3.6 on page 43. Such a strategy does not return a
unique option that the agent should take, but it returns a set of options, with
the intention that the agent should randomly select an element of this set. Our
strategies are thus akin to the randomized or ‘mixed’ strategies, or more correctly
the behavioural strategies, of game theory [79, p.212], except that we do not
consider probabilities of making particular choices. Since we deal with imperfect
information games, only uniform strategies, as defined in definition 3.3.13, are
considered.
For the example interpreted game form F0 there are three different strategies
σ{A} for agent A. The strategy can either tell the agent to take the first option,
or it can prescribe the second option, or the strategy can express that the agent
should randomly choose between both options. Formally, these possibilities are
1 2 3
defined by respectively σ{A} () = {1}, σ{A} () = {2} and σ{A} () = {1, 2}.
For any strategy σΓ for an interpreted game form F we can consider a re-
stricted interpreted game form F 0 in which the agents X ∈ Γ only choose options
that are part of the strategy. The agents Y ∈ / Γ can still do whatever they want in
0
F . Such a restricted interpreted game form models the situation in which coali-
tion Γ is committed to the given strategy. The restricted model F 0 is computed
by an update function F 0 = u(F, σΓ ).
where:
• turn 0 and π 0 are the same as turn and π, but with their domain restricted
to H 0 .
7.2. Defining Knowledge Condition Games 131
3
An update of the example F0 with strategy σ{A} does not change anything:
3 1
u(F0 , σ{A} ) = F0 . An update with σ{A} returns a model F1 with only two histories:
and 1. This means that the epistemic model of F1 only has one state in which
p holds. Thus, using the interpretation of epistemic logic (defined on page 16), it
1
holds that m(u(F0 , σ{A} )), 1 |= KB p.
Take the example game form F0 and take φ0 = KB p. For the game G0 =
kcg(F0 , {A}, ∅, φ0 ) we can compute a payoff matrix. As calculated before, {A}
has three strategies. The empty coalition only has the unique empty function f∅
as a strategy.
1 2 3
σ{A} σ{A} σ{A}
f∅ (1,0) (0,1) (0,1)
1
We see that for this game, {A} has a winning strategy (namely σ{A} ). Therefore,
w(kcg(F0 , {A}, ∅, φ0 )) = 1. In the above definition, we use the updated model
m(u(u(F, σΓ ), σΞ )) as a model for what all agents know. We have thus implicitly
assumed that everybody commonly knows which strategies are used by Γ and Ξ,
r if one assumes that strategies are somehow visible to other agents. As we have
argued on page 81 in the case of perfect information games, this is a reasonable
assumption. It makes sense if one considers strategies as well-known conventions.
Also if a game is played by computer programs that are open for inspection, this
is a reasonable assumption. Finally, one can argue that assuming that no details
can be kept secret is a very conservative and thus sound assumption if one tries
to prove the correctness of security protocols. In some circumstances, however,
one might not want to make this assumption. Therefore, we present below a
variant kcg 0 of knowledge condition games in which the knowledge formulas φ
is evaluated the original model m(F ). The strategies are used to determine the
reachable states w and the proponents win if in all these states w, it holds that
m(F ), w |= φ.
The difference between kcg and kcg 0 lies in their respective utility function.
The function U evaluates the formula φ in the model m(u(u(F, σΓ ), σΞ )), in all
states. The function U0 evaluates the formula φ in the model m(F ), thus in the
model before updates. This difference reflects the idea that in kcg, strategies are
commonly known, whereas in kcg 0 they are not known. The function U0 only
evaluates the formula φ in states w that occur in m(u(u(F, σΓ ), σΞ )). The idea
here is that the truth of φ only matters in states that are actually reached, and
which states are reachable depends on the strategies chosen.
7.3. Examples 133
7.3 Examples
7.3.1 Anonymous Voting
A voting protocol can be used when a group of agents has to make a joint decision
on a certain issue. A common protocol is majority voting: Each agent can vote for
an option and the option that gets the most votes is the outcome of the protocol.
In the example interpreted game form FV = (Σ, H, turn, ∼, P, π), three agents A,
B and C use majority voting to decide whether a plan P should be accepted or
not. Thus Σ = {A, B, c} and P = {a, b, c, p}. Each agent has to choose from two
actions: support the plan (s), or reject it (r). They vote in alphabetical order,
so first A chooses between action s and r, then B (without knowing A’s choice)
chooses either s or r and finally C does the same, unaware of what A and B
did. This protocol thus has eight terminal histories. The proposition p indicates
whether P is accepted and p holds if at least two agents choose s. Furthermore the
proposition a holds if A chooses s, b if B chooses s and the same for C with c. The
interpretation function is thus π(sss) = {a, b, c, p}, π(ssr) = {a, b, p} . . . π(rrr) =
∅. We assume that s 6∼X s0 if s and s0 differ in the evaluation of the outcome p,
or if the vote of X differs in s from that in s0 .
The following game results hold.
w(kcg(FV , {A, B}, {C}, p)) = 1
w(kcg(FV , {A, B}, {C}, KB c ∨ KB ¬c)) = 1
w(kcg(FV , {B}, {C}, KB c ∨ KB ¬c)) = 0
A and B together can ensure that p is true, by both voting s. They can also vote
differently, so that a and ¬b result. In this case the outcome will solely depend
on C’s choice. They thus learn what C voted. Agent B cannot learn what C did
on its own.
One example, described by Schneier [89, p. 133], is a voting protocol where
B would have the option of copying A’s (encrypted) vote. In that case one might
get
w(kcg(FV0 , {B}, {A, C}, KB a ∨ KB ¬a)) = 1
This is an unwanted property and thus a ‘bug’ in the protocol. It is necessary to
reason about knowledge to express this bug, so a standard game-theoretic analysis
might not have revealed this shortcoming.
N
1 2 3 4
13 14 12 14 12 13
23 24 34 34 24 23
has no clue whatsoever about the days of the week, and replies: ‘I am
not sure. Can I do fifty-fifty?’. The quiz master has to remove two
options that are not the answer, so he says: ‘The answer is not Monday
and neither Friday’. Does the candidate now know the answer?
We thus see that whether the candidate knows the answer depends on Nature
and on the quiz master Q. If Nature uses a deterministic strategy, in which for
instance a1 always holds, then the candidate knows that this is the right answer.
However, if Nature uses the nondeterministic strategy in which each answer could
be the right answer, the candidate will not know the answer.
7.3. Examples 135
N
1 2 3 4
23 34 14 12
The situation becomes more interesting if the quiz master gets involved. In
this game the quiz master has the ability to signal the right answer to the candi-
date. Consider, for example, strategy σ{Q} , defined as follows.
σ{Q} (1) = {23}
σ{Q} (2) = {34}
σ{Q} (3) = {14}
σ{Q} (4) = {12}
This strategy tells the candidate exactly what the right answer is: The answer
directly before the two eliminated options (assuming 4 comes before 1). The
updated model u(FQ , σ{Q} ) is given in figure 7.3. This strategy acts as a code
between the candidate and the quiz master. It is the strategy that proves that
w(kcg(FQ, {Q}, ∅, q)) = 1. A practical conclusion one can draw is that one should
not bet on this quiz if one does not know what the interests of the quiz master
are.
This example also demonstrates why we prefer to assume that strategies are
commonly known. If one would have used the alternative definition kcg 0 , in which
agents do not know what strategies are used, then one can obtain the following
results.
Nature cannot favour the candidate: w(kcg(FQ , {N }, ∅, ψ)) = 0
The quiz master cannot help the candidate: w(kcg(FQ , {Q}, ∅, ψ)) = 0
These results are counter-intuitive, since signaling in games is a phenomenon
that does occur in practice. When proving the security of a protocol, it is a
good principle to make the weakest assumptions possible. At first sight, it seems
that assuming that strategies are not known is the weakest possible assumption.
However, in the case of proving ignorance, first sight can be misleading. It is
harder to prove that the candidate does not know the answer when he or she
knows all strategies that are used, than it is to prove ignorance when he or she
does not know the strategies. Therefore, the weakest and safest assumption is to
assume that he does know the strategies. This shows that it is best to use the
definition of kcg rather than the alternative kcg 0 for these ignorance proofs. This
motivates the choice to make kcg the default and call kcg 0 the alternative.
136 Chapter 7. Knowledge Condition Games
From a pack of seven known cards two players each draw three cards
and a third player gets the remaining card. How can the players with
three cards openly (publicly) inform each other about their cards,
without the third player learning from any of their cards who holds
it?
Following the analysis by Van Ditmarsch [106] we call the agents A, B and C
and the cards 0, 1, 2, 3, 4, 5 and 6. The interesting thing about this problem
is that certain solutions to this problem appear sound, but are not sound. A
solution to this problem is a joint strategy for A and B that prescribes what they
should communicate to each other. We are mostly interested in direct exchanges:
statements by A such that B directly learns all of A’s cards. Agent B can respond
by telling A which card C has. Assume for the moment that the actual deal of
cards is that A holds 0, 1 and 2, that B holds 3, 4 and 5 and that C holds 6. Instead
of reasoning about complete strategies for A and B,we settle for identifying which
statements by A for this situation van can be part of a strategy. Here are some
solution attempts. Imagine that the next public statements are made by agent A
so that all agents can hear it.
I have 012 or 345: This statement is true and when taken literally it does not
tell C anything about a single card. Unfortunately A can imagine that C
holds card 5. in which case this statement would reveal A’s cards to C. So
A cannot make this statement safely.
I have 012 or I have none of these cards: A knows that C cannot pinpoint
any card after learning this statement. Unfortunately C can reason like
this: Suppose A has 345. In that case she cannot exclude that I hold card
2. If I had card 2 I would know that B holds card 0 and 1. Alice would
never allow me to learn that. Contradiction. By this line of reasoning she
can eliminate all possibilities except 012.
I have 012, 034, 056, 135, 146 or 236 This is an example of a statement A
can make.
For a deal abc|def |g, the cards of A are a, b, c, agent B owns d, e, f and C holds
card f . We can thus say that in a situation with deal 012|345|6, the following
formula holds: a0 ∧ a1 ∧ a2 ∧ b3 ∧ b4 ∧ b5 ∧ c6 .
An interpreted game form
The second part cig expresses that C does not know for any card who holds it.
We call this a negative knowledge requirement, or an ignorance requirement.
^
cig = (¬KC ai ∧ ¬KC bi )
i∈D
We can now solve the Russian cards problem by finding a strategy that fulfills,
for a suitable model F , the following question.
0 ∈ σ(abc|def |g) iff abc ∈ {012, 034, 056, 135, 146, 236, 245}
1 ∈ σ(abc|def |g) iff abc ∈ {013, 026, 045, 125, 146, 234, 356}
2 ∈ σ(abc|def |g) iff abc ∈ {014, 025, 036, 123, 156, 246, 345}
3 ∈ σ(abc|def |g) iff abc ∈ {015, 024, 036, 126, 134, 235, 456}
4 ∈ σ(abc|def |g) iff abc ∈ {016, 023, 045, 124, 135, 256, 346}
5 ∈ σ(abc|def |g) iff abc ∈ {012, 035, 046, 136, 145, 234, 256}
5. When using this strategy, A should therefore make a genuine random choice
between the two available actions, for instance using a coin flip.
Other strategies for A are deterministic. One deterministic strategy, that re-
quires at least seven different signals, is the strategy σ2 , described by the following
formula.
σ2 (abc|def |g) = {(a + b + c) mod 7}
The idea is that agent A announces the sum of its cards modula 7. For instance
if A has cards 024 it should use action 6. When C hears that A has chosen action
6, it can deduce that A has cards 024, 015, 123, 256 or 346. In case that C has
card 6, it would know that A has either cards 024, 015 or 123, but does not know
for any specific card that A has it. Thus we know that there are deterministic as
well as nondeterministic strategies for agent A.
In the existing literature it was already proven that the statement “I have
012,034,056,135,146,236 or 245” can be made. In Van Ditmarsch’s paper [106] all
statements that can be used when A holds 012 are given. However Van Ditmarsch
does not present a complete strategy, and indeed it is not trivial to come up with
a set of six statements that cover all possible card combinations of agent A.
Thus knowledge condition games is a suitable framework for searching detailed
strategies for situations such as the Russian Cards problem.
• P = {p}
turn() = A
turn(a) = B
turn(ab) = C
turn(abc) = D
¿From the definition of the equivalence relations one sees that A can see what D
does, B can see what D does, C can see what A does, and D can see what B
and C does. Also, agents can remember their own action, and they can see all
messages that are sent.
In order to come up with a knowledge condition game, we assume that the
three agents B, C and D act as a team. The goal is to make B know what action
C selects. It is not hard to see that the three agents can do this: D can copy
the message of A. Agent B can see this copied signal, and therefore knows what
C has done. In order to make this example more interesting, we add another
requirement: We assume that the coalition of agents does not want A to know
what message C sends. Since agent A can also see what agent D does, the copying
strategy sketched in this paragraph no longer works. The three agents must use
a more complicated coalition strategy.
The knowledge goal described above consists of a positive and a negative part:
agent B must gain some knowledge about C’s action, and agent A must not gain
knowledge about C. This complex goal is described by the following formula φ.
The answer to this question is “yes”. The following strategy σBCD is a successful
strategy in this knowledge condition game.
This strategy is nondeterministic in the first two steps, but deterministic in the
last step. Agent B, who knows its own action, can deduce from D’s action
whether the proposition p holds. Agent A cannot do this, since it does not know
what B has done. It is necessary for B and C that they make a nondeterministic
choice, otherwise A could deduce whether p holds from knowing the strategy that
is used.
• The first theorem is concerned with the problem of deciding whether a coali-
tion Γ can win a knowledge condition game with an empty set of opponents.
This is called the no-opponents knowledge condition game decision prob-
lem. It turns out that this problem is already NP-complete, and thus not
tractable.
• The second theorem states that the general kcg decision problem is even
harder: with opponents the problem is Σ2 P-complete.
For the other theorems we use the alternative version of knowledge condition
games kcg 0 .
• In the third theorem we claim that the no-opponents kcg 0 decision problem
is as hard as the general problem.
• Both problems are NP-complete, which is the fourth theorem.
142 Chapter 7. Knowledge Condition Games
Proof. Assume that F, Γ, φ are given. The empty coalition has only one strategy
σ∅ . This strategy is such that u(F, σ∅ ) = F . Therefore
w(kcg(F, Γ, ∅, φ)) = 1 ⇔ ∃σΓ m(u(F, σΓ )) |= φ
A nondeterministic polynomial algorithm for this problem exists. Find or guess
nondeterministically a strategy σΓ . Since a strategy encodes a subset of actions
available in F , the size of σΓ is smaller than the size of F and thus polynomial
in the input size. Now calculate M = m(u(F, σΓ )), and verify for each state w
of M that M, w |= φ. The number of states in M is at most the number of
terminal histories of F , so kM k ≤ kF k. All of this can be done in polynomial
time. Therefore, this problem can be solved using a nondeterministic polynomial
algorithm and this problem is in NP.
In order to show that the restricted kcg problem of the theorem is as hard
as any NP problem, we show that any instance of the 3SAT problem described
on page V 30 can be transformed into an equivalent restricted kcg instance. Let
φ3 = i (ai ∨ bi ∨ ci ) be a propositional logic formula in conjunctive normal
form with three literals per clause. The literal formulas ai , bi , ci must be either
atomic propositions or negated atomic propositions. We can construct an inter-
preted game form F with a single agent Σ = {A} and a formula φ such that
w(kcg(F, {A}, ∅, φ)) = 1 if and only if ∃S : S |= φ3 .
The model F = ({A}, H, turn, ∼, P, π) is constructed in the following way.
Let P 3 be the set of atomic propositions occurring in φ3 . The new set of atomic
propositions P contains two propositions for any old proposition: P = {x+ |x ∈
P 3 } ∪ {x− |x ∈ P 3 }. For each new proposition a history is created: H = {} ∪
{ep |p ∈ P }. The interpretation function is such that only the corresponding
atomic proposition is true: π(ep ) = {p}. Furthermore turn() = A. Agent A
cannot distinguish any end state: ep ∼A eq for all terminal histories ep and eq .
The formula φ = φ1 ∧ φ2 is a conjunction of two parts. The part φ1 expresses
that for each original atomic proposition p ∈ P 3 , either the positive proposition
p+ is considered possible or the negative p− , but not both:
^
φ1 = (MA p+ ∨ MA p− ) ∧ ¬(MA p+ ∧ MA p− )
p∈P 3
The idea is that the strategy that A uses is actually an assignment of values to
all atomic propositions in P 3 . The condition φ1 expresses that such assignment
must assign either the truth value true (p+ ) or false (p− ) to each proposition p.
7.4. Computational Complexity 143
p+ p− q+ q− r+ r−
Figure 7.4: The model of 3SAT formula ψ
It is not hard to see that any strategy σ{A} such that m(u(F, σ{A} )) |= φ1 ∧ φ2
corresponds to an assignment S such that p ∈ S if and only if p+ ∈ σ{X} (), and
that this assignment satisfies S |= φ3 . Since the formula and model constructed
have sizes that are linear with respect to the size of φ3 , this is a polynomial re-
duction. Therefore, the restricted kcg problem is NP-hard. Since we have also
shown that the problem is in NP, we conclude that the restricted kcg problem is
NP-complete.
ψK = (MA p+ ∨ MA p− ) ∧ ¬(MA p+ ∧ MA p− )∧
(MA q + ∨ MA q − ) ∧ ¬(MA q + ∧ MA q − )∧
(MA r + ∨ MA r − ) ∧ ¬(MA r + ∧ MA r − )∧
MA (p+ ∨ q − ∨ r + ) ∧ MA (q − ∨ p− ∨ r + )
B B B B
p+ r + p+ r − p− r + p− r − q + r + q + r − q − r + q − r −
Figure 7.5: The construction of the Σ2 P proof
¬φB ∨ (φA ∧ f (ψ(~x, ~y)). The part φB expresses that the strategy of B corresponds
to an assignment to ~y. The part φA expresses that the strategy of A corresponds
to a strategy for ~x. Finally, f (ψ(~x, ~y)) is a translation of the input formula ψ(~x, ~y).
^
φB = ((MB yj+ ∨ MB yj− ) ∧ ¬(MB (yj+ ∧ yj− ))
j
^
− −
φA = ((MA x+ +
i ∨ MA xi ) ∧ ¬(MA (xi ∧ xi ))
i
^ ^
f (ψ(~x, ~y)) = f ( (ai ∨ bi ∨ ci )) = (f (ai ) ∨ f (bi ) ∨ f (ci ))
i i
The function f is defined such that f (¬p) = p− and f (p) = p+ . The size
of φ is linear in the size of ψ. Therefore, this is a polynomial reduction. This
completes the proof that the knowledge condition game decision problem is Σ2 P-
hard. Since it is also in Σ2 P, we conclude that the problem is Σ2 P-complete.
The construction of a model F is illustrated in figure 7.5. This is the model that
you would get in the reduction of ψ(~x, ~y) where ~x contains p and q and ~y consists
of r. The model is again relatively small: only two actions happen in each play
of this interpreted game form. The first one is decided by agent A, the second
one by B.
In the two previous proofs, it is essential that the agents are aware of the
strategies they choose. Both constructions would not work with the alternative
definition kcg 0 . One can hope that the computational complexity of the kcg 0
decision problem would be lower. Indeed one can prove that in this case it does
not matter whether there are opponents.
7.4.3. Theorem. Assume that F, Γ, Ξ and φ are given. w(kcg 0 (F, Γ, Ξ, φ)) = 1
iff w(kcg 0 (F, Γ, ∅, φ)) = 1.
Proof. Let G = kcg 0 (F, Γ, Ξ, φ) be a kcg 0 decision problem. Notice that the
goal of coalition Ξ is to choose a strategy σΞ such that U0 (σΓ , σΞ ) = (0, 1), where
U0 is the utility function of the game G. Since U0 is defined using universal
quantification over the set of terminal histories of u(u(G, σΓ ), σΞ ), the best thing
to do for coalition Ξ is to make sure that this set is as large as possible. In order
to achieve this, σΞ should choose the neutral strategy that allows any action: The
strategy σ with σ(h) = A(H, h). Since we have assumed that neutral agents can
do any action, we might as well assume that the agents X ∈ Ξ are neutral, and
determine the value of the game w(kcg 0 (F, Γ, ∅, φ)) = 1.
We see thus that the presence of opponents is not relevant, and indeed in ATEL
no distinction between opponents and neutral agents is made. The question is
146 Chapter 7. Knowledge Condition Games
now whether solving the kcg 0 decision problem is still as hard as the original no-
opponents kcg problem. The answer is yes. The no-opponents kcg 0 problem is
also NP-complete. However, the proof is different in an interesting way.
7.4.4. Theorem. Deciding for given F, Γ and φ whether w(kcg 0 (F, Γ, ∅, φ)) = 1,
is an NP-complete problem.
form with three literals per clause. Let P 3 be the set of atomic propositions
occurring in φ3 . We define an interpreted game form between two agents: an
agent Q that asks questions, and an agent A that answers them. The proponent
coalition is Γ = {A} and Q is assumed to be neutral. Every terminal history is of
the form (p, b, i, x), where p ∈ P 3 , b ∈ {0, 1}, i ∈ {1, 2, . . . , n} and x ∈ {ai , bi , ci }.
The first action p is chosen by agent Q and must be one atomic proposition of φ3 .
The agent A must then reply by giving a boolean value b. This indicates what
truth value A has in mind for p. Then agent Q choses one triplet (ai ∨ bi ∨ ci ) that
appears in φ3 . Agent A then has to choose which of these three parts it thinks
should be true: either ai or bi or ci . The trick however is that ∼A is defined in
such a way that for all histories h and h0 , agent A only knows the length of the
histories: h ∼A h0 iff |h| = |h0 |.
A does not know, when making its final decision, which answer it has given on
its first turn. The agent thus risks giving inconsistent information. For instance
in the history (p, 1, (¬p ∨ q ∨ r), ¬p) agent A first says that p is true, and then
says that it thinks that ¬p holds. The goal of agent A in the game is to avoid
these inconsistent histories. We let P = {e} consist of one proposition and
define for all p ∈ P 3 the interpretation function such that π((p, 1, i, ¬p)) = {e},
π((pj , 0, i, pj )) = {e} and π((p, b, i, x)) = ∅ otherwise. One can now consider the
knowledge condition game G = kcg 0 (F, {A}, ∅, ¬e). Agent A can win the game
G iff there is a satisfying assignment for φ3 .
The proof given above is very similar to a proof given by Schobbens [91] for
the NP-completeness of ATL with imperfect information. This corroborates our
claim that this variant of knowledge condition games is closely related to ATL
and thus to ATEL. The proof exploits the fact that in games where coalitions do
not have perfect recall, it is very difficult for agents and coalitions to coordinate
their own actions.
7.4.5. Theorem. Let F be an interpreted game form with perfect recall, Γ any
coalition of agents and φ an epistemic formula. Deciding whether w(kcg 0 (F, Γ, ∅, φ)) =
1 can be done in polynomial time.
For perfect recall frameworks and the variant kcg 0 the decision problem is thus
tractable. One might wonder whether the same claim can be made for kcg. The
answer is no, because one can modify the NP-completeness proof for kcg in such a
way that it uses a perfect recall interpreted game form. The modification is that
one has two agents, A and A0 , so that A is the agent that chooses a strategy, and
A0 is the agent that cannot distinguish end states and occurs in the knowledge
condition. In general one can always find a perfect recall interpreted game form
that is equivalent for the kcg decision problem by choosing a fresh agent for each
decision node, and use fresh agents in the knowledge condition.
Instead of asking whether there are interpreted game forms F that make
decision problems easy, one can also ask whether there are easy formulas φ. The
answer to this question is yes. To see how this works, we first formulate the
notion of positive formulas and negative formulas formulas.
7.4.6. Definition. For any p ∈ P , the formula p is both positive and negative.
Falsum ⊥ is also both positive and negative. If φ is positive and ψ is negative,
then φ → ψ is negative. Vice versa, if ψ is positive and φ is negative, then φ → ψ
is positive. If φ is positive then KX φ is positive.
Positive and negative formulas are both called monotone formulas, because one
can prove that they preserve truth in the following way. Suppose that M =
(Σ, W, ∼, P, π) and M 0 = (Σ, W 0 , ∼0 , P, π 0 ) are models such that W 0 ⊆ W and ∼0
and π 0 are the restrictions of ∼ and π to W 0 . In this case we say that M 0 is a
submodel of M . Suppose φ+ is a positive formula, and φ− is a negative formula.
Then the following statements can be proven.
M, w |= φ+ implies M 0 , w |= φ+
M 0 , w |= φ− implies M, w |= φ−
The proof of these statements is done by induction over the formula structure.
The interesting step involves the knowledge operator. Suppose that M, w |=
KX φ+ . By definition this means that ∀v ∈ W : w ∼X v =⇒ M, v |= φ+ . Since
W 0 is a subset of W , this means that ∀v ∈ W 0 : w ∼0X v =⇒ M, v |= φ+ . Using
148 Chapter 7. Knowledge Condition Games
Proof. We prove the case where φ is a positive formula. The argument for
negative formulas is similar. Recall that by definition, w(kcg(F, Γ, Ξ, φ)) = 1
iff ∃σΓ ∀σΞ ∀w ∈ W it holds that m(u(u(F, σΓ ), σΞ )), w |= φ where W is the set
of worlds in the model m(u(u(F, σΓ ), σΞ )). Since φ is a positive formula, we
know that m(u(F, σΓ )), w |= φ implies m(u(u(F, σΓ ), σΞ )), w |= φ. The best thing
for coalition Ξ to do is to use a strategy that does not eliminate any action.
They should use a neutral strategy σ 0 such that u(F, σ 0 ) = F . This strategy is
described by σ 0 (h) = A(H, h).
For coalition Γ things are exactly opposite. Suppose that σ 1 and σ 2 are
strategies so that σ 1 is more specific than σ 2 . Formally, this means that ∀h :
σ 1 (h) ⊆ σ 2 (h). The monotonicity of φ implies that m(u(F, σ 2 )), w |= φ implies
m(u(F, σ 1 )), w |= φ. Coalition Γ thus does best be choosing the more specific
strategy σ 1 . For coalition Γ we thus only have to consider the most specific
strategies. These most specific strategies are what one can call pure, because they
select exactly one action at each decision point. A backward induction argument
can be used to show that there are as many pure strategies for F as there are
terminal histories in F . We can try all pure strategies σ p to see if one satisfies
∀w : m(u(F, σ p )), w |= φ. This gives an algorithm that needs time O(kF k2 · kφk).
The first kF k is caused by the fact that we need to consider all pure strategies.
The remaining term kF k · kφk is the time needed to determine whether for all w
it is the case that u(M, σ p ), w |= φ. The decision problem can thus be done in
polynomial time.
For negative formulas the roles of Γ and Ξ are interchanged. For a negative
formula φ, coalition Γ can use the neutral strategy σ 0 . The opponent coalition Ξ
should now try all pure strategies σ p .
The language of ATEL contains temporal operators similar to CTL and know-
ledge operators. The temporal operators are always preceded by an agent oper-
ator.
φ ::= p | φ → φ | ⊥ | hhΓiiψ | KX φ
ψ ::= 2φ | φ U φ
This logic is interpreted over alternating epistemic transition systems. These are
defined as tuples (P, Σ, Q, ∼, π, δ). As usual P is a set of atomic propositions and
Σ a set of agents. The set Q is a set of states the system can be in, and π : Q → P
adds propositions to these states. For any agent X the relation ∼X ⊆ Q × Q is
Q
an equivalence relation, and δ : Q × Σ → 22 assigns to each agent in each state
a set of sets of states. Each agent can choose one set of states, and the next state
of the system will be from that set.
An example would be a system where Q = {0, 1, 2, 3, 4}. Suppose that
δ(0, X) = {{1, 2}, {3, 4}} and δ(0, Y ) = {{1, 3}, {2, 4}}. Agent X can now choose
{1, 2} and Y can choose {2, 4}. They make these choices simultaneously. The
next state of the system will be 2, because that is the only common state in their
chosen sets. It is necessary to put some constraints on δ so that a next state can
always be chosen.
The interpretation of this logic uses the notion of strategy to interpret the
coalition operator hhΓii. A strategy for Γ is any function that makes a choice
σΓ (X, q) ∈ δ(q, X) for any agent X ∈ Γ in any state q ∈ Q. Based on a strategy
σΓ , one can define the set of possible walks W(σΓ ) through Q so that all choices
for agents X ∈ Γ are made as recommended by the strategy. This set of walks is
used in the following interpretation of ATEL.
M, q |= ⊥ never
M, q |= p where p ∈ P iff p ∈ π(v)
M, q |= φ → ψ iff M, q |= φ implies M, q |= ψ
M, q |= KX φ iff ∀(q, q 0 ) ∈∼X : M, q 0 |= φ
M, q |= hhΓiiφ iff ∃σΓ : ∀w = v... ∈ W(σΓ ) : M, w |= φ
A main advantage of ATEL over kcg is that ATEL extends temporal logic, and
can thus be used to express different kinds of goals such as eventually achieving
something, or avoiding some state forever. When this logic was presented it was
reported that the logic has a low model checking complexity [102]. Unfortunately
this only holds if one allows strategies that are not uniform (see definition 3.3.13).
If one demands uniform strategies, model checking becomes NP-complete, even
without using the knowledge operator [91]. Another point of discussion for this
logic is the fact that the existence of a strategy, used in the interpretation of
hhΓiiφ, is a very weak condition. One can come up with situations were hhXiiφ
holds but one would not expect X to achieve φ [54, 55, 109]. Thus, it seems that
the interpretation of this logic still needs some sorting out, and indeed ATEL
currently receives a lot of research attention [3, 87].
Knowledge condition games is a less versatile verification framework than
ATEL, because kcg does not allow complicated temporal reasoning. Only the
special case of knowledge at the outcome stage of the protocol is studied. Know-
ledge condition games also do not allow for concurrent moves. This has the
advantage that knowledge condition games are easier to understand, and that
the complications that arise in the interpretation of ATEL do not arise in the
context of knowledge condition games. An interesting difference between ATEL
and kcg is that in kcg nondeterministic (and hence arguably “richer”) strategies
are used, whereas ATEL uses deterministic strategies.
One can also compare knowledge condition games to variants of dynamic
epistemic logic, described on page 54, since dynamic epistemic logic allows rea-
soning about the effect of actions on the knowledge of agents. Indeed the quiz
master problem is inspired by Van Ditmarsch’ analysis of the Russian Cards
problem [106].
7.6 Conclusion
By combining protocols and knowledge conditions into games, one can express
properties of multi-agent protocols relating to security and secrecy. In a know-
ledge condition game, one can make fine distinctions between for instance neutral
and opponent agents, and one can give examples where this distinction is signif-
icant. Therefore, these games are a promising direction for future research into
the interaction between knowledge and strategies.
The complexity results reported in this chapter draw an interesting picture.
There seems to be a computational cost for assuming that agents know strate-
gies. The single agent decision problem is already intractable. The presence of
opponents makes it even harder to compute whether a coalition can guarantee
a property. If we drop this assumption and reformulate the notion of winning a
knowledge condition game, then the extra complexity of adding opponents dis-
appears. However, the problem without opponents is still NP-complete and thus
7.6. Conclusion 151
intractable, but for different reasons. The complexity proof is no longer based
upon formulating a difficult knowledge formula, but on the hardness of coordi-
nating in an interpreted game form without perfect recall.
Future research could focus on comparing decision problems for knowledge
condition games to other game-theoretic decision problems, in order to establish
what exactly the complexity cost is of considering knowledge goals. It would
also be interesting to find out under which assumptions knowledge condition
games can be solved in polynomial time. Other directions include looking at
knowledge condition games from a logical viewpoint by searching for axioms, and
to consider the mechanism design problem to find an interpreted game form with
given properties.
Chapter 8
Entropy and Privacy
8.1 Introduction
Information is valuable, and thus agents do not always want to give it away. Both
organisations and individuals often want to keep certain information private. At
the same time they might want to act upon it. Does this reveal the information?
In this chapter we study how agents should act if they want to maximize their
utility, while at the same time not giving away too much information. Unlike
the previous chapter, in this chapter we do this based on explicit probabilities.
We define two classes of games in which the utility for each agent does not only
depend on the payoff of the chosen action, but also on the information properties
of the strategy used. These games are called minimal information games and
most normal games and might be applied to the following situations.
153
154 Chapter 8. Entropy and Privacy
compute how one should randomise. A similar argument applies when you
send out an artificial agent to do your shopping. If the agent is sent over
an insecure network, everyone can inspect the source code and thus the
bidding strategy of the agent. You might not want to send an agent that is
exactly optimal for your preferences, in order to hide your preferences.
• Many public places are now monitored by closed circuit television systems.
If you come to one such place regularly, the camera attendants learn a lot
about your habits and thus about you. You feel that this is a breach of your
personal privacy, and decide to hide your habits by changing your behaviour
often, for instance by going to different shops in a different order every time.
This situation can also be modeled as a minimal information game. Again
one can translate this example to the domain of artificial agents and the
Internet.
• Consider now the case of a criminal who wants to steal from a shop guarded
by a closed circuit television system. He wants to look like a regular shopper,
but has different goals. He thus wants to behave so that he can steal the
most, while at the same time appear to be a normal shopper. This can be
modeled as a most normal game.
As the similar setting of the last two examples suggest, minimal information
games and most normal games are related to each other. From these examples
it should also be clear that we assume that the strategies that agents use are
publicly known. This assumption makes our results stronger (if you have privacy
while your strategy is public, you will have even more privacy when you can keep
your strategy secret).
Privacy has received a lot of attention from economists and in legal settings.
Some key sources have been collected on a website [1]. The work in this chapter
differs from these economic papers for two reasons. First of all we only deal with
personal information privacy, whereas the word ‘privacy’ also has other meanings.
The second difference is that these papers try to explain the need for personal
privacy in terms of economic utility. Odlyzko for instance relates privacy and
price discrimination [77]. It is assumed here that privacy is a fundamental value,
that is not instrumental to any gain. Privacy itself is a good cause that can be
enjoyed directly.
Distributed constraint optimization techniques can be used by agents to solve
coordination problems such as scheduling a meeting at the most suitable time
and place. In these applications agents have to reveal information on their pref-
erences for the meeting, but this information is also privacy-sensitive [33, 67].
In this application domain there is also a trade-off between solution quality and
privacy, and this can also be modeled using entropy [33]. Thus, privacy-related
research certainly has practical applications and it would be interesting to study
these further. Therefore, we agree with Maheswaran and others’ [67] ‘call to arms
8.1. Introduction 155
8.2 Example
The following problem serves as an example. Alice (agent 1) needs to buy one
box of breakfast cereals every week. Every week she is faced with the following
choice: whether to buy Allgrain (A), Barley (B) or Cornflakes (C). Alice is not
indifferent to which brand she eats. In fact she likes A better than B and B
better than C, as is indicated by the following matrix of utilities.
action A B C
utility 3.0 2.0 1.0
If Alice is solely interested in maximising her expected utility, she should buy
A every week. However, Alice knows that the shop is watching her shopping
behaviour closely, and she is concerned about her privacy. She decides that the
decision that she makes should be private, and she can achieve this by flipping a
coin and letting her decision depend on this coin flip. This way the shop cannot
predict her decision.
Alice first attempts to use the following random strategy.
action A B C
probability 0.98 0.01 0.01
If Alice uses this strategy, then the shop does not know anything about her
decision: All three actions may occur with positive probability. At the same time
her expected payoff is still very high, because the suboptimal actions occur with a
very low probability. Problem solved, so it seems. But this is not the whole story.
Even though the shop does not gain any knowledge, it does gain information from
this strategy. If the shop learns, from repeated observation, that Alice uses this
strategy, then it is quite certain that she will buy A. The shop has gained quite
a lot of information. Therefore, the indicated strategy is not the right strategy if
one analyses the situation using information theory.
One can argue that no new types of games are needed, because one can capture
Alice’s wish for privacy in the utility function of some modified pure or mixed
strategy game. This is not the case because in these games the utility of strategies
is determined solely by the utility of single actions: The utility function must be
of the form U = Σa p(a)u(a), where p(a) is the probability of action a, and u(a)
the payoff of this individual action. Privacy and uncertainty are not reducible to
certain individual actions, and therefore no suitable pure or mixed strategy game
can be found.
A more sophisticated idea is to model privacy by adding an extra player G
that tries to guess Alice’s actions. In such a game, Alice would gain a high payoff
by randomising her actions, and thus optimal strategies for this game would also
be privacy-preserving strategies. The following payoff matrix gives such a game.
The parameters 1 , 2 , 3 , and δ1 , δ2 , δ3 are all positive.
8.3. Information Theory 157
G\ Alice A B C
A 1 , 3.0 − δ1 0, 2.0 0, 1.0
B 0, 3.0 2 , 2.0 − δ2 0, 1.0
C 0, 3.0 0, 2.0 3 , 1.0 − δ3
This strategic game, in which both agent choose their strategy independently at
the same time, has been designed such that agent G has incentives i to choose the
same action as Alice, while Alice receives penalties δi if G has ‘guessed’ her next
action correctly. This game is thus arguably a good model for a situation in which
A wants privacy. It is however not clear how one should estimate all the variables
that one needs for this larger game. These considerations have convinced us that
it is easier to treat privacy as an independent aspect of an agent’s utility.
For a discrete random variable X we define the entropy E(X), which is measured
in bits, in the following way.
X
E(X) = f (p(X = k), p(X = k))
k
This definition of entropy does not work for continuous random variables. A
different definition for continuous variables also exists [95, p. 35], based on in-
tegration rather than summation. Since this is slightly more complicated and
continuous random variables are not used in this chapter, the details are not
discussed here.
A random variable X with values in the domain {1, 2, . . . , m} can be speci-
fied by giving a vector of length m with the probabilities of each value: (p(X =
158 Chapter 8. Entropy and Privacy
1
entropy
0.9
0.8
0.7
0.6
entropy
0.5
0.4
0.3
0.2
0.1
0
0 0.2 0.4 0.6 0.8 1
probability
1), p(X = 2), . . . , p(X = m)). For a mixed strategy, the numbers {1, 2, . . . , m}
represent the available actions. A requirement for probability measures on stochas-
tic variables is that the probabilities should add up to 1. We can thus only use
vectors x that indeed add up to 1, so it is convenient to define the set of all these
vectors. The set definition of the set Pm from page 40 is repeated here, and we
also define Qm as the set of nonzero vectors.
X
Pm ={x ∈ [0, 1]m | xi = 1}
i
X
m m
Q ={x ∈ (0, 1] | xi = 1}
i
The set Pm contains all vectors of length m that add up to 1, and Qm contains
all vectors that add up to 1 and do not take the value 0. The set Qm is important
in some of the proofs, but often we work with the more general set Pm . We can
apply the notion of entropy to probability vectors x ∈ Pm .
X
E(x) = f (xk , xk )
k
In figure 8.1 the function E((x, 1 − x)) is displayed (here we apply the function
E to a probabilty vector (x, 1 − x) that depends on a variable x ∈ [0, 1]). Thus
the figure shows the entropy of a two-valued random variable (y1 , y2 ) = (x, 1 − x)
, where x is the probability of the first action, and 1 − x the probability of the
second action. As you can see the entropy in the two pure strategies, namely
(1, 0) and 0, 1 is zero. The entropy is maximal if both actions are equally likely,
8.3. Information Theory 159
at (0.5, 0.5). In the context of strategies, a strategy with a higher entropy leaves
observers with more uncertainty, and thus gives the agent that uses that strategy
more privacy. Below we give five examples of entropy. The example strategy
vectors can all be seen as strategies over three basic actions. A strategy (a, b, c)
contains the probability a of selection the first action, b for the second action and
c for the third.
Pure strategies, in which only one action gets a positive probability, have an
entropy of zero bits. The entropy function is bounded. It cannot be negative,
and a vector x of length m can have at most an entropy of lg m. It has this entropy
if all the entries xi are equal to 1/m, thus if the vector represents a stochastic
variable with a uniform distribution.
The second idea that we use from information theory is relative entropy [28].
The function E rel (x, y) can be used to compare two probability vectors x, y ∈ Pn .
The underlying idea is that E rel (x, y) measures how much difference one would
notice if probability vector x is used instead of y for selecting actions. In order
to compute this difference, we add up the differences for each action k. The
probability xk corresponds to the probability that action k is chosen, given that
strategy x is used: xk = P (k|x). Similarly yk = P (k|y). Using Bayes’ law one can
calculate the relative likelihood of strategy x instead of strategy y when observing
that action k is chosen: P (x|k)/P (y|k). Assuming that the a priori probabilities
P (x) and P (y) are equal, one can derive that this is xk /yk .
If x has a higher entropy than x0 , then on average for a random vector y it is the
case that E rel (y, x) < E rel (y, x0 ). It is harder to notice a difference between y and
a high entropy vector x than to notice a difference between y and a low entropy
vector x0 .
The parameter α regulates how much all the agents value the fact that there
is uncertainty over their next action. If we would allow α = 0, then the game
becomes a mixed strategy game: Mi0 (A) = Mx(A). As α approaches infinity, the
actual payoff becomes less and less important. It would have been possible to
choose α differently for each agent, but this would have made the definition less
clear.
As an example, we consider the shopping game from the introduction. This
game has only one agent, that has three options A, B, C with respective payoffs
3, 2, 1. The optimal strategies for the minimal information game with different
values of α is given in the next table. It also lists the utility of s that the agent
would get in the mixed strategy game Mx(A) for the given strategy s and the
utility that the agent would get in the minimal information game Miα (A).
8.4. Minimal Information Games 161
The best payoff that the agent can get is 3.0 by only choosing the first action.
However this would result in no privacy, because if everybody knows that the
agent uses this strategy, then any observer knows beforehand what the agent will
do every week. For a low value of α the utility of s in Miα (A) is very close to
this optimal value of 3. For higher values, the average payoff without entropy
becomes lower. We could call this the cost of privacy. From the table we can
see that if the agent values privacy at one unit per bit (α is expressed in units
per bit) then the agent does best by paying 0.425 in order to obtain 0.775 bits of
privacy.
The question is of course how we can calculate the strategies that maximize
the utility in minimal information games. For the linear functions of the mixed
strategy games this is a solved problem, but for more complicated functions, such
as the utility function of a minimal information game, this can be difficult. In
the next theorem the solution for this optimisation problem is shown.
8.4.2. Theorem. Let Miα (A) be a minimal information game and ~s a strategy
profile. The set bX (~s) is a singleton {b} such that
−1 X
2α Ai (~s)
bi = P α−1 AX (~s)
k2
k
Proof. Let Miα (A) = (Σ, {SX }X∈Σ , U) be a minimal information game. We
have to prove that the set bX (~s) contains one element, and that that element is
described by the given formula. We first show that all points in bX (~s) are interior
points. Then we derive an equation that any best response must satisfy, and show
that this equation has a unique solution, namely the one given in the theorem.
Let n be the number of actions that agent X can choose from. Take any
vector ~x ∈ SX and assume that ~x ∈ Pn \ Qn . We are going to show that
there is a better vector ~y, and thus ~x is not a best response. There is some
i such that xi = 0 and some j such that xj 6= 0. We will show that there
is some such that ~y = [[x−i , ]−j , xj − ] is a better vector: UX ([~s−X , ~y]) >
UX ([~s−X , ~x]). To show this, note that the utility function UX is continuous and
differentiable. Note further that δxδ i UX ([~s−X , ~x]) = +∞ and δxδ j UX ([~s−X , ~x]) <
+∞. Therefore, for sufficiently small , the gain from raising xi outweighs the
potential loss from lowering xj . Therefore, for sufficiently small we have that
UX ([~s−X , ~y]) > UX ([~s−X , ~x]) and thus ~x ∈
/ bX (~s).
Now suppose that b ∈ b (~s). We know that b ∈ Qn . Take i, j ∈ {1, 2, . . . , m}
X
by increasing bi while decreasing bj , and therefore for any optimal point it holds
that δbδ i UX ([~s−X , b]) = δbδj UX ([~s−X , b]). We can use this as a starting point for the
following link of equations. First we compute the derivative δbδ i UX ([~s−X , b]).
δ X
U ([~s−X , b]) =
δbi
δ X
( bj A X s−X , b]) + αE(~b)) =
j ([~
δbi j
δ
AX
i (~
s) + α (E(~b)) =
δbi
AX s) + α(− lg bi − lg e) =
i (~
AX s) − α lg bi − α lg e
i (~
Using this derivative one can reduce the equation given above in the following
way.
δ X δ X
U ([~s−X , b]) = U ([~s−X , b]) ⇔
δbi δbj
AX s) − α lg bi = AX
i (~ s) − α lg bj
j (~ ⇔
AX
i (~
s) − AX
j (~
s) = α lg bi − α lg bj ⇔
AX
i (~
s)
2 bαi
=
2Aj
X (~
s) bαj
8.4.3. Theorem. Every minimal information game Miα (A) has a Nash equilib-
rium.
a point x with f (x) = x [4]. We thus obtain a strategy vector x with f (x) = x,
and thus a point x such that x ∈ b(x). This point is a Nash equilibrium.
This proof is related to Nash’s original proof that Nash equilibria exist in mixed
strategy games by the fact that both theorems can be proven using Brouwer’s
fixed point theorem. The difference however is that the mixed strategy games
have linear payoff functions. Minimal information games do not have linear payoff
functions, so in this proof the fixed point theorem is used in a different way.
The two theorems of this section, theorm 8.4.3 differ in their constructiveness.
Theorem 8.4.2 gives a concrete way to compute optimal responses in minimal
information games. This theorem can therefore be applied immediately. Indeed
we have used the result formula of this theorem to compute the optimal strategies
in the table on page 160. Thus one can immediately apply this theorem in order
to decide how to act, or to predict how others will act, in situations that can
be modelled as minimal information games. Indeed in section 8.7 we apply the
theorem again to find strategies for agents.
Bach or Stravinsky
Theorem 8.4.3 is not immediately applicable, because it does not tell one how one
should find a Nash Equilibrium. It is thus not constructive in a practical sense.
However it is important to know that a Nash equilibrium exists, since this can
be a strong motivation for finding one. In the next example we use the following
bi-matrix A for defining a two-person minimal information game.
2,1 0,0
0,0 1,2
This matrix is often used in a game called Bach or Stravinsky[79, p. 16]. The
story behind these payoffs is that both agents can decide where they want to
go tonight, either to a Bach concert or a Stravinsky concert. Both agents enjoy
each others company, and hence they receive zero payoff if they do not go to the
same concert. The first agent prefers Bach and thus experiences 2 units of value
when both agent choose the first option. The second agent values Bach at 1 and
Stravinsky as 2.
Since we are interested in privacy, we assume that both agents value their
privacy. Hence we define a minimal information game Miα (A), where α = 0.5. As
we have seen in theorem 8.4.2 it is optimal for agents to randomize their behaviour
somehow. Theorem 8.4.3 tells us there is at least one Nash equilibrium. We have
used computer search to find one for the stated value of α.
One can see that in this Nash equilibrium Stravinsky is the most likely outcome.
Both agents choose action 2 most often. However they do not do this with
absolute certainty, in order to leave some uncertainty for observers. The exact
probabilities are different for both agents since they have slightly different payoffs.
The parameter α again determines the trade-off between selecting actions with a
high payoff and acting normal.
8.5.2. Theorem. Let Mnα (A, ~t) be a most normal game and ~s a strategy profile
for this game. The set bX (~s) is a singleton {b} such that
−1 X
tX 2α Ai (~s)
bi = P i X α−1 AX (~s)
k tk 2
k
Proof. Let Mnα (A, ~t) be a most normal game, ~s a strategy profile and X ∈ Σ
an agent. Suppose that b ∈ bX (~s) is the best response for agent X and let i be one
of B’s actions. If ti = 0 and bi 6= 0, then the relative entropy becomes infinite,
and the utility thus infinitely low. This cannot be optimal, thus if b maximizes
the utility, then ti = 0 implies bi = 0. Thus, in this case the optimal point is not
an interior point. It follows that if ti = 1, then for any optimal strategy b we
must have bi = 1.
Consider now the case where ti > 0. We calculate the derivative of the relative
entropy function.
δ rel δ X
E (b, tX ) = −bi (lg tX X
i − lg bi ) = lg bi + lg e − lg ti
δbi δbi i
8.5. Most Normal Games 165
We see that if bi > 0 approaches zero, then this derivative becomes negative
infinity. If bi is sufficiently small, then we would lower the utility UX ([~s−X , b]) by
decreasing bi further. Therefore, for any optimal value of b, it cannot be the case
that ti > 0 and bi = 0.
Since we have shown that ti = 0 implies bi P = 0, it remains for us to find the
m
optimal vector in the space S = {b ∈ [0, 1] | i bi = 1 ∧ (ti = 0 → bi = 0)}.
The previous argument has shown that b is an interior point of this set S. Such
points can only be optimal if δbδ i UX ([~s−X , b]) = δbδj UX ([~s−X , b]) for any pair i, j
with ti , tj > 0. The next computation will show that there is a unique point
satisfying this condition. Since any continuous function on a closed domain must
have a maximum, this point b will maximize agent X’s utility in the normal form
game.
First we calculate the derivative.
δ X
U ([~s−X , b]) =
δbi
δ
AX s) − α E rel (b, tX ) =
i (~
δbi
Ai (~s) − α(lg bi + lg e − lg tX
X
i ) =
AX s) − α lg bi − α lg e + α lg tX
i (~ i
δ δ
Now find the points b where the derivatives δbi
UX and δbj
UX are equal.
δ X δ X
U ([~s−X , b]) = U ([~s−X , b]) ⇔
δbi δbj
AX s) − α lg bi + α lg tX
i (~
X
i = Aj (~ s) − α lg bj + α lg tX
j ⇔
α lg(bi /bj ) − α lg(tX X
i /tj ) = AX
i (~
s) − AX
j (~
s) ⇔
α−1 AX
i (~
s)
bi tX
i 2
= α−1 AX
bj tX
j 2
j (~
s)
−1 AX (~ 1 X α−1 AX
Again we can choose c such that bi = ctX α i s) k (~
s)
P
i 2 and show that c
= k tk 2 .
This leads to the next formula.
−1 X
tX 2α Ai (~s)
bi = P i X α−1 AX (~s)
k tk 2
k
Discussion
One consequence of the theorem is the following observation. If a certain action
i is not considered by normal agents (tX i = 0) then the non-normal agent should
not consider action i either (bi = 0). If one had used a hard, logical approach
one could have reached the same conclusion. In the most extreme case one can
consider the case where normal agents use a pure strategy. In that case the non-
normal agent has to use the same pure strategy. If the non-normal agent values
all actions equally, he also does best by copying the normal strategy. In all other
cases the best strategy for the non-normal agent is different. Apparently the
agent does best by always taking some risk and getting a higher utility.
8.6.2. Theorem. Every mixed strategy game Mx(A) has a minimal information
equilibrium.
of Mx(A).
details.
citizens go to each shop with equal probability. The criminals have other sources
of income, and thus have no need to visit the bank. However the criminals do
not want others to know that they are criminal, so sometimes they do walk to
the bank to keep up appearances, but less often than they go to the shop. How
often they go to the shop depends on their level of paranoia: Normal agents go
less than paranoid agents.
This level demonstrates the influence of the parameter α on the behaviour of
agents. The four different types of agents, from normal to paranoid, have the
same preferences but value privacy differently. Anyone who has solved this level
has experienced that paranoid agents are harder to identify. One can thus protect
ones privacy better by acting more randomly.
The spooks and the crooks have the same preferences. The difference between
those two groups is that the spooks know what the citizens do, whereas the
crooks have no idea what normal is. Therefore, the crooks use a strategy that is
as random as possible, whereas the spooks use a strategy that is as similar as the
citizens as possible. The crooks can be said to be playing a most normal game,
and the spooks a minimal information game.
In the next table one sees the strategies that the agents use in this simulation.
The first column lists the type of an agent. The second lists the value of α that
that agent uses. For each agent type, there is a strategy for a not-so paranoid
agents (α = 1) and for more paranoid agents (α = 1.5). The remaining columns
list the probability that each agent visits a location.
For computing the strategy of agent types citizens and crooks we have used
theorem 8.4.2 to compute the optimal strategies. For the spooks agents we have
used theorem 8.5.2, where the strategy of the non-paranoid citizens has been used
as the normal strategy. One can see in the table that for all three types of agents,
the more paranoid agents choose a strategy with a higher entropy. They act more
random. It is also clear that the spooks use a strategy that is more similar to
the citizens strategy, and hence they are harder to distinguish from the citizens.
For instance the crooks go often to walmart, but the other two types of agents do
not. By determining the frequency of walmart visits, an observer can determine
whether an agent is a crook or not.
In general, animated simulations such as this one can be used to demonstrate
certain phenomena in a more convincing and entertaining way than calculations
can. One can simulate much larger systems than one can solve by analytical
means, and thus simulations can be of more realistic size than examples can. On
the other hand, a proof-by-simulation lacks rigour. One can argue that simula-
tions do not lead to scientific knowledge in a way that proof does.
This simulation has been programmed in Java, a language very suitable for
interactive graphical programs. No specific agent systems library has been used.
The source code is available on request.
8.8 Conclusion
Two new kinds of games have been defined. First of all, minimal information
games, in which agents want to maximize the uncertainty that observers have
over their next move. Secondly, most normal games, in which agents want to
behave as similar as possible to an existing ‘normal’ agent, while maximizing
their payoff. The definitions use the concepts entropy and relative entropy which
are borrowed from information theory. In two theorems it is shown what the
optimal best responses are in these games. These turn out to be unique in each
situation, and to depend continuously on the payoff matrix and the opponent
strategies. From this continuity one can derive that Nash equilibria exist in these
games.
Minimal information games can be used to analyse situations with privacy-
minded agents. If agents attach some value to privacy, the best strategy always
gives them some privacy.
In most normal games, the situation is slightly more complicated. How well
the non-normal agent X can do depends very much on the strategy that normal
agents use. If the normal agents use a pure strategy, then X has no choice but to
adopt the same strategy. The situation however becomes a lot better if the normal
agents are privacy-minded. In this case they choose a high-entropy strategy, and
this leaves the wanting-to-be-normal agent a lot of room to pursue its own agenda.
One can extend the work in these games in several ways. It would be in-
8.8. Conclusion 171
For many people, verification of software sounds like watching paint dry: Appar-
ently necessary, but quite dull compared to the creative process that came before
it, and the creative uses that come after it. The average user of the verified
software hardly learns anything from watching the process: either the program is
fine, or a bug is found and fixed, after which the program is also fine.
This dissertation is intented to convince the reader that verification of multi-
agent protocols is in fact very interesting. First of all because multi-agent pro-
tocols are widely used, sometimes at unexpected places. The debate about the
proposed constitution for the European Union which took place in May 2005, is
essentially a multi-agent protocol problem: what voting procedure should be used
so that every country and person is represented fairly? Often one can capture
requirements such as fairness in different ways, and deciding what is the best way
is not a mere technical matter.
The second reason why multi-agent protocols are so interesting is that rea-
soning about multi-agent systems is complicated and can have surprising results.
In software verification, the state-space explosion problem is often cited as the
biggest obstacle: the systems to be verified often have a huge number of different
states. Multi-agent protocols can have a small number of states, especially when
these protocols have to be explained to and used by humans. On the other hand
the requirements for these protocols can be subtle and difficult to interpret: in
many cases, properties such as fairness can be hard to define and verify. Different
logics based on extensive games have been presented in the previous chapters.
Using three examples, a voting problem, the joint decision problem and the inde-
pendent decision problem, we have shown that more complex logics can be used
to identify subtle differences in protocols. These more expressive logics can have
less favourable computational properties, making verification intractable. Thus,
besides social arguments, there are also technical arguments in favour or against
certain approaches.
An important distinction, that has been borrowed from game theory, is the
173
174 Chapter 9. Conclusion
other group wants to stop the first group from reaching this situation. This situ-
ation that the groups want to reach or avoid is specified using ordinary epistemic
logic. The fact that a well known logic is used makes knowledge condition games
easier to understand, compared to logical languages with new operators. The fact
that knowledge condition games only model the knowledge of the agents in the
final situation is also an advantage: no temporal reasoning is necessary. Research
in temporal logic has shown that reasoning about time is complex in itself, so it
is not wise to make things even more difficult by mixing the aspects of time and
strategies.
The complexity results for knowledge condition games indicate that games
about knowledge can be intractable. They become tractable when monotone for-
mulas are used. The complexity is thus caused by the fact that in epistemic logic,
one can mix knowledge demands (Somebody knows something) and ignorance
demands (Somebody does not know something).
It often makes sense to assume that agents are aware of the strategies that are
used, for instance of strategies that are so often used that they become conven-
tions, or when dealing with security protocols. One can also assume that agents
do not know strategies. This has been defined as kcg 0 . This alternative definition
makes decision problems slightly easier, and is thus a convenient assumption.
In a knowledge condition game where ignorance is demanded, the optimal
strategy is often a random one. The coalition of agents that wants somebody to
be ignorant should choose their actions in a random, unpredictable way. The fact
that making random choices can be optimal has been known to game theorists
before [11], but sometimes surprises people: flipping a coin is not often recom-
mended for important decisions. The chapter on knowledge condition games does
not tell what kind of coin one should use. It does not tell what exact probabilities
one should use to choose between actions, because the logical approach does not
work with explicit probabilities.
In order to be able to say something about those probabilities, chapter 8
introduces minimal information games. In these games agents have two goals:
getting an optimal payoff by choosing the best actions, and randomizing their
behaviour in such a way that an observer is kept ignorant about what the agent
might do in the future. In order to measure ‘ignorance’, information theory is
used. I have computed optimal strategies for these games, and these strategies
give detailed information how one should randomize. The same is done for the
related notion of most normal games. In those games, agents want to behave as
similar to ‘normal’ as possible, but also getting the highest payoff. Thus, in this
chapter the question about what coin one should use is solved.
Comparing those two approaches, one based on logic and one based on infor-
mation theory, one can make two observations. On the one hand one can say that
the logical approach is more general. Using epistemic logic one can express goals
that mix knowledge and ignorance. The games based on information theory only
deal with ignorance. In general one needs a logical approach in order to form
176 Chapter 9. Conclusion
complex goals. On the other hand, a logical approach has the disadvantage that
it is more abstract: important details, such as the exact probabilities, are often
omitted.
9.3 Results
The next table shows the complexity results stated in this dissertation. The
problems in the class PSPACE are definitely not tractable: no efficient algorithms
for these problems exist. The same is probably true, in practical terms, of the
problems in the class Σ2 P: Even though Σ2 P problems are theoretically easier to
solve, all problems in both classes are too hard to be solved in practice. The class
NP contains problems that are also believed to be hard. No efficient algorithms
for these problems are known, but sometimes one can find heuristics for those
problems. The problems in the final class, P, are called tractable. They can be
solved in reasonable time.
number class members
1 PSPACE efl model checking with linear representation
2 efln model checking
3 Σ2 P kcg decision problem with opponents
4 NP kcg without opponents
5 kcg 0
6 P eflmodel checking
7 efls model checking
8 kcg for monotone formulas
It is clear that analysing games is a complex affair: many of these problems are
intractable. The intractability has different causes. Sometimes, in cases 3 and
4 for instance, the presence of opponents can make a problem much harder. In
other cases, namely 1 and 2, the situation with one agent is already complex.
This is a bit surprising.
In the chapter on logic it has been explained that theorem proving and model
checking are both important techniques for multi-agent protocol verification. In
this dissertation the following complete proof systems are presented.
The first result, that there is a complete proof system for efl, supports the hope
that logical mechanism design is possible. The completeness proof sketches an
9.3. Results 177
[4] M. Aigner and G. Ziegler. Proofs from the Book. Springer-Verlag: Berlin,
Germany, 1999.
[8] A. Baltag. A logic for suspicious players: Epistemic actions and belief-
updates in games. Bulletin of Economic Research, 54:1–45, 2002.
[9] A. Baltag, L.S. Moss, and S. Solecki. The logic of public announcements,
common knowledge and private suspicions. Originally presented at TARK
98, accepted for publication in Annals of Pure and Applied Logic, 2002.
179
180 Bibliography
[10] M. Benerecetti and A. Cimatti. Symbolic model checking for multi agent
systems. In Proceedings of the ICLP’01 workshop on Computational Logic
in Multi-Agent Systems, 2001.
[11] K. Binmore. Fun and Games: A Text on Game Theory. D. C. Heath and
Company: Lexington, MA, 1992.
[12] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge
University Press: Cambridge, England, 2001.
[13] P. Blackburn and W. Meyer-Viol. Linguistics, logic, and finite trees. Logic
Journal of the IGPL, pages 3–29, 1994.
[14] G. Bonanno. Branching time, perfect information games and backward
induction. Games and Economic Behavior, 36:57–73, 2001.
[15] G. Bonanno. Memory implies von neumann-morgenstern games. Knowledge
Rationality and Action, to appear, 2004.
[16] G. Boolos. The Logic of Provability. Cambridge University Press, 1993.
[17] S. Brahms and D. Taylor. Fair division: from cake cutting to dispute reso-
lution. Cambridge University Press, 1996.
[18] F. Brandt and T. Sandholm. (Im)possibility of unconditionally privacy-
preserving auctions. In Proceedings of the International Joint Conference
on Autonomous Agents and Multi-Agent Systems (AAMAS), pages 810–
817, New York, 2004.
[19] D. Chaum. The dining cryptographers problem: Unconditional sender and
recipient untraceability. Journal of Cryptology, 1:65–75, 1988.
[20] R. Chisholm and E. Rosa. On the logic of intrinsically better. American
Philosophical Quarterly, 3:244–249, 1966.
[21] M. Chwe. Rational Ritual: Culture, Coordination and Common Knowledge.
Princeton University Press: Princeton, NJ, 2001.
[22] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT
Press: Cambridge, MA, 2000.
[23] E.M. Clarke and E.A. Emerson. Design and synthesis of synchronisation
skeletons using branching time temporal logic. Lecture Notes in Computer
Science, 131:52–71, 1981.
[24] V. Conitzer and T. Sandholm. Complexity of manipulating elections with
few candidates. In Proceedings of the 18th National Conference on Artificial
Intelligence (AAAI-02), pages 262–273, 2002.
Bibliography 181
[26] S. Cook. The P versus NP problem. Manuscript prepared for the Clay
Mathematics Institute for the Millennium Prize Problems, 2000.
[28] T. Cover and J. Thomas. Elements of Information Theory. John Wiley &
Sons, New York, 1991.
[31] F. Dechesne. Game, set, maths: formal investigations into logic with im-
perfect information. PhD thesis, Tilburg University and Technische Uni-
versiteit Eindhoven, 2005.
[35] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide
to the Theory of NP-completeness. W. H. Freeman and Company, San
Francisco, 1979.
[43] J. Halpern. Reasoning about uncertainty. The MIT Press: Cambridge, MA,
2003.
[45] B. Harrenstein, W. van der Hoek, J.-J. Ch. Meyer, and C. Witteveen. A
modal characterization of Nash equilibrium. Fundamenta Informaticae,
57(2–4):281–321, 2003.
[48] J. Hintikka. Knowledge and Belief: an introduction to the logic of the two
notions. Cornell University Press: Ithaca, NY, 1962.
[51] G. Holzmann. The model checker Spin. IEEE Trans. on Software Engi-
neering, 23:279–295, May 1997.
[52] Z. Huang. Logics for Agents with Bounded Rationality. PhD thesis, Uni-
versity of Amsterdam, 1994. ILLC Dissertation Series 1994-10.
[53] M. Huth and M. Ryan. Logic in Computer Science: Modelling and reasoning
about systems. Cambridge University Press: Cambridge, England, 2000.
Bibliography 183
[68] J. Maynard Smith. Evolution and the theory of games. Cambridge Univer-
sity Press: Cambridge, England, 1982.
[69] K. McMillan. Symbolic Model Checking. PhD thesis, Carnegie Mellon Uni-
versity, 1992.
[71] J.-J. Ch. Meyer and W. van der Hoek. Epistemic Logic for AI and Computer
Science. Cambridge University Press: Cambridge, England, 1995.
[76] A. Ockenfels and A. Roth. The timing of bids in internet auctions: Market
design, bidder behavior, and artificial agents. Artificial Intelligence Maga-
zine, 2005.
[78] O. Ore. Cardano, the gambling scholar. Princeton University Press: Prince-
ton, NJ, 1953.
[100] D. van Dalen. Variants of rescher’s semantics for preference logic and some
completeness theorems. Studia Logica, 33:163–181, 1974.
[101] W. van der Hoek and M. Wooldridge. Model checking knowledge and time.
In D. Bos̆nac̆ki and S. Leue, editors, Model Checking Software, Proceedings
of SPIN 2002 (LNCS Volume 2318), pages 95–111. Springer-Verlag: Berlin,
Germany, 2002.
[102] W. van der Hoek and M. Wooldridge. Tractable multiagent planning for
epistemic goals. In Proceedings of the First International Joint Conference
on Autonomous Agents and Multiagent Systems (AAMAS-2002), pages
1167–1174, Bologna, Italy, 2002.
[103] W. van der Hoek and M. Wooldridge. Cooperation, knowledge, and time:
Alternating-time temporal epistemic logic and its applications. Studia Log-
ica, 75(4):125–157, 2003.
[104] R. van der Meyden and K. Su. Symbolic model checking the knowledge of
the dining cryptographers. under review, 2004.
[106] H. P. van Ditmarsch. The russian cards problem. Studia Logica, 75(4):31–
62, 2003.
[107] S. van Otterloo. Reasoning about extensive games. ESSLLI student session,
2005.
[108] S. van Otterloo. The value of privacy: optimal strategies for privacy minded
agents. In Proceedings of the International Joint Conference on Autonomous
Agents and Multi-Agent Systems (AAMAS), Utrecht, July 2005.
[110] S. van Otterloo, W. van der Hoek, and M. Wooldridge. Knowledge condition
games. In S. Parsons and P. Gmytrasiewicz, editors, Sixth Workshop on
Game Theoretic and Decision Theoretic Agents, New York, 2004.
Bibliography 187
[111] S. van Otterloo, W. van der Hoek, and M. Wooldridge. Knowledge con-
dition games. In S. van Otterloo, P. McBurney, W. van der Hoek, and
M. Wooldridge, editors, Proceedings of the first Knowledge and Games
Workshop. University of Liverpool, 2004.
[112] S. van Otterloo, W. van der Hoek, and M. Wooldridge. Model checking
a knowledge exchange scenario. Applied Artificial Intelligence, 18:937–952,
2004.
[113] S. van Otterloo, W. van der Hoek, and M. Wooldridge. Preferences in game
logics. In Proceedings of the International Joint Conference on Autonomous
Agents and Multi-Agent Systems (AAMAS), New York, July 2004.
[114] S. van Otterloo, W. van der Hoek, and M. Wooldridge. Knowledge condition
games. Journal of Logic, Language and Information (to appear), 2006.
[119] G. von Wright. The logic of preference. Edinburgh University Press, Edin-
burgh, 1963.
[120] J. Weibull. Evolutionary Game Theory. The MIT Press: Cambridge, MA,
1995.
[123] T. Williamson. Knowledge and its limits. Oxford University Press, 2000.
189
190 Index
valid formulas, 9
validities, 9
weakly playable, 51
win-loss games, 41
Zermelo’s algorithm, 36
zero-sum game, 41
List of Symbols
193
194 Index
Multi-agent protocollen zijn collecties van regels die aangeven hoe meerdere par-
tijen met elkaar in contact kunnen treden. Een veiling bijvoorbeeld heeft strikte
regels die aangeven hoe er geboden kan worden. Ook de mogelijke zetten van
een schaakpartij zijn vastgelegd in een collectie regels, en vormen dus een multi-
agent protocol. Tenslotte zijn ook verkiezingen een voorbeeld van een multi-agent
protocol. Deze activiteiten hebben gemeen dat ze in het echte leven, zonder on-
dersteuning van computers gedaan kunnen worden. Men kan zich echter ook
voorstellen dat computerprogramma’s meedoen aan veilingen en verkiezingen,
misschien zelfs met of tegen menselijke spelers. Aangezien computerprogramma’s
nog niet zo intelligent zijn als wetenschappers soms wensen, is het vaak van be-
lang dat protocollen aan bepaalde veiligsheidseisen voldoen. Men wil dus kunnen
nagaan aan welke eigenschappen een protocol voldoet.
Het doel van mijn onderzoek is om methodes te ontwikkelen waarmee men
multi-agent protocollen kan vergelijken en analyseren. Om dit te kunnen doen
moet men een onderscheid maken tussen verschillende klassen protocollen, en ook
verschillende soorten eigenschappen onderscheiden. Protocollen waarin iedere
‘speler’ geheel op de hoogte is van de huidige toestand (schaak bijvoorbeeld) wor-
den behandeld in het eerste deel van dit proefschrift. Voor deze protocollen geldt
dat de eigenschappen die te beschrijven zijn in de logische taal van hoofdstuk 4,
efficient door een computer te verifiëren zijn. Ook kan men formeel redeneren over
deze eigenschappen. Echter, ook voor deze relatief eenvoudige protocollen zijn er
eigenschappen, die uitgedrukt kunnen worden in logische talen uit hoofdstuk 5,
waarvoor automatische verificatie erg complex is. Over sommige ingewikkeldere
eigenschappen kan men echter wel formeel redeneren met het bewijssysteem uit
hoofdstuk 6.
Er zijn ook veel protocollen waarin niet alle spelers van alle details van de
situatie op de hoogte zijn. Denk bijvoorbeeld aan spelen zoals Stratego of Poker.
In deze protocollen is informatie over de huidige situatie, en kennis over wat
andere spelers weten een belangrijke factor. In hoofdstuk 7 worden situaties
197
198 Samenvatting
behandeld waarin het doel van bepaalde spelers is om bepaalde kennis juist wel
of juist niet te hebben. De complexiteit van het analyseren van dit soort situaties
kan hoog zijn, afhankelijk van welke aannames men maakt.
In al deze eerste hoofdstukken wordt kennis als een kwalitatieve eigenschap be-
handeld: als iets wat men wel of niet heeft. In het laatste hoodstuk gebruiken we
kwantitatieve methoden uit de informatie-theorie, om de hoeveelheid informatie
is bepaalde situaties te minimaliseren. Er worden spelen gedefinieerd waarin het
de bedoeling van bepaalde spelers is om zo weinig mogelijk informatie bloot te
geven, en voor deze spelers worden de optimale strategieën berekend. Een mo-
gelijke toepassing van dit onderzoek ligt in de bescherming van privacy tegen
privacy-schendende technologie.
Abstract
The research goal behind this dissertation is to develop ways to compare and anal-
yse multi-agent protocols. In order to do so one has to distinguish different types
of protocols, and one has to distinguish different classes of properties. Protocols
that can be modelled as imperfect information game forms are therefore discussed
in the first part of this dissertation, whereas protocols that can be modeled as
imperfect information are the subject of the second part. In both parts we define
concepts that help us to analyse and understand protocols, demonstrate these
concepts on example protocols, and investigate the computational properties of
these concepts.
In chapter 4, a logic for reasoning about what coalitions can achieve in proto-
cols is presented. For this logic, a complete proof system is given, and the model
checking complexity is determined.
In chapter 5, logics for reasoning about more complicated properties are pre-
sented. Specifically we compare the model checking complexity of logics for rea-
soning about side-effects and nested abilities.
In chapter 6, protocols are analysed using logics that deal with preferences
explicitly. For two different variants of preference logics we give completeness
proofs, and as an example, a characterisation of backward induction is given.
Protocols with imperfect information are the topic of the second part of this
dissertation. In these protocols the knowledge that agents have plays a leading
role. One can look at knowledge in a qualitative way, using epistemic logic, and
this is done in chapter 7. In this chapter, it is shown how the computational
complexity of protocol verification, depends on the presence of opponents, on
whether strategies are known, and on the monotonic nature of the knowledge
requirements. In chapter 8, it is shown that one can also model knowledge in a
quantitative way. Using this approach, we compute optimal strategies for privacy
preservation.
199
Curriculum Vitae
Sieuwert van Otterloo was born on 20 Maart 1979 in IJsselstein (Utrecht, the
Netherlands). He graduated from the Christelijk Gymnasium in Utrecht in 1997,
and went on to study at the Universiteit Utrecht. In 2001 he received the title
of Doctorandus (Master of Science) in Mathematics Cum Laude, and the year
after he also became Doctorandus (Master of Science) in Cognitive Artificial
Intelligence.
In 2002 Sieuwert van Otterloo joined the Department of Computer Science
at the University of Liverpool, where he worked as a PhD scholar. In the final
year he also was a visiting researcher at the Institute for Logic, Language and
Computation of the University of Amsterdam. He successfully defended this PhD
dissertation in Liverpool in November 2005. At the same time he made a next
step in his career, by joining McKinsey&Company in Amsterdam as a business
consultant.
201
Titles in the ILLC Dissertation Series: