---
_id: '6752'
abstract:
- lang: eng
  text: 'Two-player games on graphs are widely studied in formal methods, as they
    model the interaction between a system and its environment. The game is played
    by moving a token throughout a graph to produce an infinite path. There are several
    common modes to determine how the players move the token through the graph; e.g.,
    in turn-based games the players alternate turns in moving the token. We study
    the bidding mode of moving the token, which, to the best of our knowledge, has
    never been studied in infinite-duration games. The following bidding rule was
    previously defined and called Richman bidding. Both players have separate budgets,
    which sum up to 1. In each turn, a bidding takes place: Both players submit bids
    simultaneously, where a bid is legal if it does not exceed the available budget,
    and the higher bidder pays his bid to the other player and moves the token. The
    central question studied in bidding games is a necessary and sufficient initial
    budget for winning the game: a threshold budget in a vertex is a value t ∈ [0,
    1] such that if Player 1’s budget exceeds t, he can win the game; and if Player
    2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously
    shown to exist in every vertex of a reachability game, which have an interesting
    connection with random-turn games—a sub-class of simple stochastic games in which
    the player who moves is chosen randomly. We show the existence of threshold budgets
    for a qualitative class of infinite-duration games, namely parity games, and a
    quantitative class, namely mean-payoff games. The key component of the proof is
    a quantitative solution to strongly connected mean-payoff bidding games in which
    we extend the connection with random-turn games to these games, and construct
    explicit optimal strategies for both players.'
article_number: '31'
article_processing_charge: No
arxiv: 1
author:
- first_name: Guy
  full_name: Avni, Guy
  id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
  last_name: Avni
  orcid: 0000-0001-5588-8287
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ventsislav K
  full_name: Chonev, Ventsislav K
  id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
  last_name: Chonev
citation:
  ama: Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. <i>Journal
    of the ACM</i>. 2019;66(4). doi:<a href="https://doi.org/10.1145/3340295">10.1145/3340295</a>
  apa: Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2019). Infinite-duration bidding
    games. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/3340295">https://doi.org/10.1145/3340295</a>
  chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
    Bidding Games.” <i>Journal of the ACM</i>. ACM, 2019. <a href="https://doi.org/10.1145/3340295">https://doi.org/10.1145/3340295</a>.
  ieee: G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
    <i>Journal of the ACM</i>, vol. 66, no. 4. ACM, 2019.
  ista: Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal
    of the ACM. 66(4), 31.
  mla: Avni, Guy, et al. “Infinite-Duration Bidding Games.” <i>Journal of the ACM</i>,
    vol. 66, no. 4, 31, ACM, 2019, doi:<a href="https://doi.org/10.1145/3340295">10.1145/3340295</a>.
  short: G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).
date_created: 2019-08-04T21:59:16Z
date_published: 2019-07-16T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '16'
department:
- _id: ToHe
doi: 10.1145/3340295
external_id:
  arxiv:
  - '1705.01433'
  isi:
  - '000487714900008'
intvolume: '        66'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1705.01433
month: '07'
oa: 1
oa_version: Preprint
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 264B3912-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: M02369
  name: Formal Methods meets Algorithmic Game Theory
publication: Journal of the ACM
publication_identifier:
  eissn:
  - 1557735X
  issn:
  - '00045411'
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
  record:
  - id: '950'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Infinite-duration bidding games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 66
year: '2019'
...
---
_id: '716'
abstract:
- lang: eng
  text: '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 solving recursive game graphs (or pushdown game graphs) that
    model the control flow of sequential programs with recursion.While pushdown games
    have been studied before with qualitative objectives-such as reachability and
    ?-regular objectives- in this work, we study for the first time such games with
    the most well-studied quantitative objective, the mean-payoff objective. In pushdown
    games, two types of strategies are relevant: (1) global strategies, which depend
    on the entire global history; and (2) modular strategies, which have only local
    memory and thus do not depend on the context of invocation but rather only on
    the history of the current invocation of the module. Our main results are as follows:
    (1) One-player pushdown games with mean-payoff objectives under global strategies
    are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff
    objectives under global strategies are undecidable. (3) One-player pushdown games
    with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player
    pushdown games with mean-payoff objectives under modular strategies can be solved
    in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives
    under modular strategies are NP-complete). We also establish the optimal strategy
    complexity by showing that global strategies for mean-payoff objectives require
    infinite memory even in one-player pushdown games and memoryless modular strategies
    are sufficient in two-player pushdown games. Finally, we also show that all the
    problems have the same complexity if the stack boundedness condition is added,
    where along with the mean-payoff objective the player must also ensure that the
    stack height is bounded.'
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Yaron
  full_name: Velner, Yaron
  last_name: Velner
citation:
  ama: Chatterjee K, Velner Y. The complexity of mean-payoff pushdown games. <i>Journal
    of the ACM</i>. 2017;64(5):34. doi:<a href="https://doi.org/10.1145/3121408">10.1145/3121408</a>
  apa: Chatterjee, K., &#38; Velner, Y. (2017). The complexity of mean-payoff pushdown
    games. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/3121408">https://doi.org/10.1145/3121408</a>
  chicago: Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff
    Pushdown Games.” <i>Journal of the ACM</i>. ACM, 2017. <a href="https://doi.org/10.1145/3121408">https://doi.org/10.1145/3121408</a>.
  ieee: K. Chatterjee and Y. Velner, “The complexity of mean-payoff pushdown games,”
    <i>Journal of the ACM</i>, vol. 64, no. 5. ACM, p. 34, 2017.
  ista: Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games.
    Journal of the ACM. 64(5), 34.
  mla: Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown
    Games.” <i>Journal of the ACM</i>, vol. 64, no. 5, ACM, 2017, p. 34, doi:<a href="https://doi.org/10.1145/3121408">10.1145/3121408</a>.
  short: K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.
date_created: 2018-12-11T11:48:06Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2021-01-12T08:12:08Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3121408
ec_funded: 1
external_id:
  arxiv:
  - '1201.2829'
intvolume: '        64'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1201.2829
month: '09'
oa: 1
oa_version: Preprint
page: '34'
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Journal of the ACM
publication_identifier:
  issn:
  - '00045411'
publication_status: published
publisher: ACM
publist_id: '6964'
quality_controlled: '1'
scopus_import: 1
status: public
title: The complexity of mean-payoff pushdown games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 64
year: '2017'
...