Tutorials

Véronique Bruyère is Full Professor at the Computer Science Department of the Faculty of Sciences of the University of Mons (UMONS) in Belgium. She is responsable for the Theoretical Computer Science team, and teaches courses in data structures, algorithms, compilers, calculability and complexity. She is interested in computer aided verification and synthesis, and in particular game theory and its application to verification and synthesis, verification and control of timed and hybrid systems, as well as automata theory, combinatorics on words, variable-length codes, and extremal graph theory.

The tutorial. Reactive computer systems (like power plants, plane navigation systems, ABS systems, ...) bear inherent complexity due to continuous interactions with the environment in which they evolve. Formal techniques using mathematical models have been advocated to help to their systematic design. A challenging goal is the automatic synthesis of a correct system from a given specification, that is, a system that enforces this specification no matter how the environment behaves. The mathematical framework used for the synthesis problem is game theory and in particular infinite two-player games played on graphs where the two players are the system and the environment, the vertices of the graph model their possible states, and the edges model their possible interactions. Synthesizing a correct system then means constructing a winning strategy of the system such that, whatever the strategy of the environment, the outcome of the play satisfies the specification. The fundamental algorithmic questions are therefore: Can we decide whether a player has a winning strategy? Can we construct such a strategy, and if possible a simple one? What are the complexities of these problems? In the first part of the tutorial, we will present classical answers to these questions in the case of qualitative specifications like reachability objectives, Büchi objectives, … . We will also present well-known results about games played on weighted graphs with quantitative objectives, in a way to treat specifications like never dropping out of fuel, ensuring a suitable mean response time, … . In the second part of this tutorial, instead of the simple situation of a system embedded in a hostile environment, we will consider more complex situations with systems/environments formed of several components each of them with their own objectives. In this context, we use the model of multi-player games played on graphs: the components are the different players, each of them aiming at satisfying his objective, without being necessarily opposed to the other players. The notion of winning strategy has to be replaced by adapted solution concepts, called equilibria, that are good for each player with respect to his objective. We will present some different kinds of equilibria among which the famous notion of Nash equilibrium.