Computational Aspects of Game Theory (CAGT)
Prof. Bruno CodenottiConsiglio Nazionale delle Ricerche, Pisa (Italy)
Summary:
The widespread use of Internet has promoted tighter
interactions between Computer Science and Game Theory. Game
Theory techniques are being increasingly used to analyze
scenarios featuring users with potentially conflicting
interests. In such environments, a fundamental notion is
the one of equilibrium. The main purpose of this course is
to analyze different notions of equilibrium under suitable
models (non-cooperative games, cooperative games, and
markets). Specifically, we will discuss the computation of
such equilibria and their applications to relevant case
studies (e.g., routing, resource sharing, pricing of shared
resources, etc.). Topics:
- Non-cooperative games in normal form
- Two-player constant-sum games
- Two-player variable-sum games
- Multi-player games
- Existence of Nash equilibria
- Cooperative Games
- Cooperative three-player games
- Bargaining
- Cooperative multi-player games
- Coalitions
- Equilibria in a cooperative environment (core, kernel, nucleolus, Shapley value)
- Markets
- Simple market models
- Arrow-Debreu model
- Walras equilibrium (definition, existence results)
- Markets and games: comparison and reductions
- Classical Algorithms
- Preliminaries: Sperner’s lemma
- Scarf’s algorithm
- Lemke-Howson’s algorithm
- Variations and extensions
- Recent Algorithms and Applications
- Selection of recent algorithms (chosen based on the students’ interests and inclinations)
- Selfish routing: Nash equilibria vs optimal solution
- Resource sharing: fairness criteria
- Mechanism design and Internet protocols
Prerequisites: Basic background in algorithms and mathematics.
Trust in Anonymity Networks (TAN)
Prof. Vladimiro SassoneUniversity of Southampton (United Kingdom)
Summary:
Anonymity is a security property of paramount importance,
as we move steadily towards a `wired,' online community.
Its import touches upon subjects as different as
eGovernance, eBusiness and eLeisure, as well as personal
freedom of speech in authoritarian societies. Trust metrics
are used in anonymity networks to support and enhance
reliability in the absence of verifiable identities, and a
variety of security attacks currently focus on degrading a
user’s trustworthiness in the eyes of the other users.
The course will introduce to the fundamentals of both anonymity and trust, and then move to analyse their interplay. The first part will focus on the protocol Crowds and Onion Routing. We shall discuss what it means for a protocol to guarantee anonymity, and study the most prominent proposals in the literature. The second part will introduce and contrast the notions of credential-based and predictive models, and then present some recent results on the open research issue of dynamic trust models. The final part of the course will bring together these two strands, and focus on current research in the field, in particular on a game theoretic model of cooperation incentives and its validation through experimental results. Topics:
- Part I (6 hours)
- Web anonymity
- The Crowds protocol
- Onion routing
- Anonymity and Information Theory
- Protocol vulnerability
- Attackers belief and knowledge in Crowds
- Part II (4 hours)
- The notion of computational trust
- Probabilist trust and the Bayesian method
- Dynamic trust and reputation models
- Part III (5 hours)
- The impact of trust on Crowds
- Trust in anonymity networks
- Adaptive attackers in anonymity protocols
- Incentives to cooperation in anonymity networks
Prerequisites: There are really no strong prerequisites; an acquaintance with the following notions may nevertheless prove useful: Fundamental notions of probability theory (discrete distributions, random variables, expectations, variance, ... nothing too advanced); discrete markov chains (definition and basic properties); information theory (only notions of entropy, channels, capacity); game theory (only basic equilibrium properties); cryptographic primitives (differences between symmetric and public key cryptography).
More information and reading material are available at the course site.
Information Integration (II)
Prof. Maurizio LenzeriniLa Sapienza University, Rome (Italy)
Summary:
Information integration is the problem of combining data
residing at different sources, and providing the user with
a unified view of these data. The problem of designing
information integration systems is important in current
real world applications, and is characterized by a number
of issues that are interesting from both a theoretical and
a practical point of view. In the last years, there has
been a huge amount of research work on data integration,
and a precise, clear picture of a systematic approach to
such problem is now available. We will present an overview
of the research work carried out in the area of data
integration, with emphasis on the theoretical results that
are relevant for the development of information integration
solutions. Special attention will be devoted to the
following aspects: architectures for information
integration, modeling an information integration
application, ontology-based data access, processing queries
in information integration, data exchange.
Prerequisites: Basic knowledge about Databases (in particular, relational databases) and basic knowledge about Logic.
Model Checking: From Finite-state to Infinite-state Systems (MCFIS)
Prof. Giorgio DelzannoUniversity of Genova (Italy)
Summary:
Model checking is an automated verification method for
checking temporal properties of finite-state models of
(concurrent) systems. Model checking has been successfully
applied to validate hardware designs and communication
protocols. Domain-specific abstractions are necessary in
order to model a complex system as the (synchronous or
asynchronous) composition of a finite collection of state
machines. To reduce the loss of precision of finite-state
abstractions, several efforts have been spent to extend the
theoretical foundations and the verification tools in order
to deal with systems with an infinite-state space. The
extensions considered in the literature range from program
skeletons with recursive calls to processes communicating
via FIFO channels. Techniques like forward/backward
reachability analysis are often the core of decision
procedures for verification of the resulting models. In the
first part of th course we introduce the basic notions
underlying finite-state model checking. In the second part
we present some of the main results obtained in the field
of infinite-state verification (unbounded control
structure, unbounded channels, time conditions, and
parameterized definition). Topics:
- Finite-state Model Checking
- Models and properties (3hours)
- Introduction and tools (SPIN/nuSMV)
- Models: Finite-state machines
- Properties: Linear and Branching Time Temporal Logic
- Expressiveness of the specification languages
- Decision problems and algorithms (6hours)
- Satisfiability, Validity and Model Checking
- Decision procedures for Linear and Branching Time
- Efficient data structures and algorithms
- Models and properties (3hours)
- Infinite-state Model Checking (6hours)
- Infinite-state Models
- Systems with unbounded control structure: Pushdown systems
- Asynchronous Communication: Lossy FIFO channel systems
- Real-time constraints: Timed automata
- Parameterized Systems: Automata with global conditions
- Decidability results and verification algorithms
- Examples of tools
- Infinite-state Models
Prerequisites: Basics of logic and algorithms.
More information are available at the course site.