Heterogeneous multi-dimensional quantitative games

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.

Authors

• Quentin Hautem

Keywords

No keywords are indexed for this paper.