Strategy Synthesis for Mean-Payoff Expression Objectives
Yaron Velner · arXiv (Cornell University) · 2012
Mean-payoff expressions are the closure of mean-payoff objectives under the algebraic operations of min, max and sum. This class of objectives was introduced by Chatterjee et al., and the decidability of the verification problem (that is, one-player games) for such objective was established. In this paper, we study, for the first time, synthesis problems for mean-payoff expression objectives, and the most relevant problem is the synthesis of a finite-memory controller. This problem is captured by two-player mean-payoff expression games on graph, where the objective of one player is to maximize the value of the expression, the objective of the other player is to minimize the value, and player 1 is restricted to finite-memory strategies. Our main contribution is an effective algorithm that computes the optimal value that player 1 can achieve by a finite-memory strategy. (More accurately, the algorithm computes the least upper bound on the achievable values.)