KeywordsFormal methods Complex computer systems synthesis of equilibria multiplayer games played on graphs qualitative/quantitative objectives
The team of Véronique Bruyère has research activities in the field of formal methods, and more particularly in verification and synthesis of reliable computer systems, by means of algorithmic game theory. During the last years, important progress has been made concerning complex systems where several agents interact while trying to reach their own objective. As an example we can think of several users behind their computers on a shared network. Such systems are modelled by graphs the vertices of which are the configurations of the system and the edges of which are the possible actions of the different agents. The interaction between the agents is modeled as a multiplayer game played on the graph where each agent/player tries to maintain a coherent behavior with respect to the objective he wants to acheive. One important question is how to conceive adequate playing strategies for all the agents by taking into account their own objective and the interaction between them. The notion of Nash equilibrium is a celebrated solution concept which has its limitations in the case of games played on graphs. Other more adequate solution concepts have been studied like the subgame perfect equilibria or the more recent secure equilibria. Nevertheless, on one hand, it is necessary to propose and study new solution concepts that are the more appropriate possible for complex systems. On the other hand, for know equilibrium notions, it is necessary to deepen the study about their existence, construction, implementation and structure for qualitative objectives (like avoiding a deadlock) or quantitative objectives (like minimizing the power consumption).