---
res:
  bibo_abstract:
  - Multi-dimensional mean-payoff and energy games provide the mathematical foundation
    for the quantitative study of reactive systems, and play a central role in the
    emerging quantitative theory of verification and synthesis. In this work, we study
    the strategy synthesis problem for games with such multi-dimensional objectives
    along with a parity condition, a canonical way to express ω ω -regular conditions.
    While in general, the winning strategies in such games may require infinite memory,
    for synthesis the most relevant problem is the construction of a finite-memory
    winning strategy (if one exists). Our main contributions are as follows. First,
    we show a tight exponential bound (matching upper and lower bounds) on the memory
    required for finite-memory winning strategies in both multi-dimensional mean-payoff
    and energy games along with parity objectives. This significantly improves the
    triple exponential upper bound for multi energy games (without parity) that could
    be derived from results in literature for games on vector addition systems with
    states. Second, we present an optimal symbolic and incremental algorithm to compute
    a finite-memory winning strategy (if one exists) in such games. Finally, we give
    a complete characterization of when finite memory of strategies can be traded
    off for randomness. In particular, we show that for one-dimension mean-payoff
    parity games, randomized memoryless strategies are as powerful as their pure finite-memory
    counterparts.@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: Mickael
      foaf_name: Randour, Mickael
      foaf_surname: Randour
  - foaf_Person:
      foaf_givenName: Jean
      foaf_name: Raskin, Jean
      foaf_surname: Raskin
  bibo_doi: 10.1007/s00236-013-0182-6
  bibo_issue: 3-4
  bibo_volume: 51
  dct_date: 2014^xs_gYear
  dct_identifier:
  - UT:000335981500002
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Strategy synthesis for multi-dimensional quantitative objectives@
...