Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam: a winning strategy. It is often assumed that Eve always knows the exact state of the game, that is, she has full observation. In this dissertation, we are interested in two variations of quantitative games. First, we study a different kind of strategy for Eve. More specifically, we consider strategies that minimize her regret: the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. Second, we study the effect of relaxing the full observation assumption on the complexity of computing winning strategies for Eve. Regarding regret-minimizing strategies, we give algorithms to compute the strategies of Eve that ensure minimal regret against three classes of adversaries: (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. These results apply for quantitative games defined with the classical payoff functions Inf, Sup, LimInf, LimSup, mean payoff, and discounted sum. For partial-observation games, we continue the study of energy and mean- payoff games started in 2010 by Degorre et al. We complement their decidability result for a particular problem related to energy games (the Fixed Initial Credit Problem) by giving tight complexity bounds for it. Also, we show that mean-payoff games are undecidable for all versions of the mean-payoff function. Motivated by the latter negative result, we define and study several decidable sub-classes of mean-payoff games. Finally we extend the newly introduced window mean-payoff objectives to the partial observation setting. We show that they are conservative approximations of partial-observation mean-payoff games and we classify them according to whether they are decidable. Furthermore, we give a symbolic algorithm to solve them. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished
| Identifer | oai:union.ndltd.org:ulb.ac.be/oai:dipot.ulb.ac.be:2013/239330 |
| Date | 03 November 2016 |
| Creators | Perez, Guillermo A. |
| Contributors | Raskin, Jean-François, Cardinal, Jean, Geeraerts, Gilles, Chatterjee, Krishnendu, Worrell, J., Bruyère, Véronique |
| Publisher | Universite Libre de Bruxelles, Université libre de Bruxelles, Faculté des Sciences – Informatique, Bruxelles |
| 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 | 214 p., No full-text files |
Page generated in 0.0027 seconds