Computational Aspects of Game Theory (CAGT)

Prof. Bruno Codenotti
Consiglio Nazionale delle Ricerche, Pisa (Italy)

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:

  1. Non-cooperative games in normal form
    1. Two-player constant-sum games
    2. Two-player variable-sum games
    3. Multi-player games
    4. Existence of Nash equilibria
  2. Cooperative Games
    1. Cooperative three-player games
    2. Bargaining
    3. Cooperative multi-player games
    4. Coalitions
    5. Equilibria in a cooperative environment (core, kernel, nucleolus, Shapley value)
  3. Markets
    1. Simple market models
    2. Arrow-Debreu model
    3. Walras equilibrium (definition, existence results)
    4. Markets and games: comparison and reductions
  4. Classical Algorithms
    1. Preliminaries: Sperner’s lemma
    2. Scarf’s algorithm
    3. Lemke-Howson’s algorithm
    4. Variations and extensions
  5. Recent Algorithms and Applications
    1. Selection of recent algorithms (chosen based on the students’ interests and inclinations)
    2. Selfish routing: Nash equilibria vs optimal solution
    3. Resource sharing: fairness criteria
    4. Mechanism design and Internet protocols

Prerequisites: Basic background in algorithms and mathematics.

Trust in Anonymity Networks (TAN)

Prof. Vladimiro Sassone
University of Southampton (United Kingdom)

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:

  1. Part I (6 hours)
    1. Web anonymity
    2. The Crowds protocol
    3. Onion routing
    4. Anonymity and Information Theory
    5. Protocol vulnerability
    6. Attackers belief and knowledge in Crowds
  2. Part II (4 hours)
    1. The notion of computational trust
    2. Probabilist trust and the Bayesian method
    3. Dynamic trust and reputation models
  3. Part III (5 hours)
    1. The impact of trust on Crowds
    2. Trust in anonymity networks
    3. Adaptive attackers in anonymity protocols
    4. 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 Lenzerini
La Sapienza University, Rome (Italy)

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 Delzanno
University of Genova (Italy)

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:

  1. Finite-state Model Checking
    1. Models and properties (3hours)
      1. Introduction and tools (SPIN/nuSMV)
      2. Models: Finite-state machines
      3. Properties: Linear and Branching Time Temporal Logic
      4. Expressiveness of the specification languages
    2. Decision problems and algorithms (6hours)
      1. Satisfiability, Validity and Model Checking
      2. Decision procedures for Linear and Branching Time
      3. Efficient data structures and algorithms
  2. Infinite-state Model Checking (6hours)
    1. Infinite-state Models
      1. Systems with unbounded control structure: Pushdown systems
      2. Asynchronous Communication: Lossy FIFO channel systems
      3. Real-time constraints: Timed automata
      4. Parameterized Systems: Automata with global conditions
    2. Decidability results and verification algorithms
    3. Examples of tools

Prerequisites: Basics of logic and algorithms.

More information are available at the course site.