Date Added: Oct 2012
Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this paper, the authors consider both finite-state game graphs and recursive game graphs that can model the control flow of sequential programs with recursion. The objectives they consider are multi-dimensional mean-payoff objectives, where the goal of player 1 is to ensure that the mean-payoff is at least zero in all dimensions. In pushdown games two types of strategies are relevant: global strategies, that depend on the entire global history and modular strategies that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module.