Today, as computer systems are ubiquitous in our everyday life, there is no need to argue that their correctness is of capital importance. In order to prove (in a mathematical sense) that a given system satisfies a given property, formal methods have been introduced. They include concepts such as model checking and synthesis. Roughly speaking, when considering synthesis, we aim at building a model of the system which is correct by construction. In order to do so, models are mainly borrowed from game theory. During the last decades, there has been a shift from two-player qualitative zero-sum games (used to model antagonistic interactions between a system and its environment) to multiplayer quantitative games (used to model complex systems composed of several agents whose objectives are not necessarily antagonistic). In the latter setting, the solution concepts of interest include numerous equilibria, such as Nash equilibrium (NE) and subgame perfect equilibrium (SPE). While the existence of equilibria is widely studied, it is also well known that several equilibria may coexist in the same game. Nevertheless, some equilibria are more relevant than others. For example, if we consider a game in which each player aims at satisfying a given qualitative objective, it is possible to have both an equilibrium in which no player satisfies his objective and another one in which each player satisfies it. In this case one prefers the latter equilibrium which is more relevant.In this thesis, we focus on multiplayer turn-based games played on graphs either with qualitative or quantitative objectives. Our contributions are twofold: (i) we provide equilibria characterizations and (ii) we use these characterizations to solve decision problems related to the existence of relevant equilibria; and characterize their complexities. Firstly, we provide a characterization of a weaker notion of SPE (weak SPE) in multiplayer games with omega-regular objectives based on the payoff profiles which are realizable by a weak SPE. We then adopt another point of view by characterizing the outcomes of equilibria instead of their payoff profiles. In particular we focus on weak SPE outcome characterization. As for some kinds of games (e.g. multiplayer quantitative Reachability games), weak SPEs and SPEs are equivalent, this characterization is useful in order to study SPEs in these games.Secondly, we use those different equilibrium characterizations to provide the exact complexity classes of different decision problems related to the existence of relevant equilibria. We mainly focus on the constrained existence problem: if each player aims at maximizing his gain, this problem asks whether there exists an equilibrium such that each resulting player’s gain is greater than a threshold (one per player). We also consider variants of relevant equilibria based on the social welfare and the Pareto optimality of the players’ payoff. In this way, we prove the exact complexity classes for (i) the weak SPE constrained existence problem in multiplayer games with classical qualitative objectives such as Büchi, co-Büchi and Safety and (ii) the NE and SPE constrained existence problems (and variants) for qualitative and quantitative reachability games. In the latter case, the upper bounds on the required memory for such relevant equilibria are studied and proved to be finite. Studying memory requirements of strategies is important since with the synthesis process those strategies have to be implemented.Finally, we consider multiplayer, non zero-sum, turn-based timed games with qualitative Reachability objectives together with the concept of SPE. We prove that the SPE constrained existence problem is EXPTIME-complete for qualitative Reachability timed games. In order to obtain an EXPTIME algorithm, we proceed in different steps. In the first step, we prove that the game variant of the classical region graph is a good abstraction for the SPE constrained existence problem. In fact, we identify conditions on bisimulations under which the study of SPE in a given game can be reduced to the study of its quotient. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished
| Identifer | oai:union.ndltd.org:ulb.ac.be/oai:dipot.ulb.ac.be:2013/322079 |
| Date | 27 April 2021 |
| Creators | Goeminne, Aline |
| Contributors | Brihaye, Thomas, Raskin, Jean-François, Bruyère, Véronique, Flesch, János, Geeraerts, Gilles, Sankur, Ocan |
| Publisher | Universite Libre de Bruxelles, Université de Mons, Faculté des Sciences, Département de Mathématique - Docteur en Sciences, Université libre de Bruxelles, Faculté des Sciences – Informatique, Mons |
| Source Sets | Université libre de Bruxelles |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/doctoralThesis, info:ulb-repo/semantics/doctoralThesis, info:ulb-repo/semantics/openurl/vlink-dissertation |
| Format | 346 p., 3 full-text file(s): application/pdf | application/pdf | application/pdf |
| Rights | 3 full-text file(s): info:eu-repo/semantics/closedAccess | info:eu-repo/semantics/restrictedAccess | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0031 seconds