Mean-Payoff Parity Games

Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski

Games played on graphs may have qualitative objectives, such as the satisfaction of an omega-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory.

Proceedings of the 20th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, 2005, pp. 178-187.

Download inofficial, sometimes updated PostScript / PDF document. © 2005 IEEE.