Highlights Conference 2017 Conference Abstract
Games with lexicographically ordered omega-regular objectives
- Quentin Hautem
Abstract available in PDF.
Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
Highlights Conference 2017 Conference Abstract
Abstract available in PDF.
GandALF Workshop 2016 Workshop Paper
Classical objectives in two-player zero-sum games played on graphs often deal with limit behaviors of infinite plays: e. g. , mean-payoff and total-payoff in the quantitative setting, or parity in the qualitative one (a canonical way to encode omega-regular properties). Those objectives offer powerful abstraction mechanisms and often yield nice properties such as memoryless determinacy. However, their very nature provides no guarantee on time bounds within which something good can be witnessed. In this work, we consider two approaches toward inclusion of time bounds in parity games. The first one, parity-response games, is based on the notion of finitary parity games [CHH09] and parity games with costs [FZ14, WZ16]. The second one, window parity games, is inspired by window mean-payoff games [CDRR15]. We compare the two approaches and show that while they prove to be equivalent in some contexts, window parity games offer a more tractable alternative when the time bound is given as a parameter (P-c. vs. PSPACE-c. ). In particular, it provides a conservative approximation of parity games computable in polynomial time. Furthermore, we extend both approaches to the multi-dimension setting. We give the full picture for both types of games with regard to complexity and memory bounds. [CHH09] K. Chatterjee, T. A. Henzinger, F. Horn (2009): Finitary winning in omega-regular games. ACM Trans. Comput. Log. 11(1). [FZ14] N. Fijalkow, M. Zimmermann (2014): Parity and Streett Games with Costs. LMCS 10(2). [WZ16] A. Weinert, M. Zimmermann (2016): Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. Proc. of CSL, LIPIcs, Schloss Dagstuhl - LZI. To appear. [CDRR15] K. Chatterjee, L. Doyen, M. Randour, J. -F. Raskin (2015): Looking at mean-payoff and total-payoff through windows. Information and Computation 242, pp. 25-52.
Highlights Conference 2015 Conference Abstract
In most system design problems, there is no unique objective to be op- timized, but multiple, potentially conflicting objectives. For example, in designing a controller, one is interested not only in minimizing the aver- age response time of the system but also in minimizing its average power consumption. Recently, in [CDHR10], multi-objective generalizations of mean-payoff and energy objectives have been studied. Nevertheless, in this work the multi-dimensionality is homogeneous in the sense that each dimension is measured with the same function: either the mean-payoff measure is used for all the dimensions, or the energy measure is used for all the dimensions. In our work, we want instead to consider the more ambitious goal of considering heterogeneous multi-dimensional quantitative games: we want to allow the use of different measures in the multiple quantitative dimensions. For example, we would like to use the energy measure (to record the energy consumption of the system) for one dimension and the mean-payoff measure for another dimension (to measure the mean response time of the system for example). The kind of questions that we try to solve are the following ones. Can we decide whether the system is able to achieve its objective from its initial configuration against any behavior of the environment? In case of positive answer, can we construct an appropriate strategy for the system to reach this goal? Can we optimize the parameters of such a winning strategy (size of required memory, quality of satisfaction of the objective, etc). For all these questions we are also interested in the computational complexities. Games that we here consider are zero-sum turn-based games played on a finite multi-dimensional weighted graph. Given a measure and a threshold (in Z) for each dimension, the objective of player 1 is the set of plays such that, for every dimension, the measure of the play (on the considered dimension) is greater or equal to the corresponding threshold. Since we consider heterogeneous multi-dimensional quantitative games, we allow the use of a different measure for each dimension. Firstly, we study games with ω-regular objectives in {inf, sup, liminf, limsup}. We prove that the decision problem for these games is PSPACE- complete, and that finite-memory winning strategies are sufficient for both players. Moreover, we get several refinements (on the number of occurrence of each kind of objective) saying when the problem becomes P-complete and when memory requirements can be improved. This is a first step in order to mix ω-regular objectives with one that is not (such as mean-payoff and energy), and more generally with several ones that are not ω-regular objectives. Secondly, we consider an additional ω-regular objective, the window-mean-payoff (WMP) introduced in [CDRR13] which is a conservative approximation of the mean-payoff objective considered over a local finite window sliding along a play, instead of the whole play. Adding this objective to {inf, sup, liminf, limsup} leads to an EXPTIME-complete (in- stead of PSPACE-complete) decision problem but still with finite-memory strategies for both players. We also study in which cases we can get a better complexity and better memory requirements. Finally, the value problem for one-dimensional WMP-games was not studied in [CDRR13], and we prove that it can be solved in polynomial time. Those results are joint work with Bruyère and Raskin. References [CDHR10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-Fran ̧cois Raskin. Generalized mean-payoff and energy games. In IARCS Annual Conference on Foundations of Soft- ware Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, pages 505–516, 2010. [CDRR13] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-Franc ̧ois Raskin. Looking at mean-payoff and total-payoff through windows. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, pages 118– 132, 2013.