Mean-Payoff Parity Game

A mean-payoff parity game combines the reward objective of a mean-payoff game with the recurring-priority objective of a parity game. Each graph vertex of a finite directed graph is owned by Max or Min, has an integer reward and a nonnegative integer priority , and has an outgoing graph edge. The owner chooses the next graph edge with full knowledge of the preceding play.

In the minimum-priority convention, Max wins a play iff both

and the least priority appearing infinitely often is even. The is the infimum limit. Min wins whenever either requirement fails.