Titre de la dissertation: « On Pareto-Optimality for Verification and Synthesis in Games Played on Graphs ».

 Promoteur: Madame Véronique BRUYERE et co-promoteur:  Monsieur Jean-François RASKIN

Résumé de la dissertation:Two-player zero-sum games played on graphs are a mathematical model from the field of game theory used to formalize several important problems in computer science, such as formal verification and reactive system synthesis. In the former problem, a model of a system and of the environment with which it interacts is provided, along with a specification (which is a specific property pertaining to the system). The goal of formal verification is to ensure that the system is correct, i.e., that it enforces the specification, whatever the behavior of the environment. In the later problem, a model of the possible interactions with the environment is provided, and the goal is to synthesize a system which enforces the specification and is thus correct by construction. The classical approach to these problems is to use games played on a graph, which embeds the possible interactions between the players, who themselves represent the system and the (uncontrollable) environment in which it operates. In this classical setting, the objectives of the two players are opposite, that is, the environment is adversarial and its aim is to make the system fail. Modeling the environment as fully adversarial is usually a bold abstraction of reality as it can be composed of one or several components, each of them having their own objective. Our work aims at alleviating these assumptions by providing a novel class of games, called Stackelberg-Pareto games, based on the framework of Stackelberg game, a richer non-zero-sum setting. In this setting, Player 0 (the system) called leader announces his strategy and then Player 1 (the environment) called follower plays rationally by using a strategy that is an optimal response to the leader’s strategy. This framework captures the fact that in practical applications, a strategy for interacting with the environment is committed before the interaction actually happens. The goal of the leader is to announce a strategy that guarantees him a payoff at least equal to some given threshold. In the specific case of Boolean objectives, the leader wants to see his objective being satisfied. Our work proposes a novel and natural alternative in which the single follower, modeling the environment, has several objectives that he wants to satisfy. After responding to the leader with his own strategy, Player 1 receives a vector of Booleans which is his payoff in the corresponding outcome. Rationality of Player 1 is encoded by the fact that he only responds in such a way to receive Pareto-optimal payoffs, given the strategy announced by the leader. This setting encompasses scenarios where, for instance, several components can collaborate and agree on trade-offs. We study in this thesis the problems of verification and synthesis in this context where the goal is to verify that a system is correct with regard to the specification (or to synthesize such a correct system), not in all the executions of the environment, but only in those executions that are rational with regard to the objectives of the environment. We solve these two problems, called Pareto-rational verification and Stackelberg-Pareto synthesis, for different kinds of objectives and characterize their exact complexities.