---
res:
bibo_abstract:
- '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
work, we consider both finite-state game graphs, and recursive game graphs (or
pushdown game graphs) that model the control flow of sequential programs with
recursion. The objectives we study are multidimensional mean-payoff objectives,
where the goal of player 1 is to ensure that the mean-payoff is non-negative in
all dimensions. In pushdown games two types of strategies are relevant: (1) global
strategies, that depend on the entire global history; and (2) modular strategies,
that have only local memory and thus do not depend on the context of invocation.
Our main contributions are as follows: (1) We show that finite-state multidimensional
mean-payoff games can be solved in polynomial time if the number of dimensions
and the maximal absolute value of the weights are fixed; whereas if the number
of dimensions is arbitrary, then the problem is known to be coNP-complete. (2)
We show that pushdown graphs with multidimensional mean-payoff objectives can
be solved in polynomial time. For both (1) and (2) our algorithms are based on
hyperplane separation technique. (3) For pushdown games under global strategies
both one and multidimensional mean-payoff objectives problems are known to be
undecidable, and we show that under modular strategies the multidimensional problem
is also undecidable; under modular strategies the one-dimensional problem is NP-complete.
We show that if the number of modules, the number of exits, and the maximal absolute
value of the weights are fixed, then pushdown games under modular strategies with
one-dimensional mean-payoff objectives can be solved in polynomial time, and if
either the number of exits or the number of modules is unbounded, then the problem
is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for
finite-state multidimensional mean-payoff games or pushdown games under modular
strategies with one-dimensional mean-payoff objectives would imply the fixed parameter
tractability of parity games.@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Yaron
foaf_name: Velner, Yaron
foaf_surname: Velner
bibo_doi: 10.1007/978-3-642-40184-8_35
bibo_volume: 8052
dct_date: 2013^xs_gYear
dct_language: eng
dct_publisher: Springer@
dct_title: Hyperplane separation technique for multidimensional mean-payoff games@
...