---
_id: '10674'
abstract:
- lang: eng
  text: 'In two-player games on graphs, the players move a token through a graph to
    produce an infinite path, which determines the winner of the game. Such games
    are central in formal methods since they model the interaction between a non-terminating
    system and its environment. In bidding games the players bid for the right to
    move the token: in each round, the players simultaneously submit bids, and the
    higher bidder moves the token and pays the other player. Bidding games are known
    to have a clean and elegant mathematical structure that relies on the ability
    of the players to submit arbitrarily small bids. Many applications, however, require
    a fixed granularity for the bids, which can represent, for example, the monetary
    value expressed in cents. We study, for the first time, the combination of discrete-bidding
    and infinite-duration games. Our most important result proves that these games
    form a large determined subclass of concurrent games, where determinacy is the
    strong property that there always exists exactly one player who can guarantee
    winning the game. In particular, we show that, in contrast to non-discrete bidding
    games, the mechanism with which tied bids are resolved plays an important role
    in discrete-bidding games. We study several natural tie-breaking mechanisms and
    show that, while some do not admit determinacy, most natural mechanisms imply
    determinacy for every pair of initial budgets.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
  (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M
  2369-N33 (Meitner fellowship).\r\n"
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Milad
  full_name: Aghajohari, Milad
  last_name: Aghajohari
- 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
citation:
  ama: Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration
    games. <i>Logical Methods in Computer Science</i>. 2021;17(1):10:1-10:23. doi:<a
    href="https://doi.org/10.23638/LMCS-17(1:10)2021">10.23638/LMCS-17(1:10)2021</a>
  apa: Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2021). Determinacy in discrete-bidding
    infinite-duration games. <i>Logical Methods in Computer Science</i>. International
    Federation for Computational Logic. <a href="https://doi.org/10.23638/LMCS-17(1:10)2021">https://doi.org/10.23638/LMCS-17(1:10)2021</a>
  chicago: Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding
    Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>. International
    Federation for Computational Logic, 2021. <a href="https://doi.org/10.23638/LMCS-17(1:10)2021">https://doi.org/10.23638/LMCS-17(1:10)2021</a>.
  ieee: M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding
    infinite-duration games,” <i>Logical Methods in Computer Science</i>, vol. 17,
    no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.
  ista: Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding
    infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.
  mla: Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration
    Games.” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1, International
    Federation for Computational Logic, 2021, p. 10:1-10:23, doi:<a href="https://doi.org/10.23638/LMCS-17(1:10)2021">10.23638/LMCS-17(1:10)2021</a>.
  short: M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science
    17 (2021) 10:1-10:23.
date_created: 2022-01-25T16:32:13Z
date_published: 2021-02-03T00:00:00Z
date_updated: 2023-08-17T06:56:42Z
day: '03'
ddc:
- '510'
department:
- _id: ToHe
doi: 10.23638/LMCS-17(1:10)2021
external_id:
  arxiv:
  - '1905.03588'
  isi:
  - '000658724600010'
file:
- access_level: open_access
  checksum: b35586a50ed1ca8f44767de116d18d81
  content_type: application/pdf
  creator: alisjak
  date_created: 2022-01-26T08:04:50Z
  date_updated: 2022-01-26T08:04:50Z
  file_id: '10690'
  file_name: 2021_LMCS_AGHAJOHAR.pdf
  file_size: 819878
  relation: main_file
  success: 1
file_date_updated: 2022-01-26T08:04:50Z
has_accepted_license: '1'
intvolume: '        17'
isi: 1
issue: '1'
keyword:
- computer science
- computer science and game theory
- logic in computer science
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 10:1-10:23
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: M02369
  name: Formal Methods meets Algorithmic Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Logical Methods in Computer Science
publication_identifier:
  eissn:
  - 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
quality_controlled: '1'
scopus_import: '1'
status: public
title: Determinacy in discrete-bidding infinite-duration games
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 17
year: '2021'
...
---
_id: '10002'
abstract:
- lang: eng
  text: 'We present a faster symbolic algorithm for the following central problem
    in probabilistic verification: Compute the maximal end-component (MEC) decomposition
    of Markov decision processes (MDPs). This problem generalizes the SCC decomposition
    problem of graphs and closed recurrent sets of Markov chains. The model of symbolic
    algorithms is widely used in formal verification and model-checking, where access
    to the input model is restricted to only symbolic operations (e.g., basic set
    operations and computation of one-step neighborhood). For an input MDP with  n  vertices
    and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition
    requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other
    symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations
    and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound
    for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic
    operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our
    algorithm provides a trade-off between symbolic operations and symbolic space:
    for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations
    and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques
    we present faster algorithms for computing the almost-sure winning regions of  ω
    -regular objectives for MDPs. We consider the canonical parity objectives for  ω
    -regular objectives, and for parity objectives with  d -priorities we present
    an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic
    operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .'
acknowledgement: The authors are grateful to the anonymous referees for their valuable
  comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF)
  through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF)
  NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For
  M. H. the research leading to these results has received funding from the European
  Research Council under the European Unions Seventh Framework Programme (FP/2007–2013)
  / ERC Grant Agreement no. 340506.
article_processing_charge: No
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: Wolfgang
  full_name: Dvorak, Wolfgang
  last_name: Dvorak
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Alexander
  full_name: Svozil, Alexander
  last_name: Svozil
citation:
  ama: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs
    for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics
    Engineers; 2021:1-13. doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>'
  apa: 'Chatterjee, K., Dvorak, W., Henzinger, M. H., &#38; Svozil, A. (2021). Symbolic
    time and space tradeoffs for probabilistic verification. In <i>Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13).
    Rome, Italy: Institute of Electrical and Electronics Engineers. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander
    Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In
    <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>,
    1–13. Institute of Electrical and Electronics Engineers, 2021. <a href="https://doi.org/10.1109/LICS52264.2021.9470739">https://doi.org/10.1109/LICS52264.2021.9470739</a>.
  ieee: K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and
    space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th
    Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021,
    pp. 1–13.
  ista: 'Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space
    tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE
    Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science,
    1–13.'
  mla: Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic
    Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in
    Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021,
    pp. 1–13, doi:<a href="https://doi.org/10.1109/LICS52264.2021.9470739">10.1109/LICS52264.2021.9470739</a>.
  short: K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of
    the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of
    Electrical and Electronics Engineers, 2021, pp. 1–13.
conference:
  end_date: 2021-07-02
  location: Rome, Italy
  name: 'LICS: Symposium on Logic in Computer Science'
  start_date: 2021-06-29
date_created: 2021-09-12T22:01:24Z
date_published: 2021-07-07T00:00:00Z
date_updated: 2025-07-14T09:10:07Z
day: '07'
department:
- _id: KrCh
doi: 10.1109/LICS52264.2021.9470739
ec_funded: 1
external_id:
  arxiv:
  - '2104.07466'
  isi:
  - '000947350400089'
isi: 1
keyword:
- Computer science
- Computational modeling
- Markov processes
- Probabilistic logic
- Formal verification
- Game Theory
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.07466
month: '07'
oa: 1
oa_version: Preprint
page: 1-13
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer
  Science
publication_identifier:
  eisbn:
  - 978-1-6654-4895-6
  isbn:
  - 978-1-6654-4896-3
  issn:
  - 1043-6871
publication_status: published
publisher: Institute of Electrical and Electronics Engineers
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic time and space tradeoffs for probabilistic verification
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '11667'
abstract:
- lang: eng
  text: The focus of classic mechanism design has been on truthful direct-revelation
    mechanisms. In the context of combinatorial auctions, the truthful direct-revelation
    mechanism that maximizes social welfare is the Vickrey-Clarke-Groves mechanism.
    For many valuation spaces, computing the allocation and payments of the VCG mechanism,
    however, is a computationally hard problem. We thus study the performance of the
    VCG mechanism when bidders are forced to choose bids from a subspace of the valuation
    space for which the VCG outcome can be computed efficiently. We prove improved
    upper bounds on the welfare loss for restrictions to additive bids and upper and
    lower bounds for restrictions to non-additive bids. These bounds show that increased
    expressiveness can give rise to additional equilibria of poorer efficiency.
article_number: '5'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Paul
  full_name: Dütting, Paul
  last_name: Dütting
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Martin
  full_name: Starnberger, Martin
  last_name: Starnberger
citation:
  ama: Dütting P, Henzinger MH, Starnberger M. Valuation compressions in VCG-based
    combinatorial auctions. <i>ACM Transactions on Economics and Computation</i>.
    2018;6(2). doi:<a href="https://doi.org/10.1145/3232860">10.1145/3232860</a>
  apa: Dütting, P., Henzinger, M. H., &#38; Starnberger, M. (2018). Valuation compressions
    in VCG-based combinatorial auctions. <i>ACM Transactions on Economics and Computation</i>.
    Association for Computing Machinery. <a href="https://doi.org/10.1145/3232860">https://doi.org/10.1145/3232860</a>
  chicago: Dütting, Paul, Monika H Henzinger, and Martin Starnberger. “Valuation Compressions
    in VCG-Based Combinatorial Auctions.” <i>ACM Transactions on Economics and Computation</i>.
    Association for Computing Machinery, 2018. <a href="https://doi.org/10.1145/3232860">https://doi.org/10.1145/3232860</a>.
  ieee: P. Dütting, M. H. Henzinger, and M. Starnberger, “Valuation compressions in
    VCG-based combinatorial auctions,” <i>ACM Transactions on Economics and Computation</i>,
    vol. 6, no. 2. Association for Computing Machinery, 2018.
  ista: Dütting P, Henzinger MH, Starnberger M. 2018. Valuation compressions in VCG-based
    combinatorial auctions. ACM Transactions on Economics and Computation. 6(2), 5.
  mla: Dütting, Paul, et al. “Valuation Compressions in VCG-Based Combinatorial Auctions.”
    <i>ACM Transactions on Economics and Computation</i>, vol. 6, no. 2, 5, Association
    for Computing Machinery, 2018, doi:<a href="https://doi.org/10.1145/3232860">10.1145/3232860</a>.
  short: P. Dütting, M.H. Henzinger, M. Starnberger, ACM Transactions on Economics
    and Computation 6 (2018).
date_created: 2022-07-27T11:46:46Z
date_published: 2018-05-01T00:00:00Z
date_updated: 2022-09-09T12:04:42Z
day: '01'
doi: 10.1145/3232860
extern: '1'
external_id:
  arxiv:
  - '1310.3153'
intvolume: '         6'
issue: '2'
keyword:
- Theory of computation
- Algorithmic game theory and mechanism design
- Applied computing
- Economics
- Simplified mechanisms
- Combinatorial auctions with item bidding
- Price of anarchy
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1310.3153
month: '05'
oa: 1
oa_version: Preprint
publication: ACM Transactions on Economics and Computation
publication_identifier:
  eissn:
  - 2167-8383
  issn:
  - 2167-8375
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Valuation compressions in VCG-based combinatorial auctions
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2018'
...
---
_id: '11669'
abstract:
- lang: eng
  text: We study individual rational, Pareto-optimal, and incentive compatible mechanisms
    for auctions with heterogeneous items and budget limits. We consider settings
    with multiunit demand and additive valuations. For single-dimensional valuations
    we prove a positive result for randomized mechanisms, and a negative result for
    deterministic mechanisms. While the positive result allows for private budgets,
    the negative result is for public budgets. For multidimensional valuations and
    public budgets we prove an impossibility result that applies to deterministic
    and randomized mechanisms. Taken together this shows the power of randomization
    in certain settings with heterogeneous items, but it also shows its limitations.
article_number: '4'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Paul
  full_name: Dütting, Paul
  last_name: Dütting
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Martin
  full_name: Starnberger, Martin
  last_name: Starnberger
citation:
  ama: Dütting P, Henzinger MH, Starnberger M. Auctions for heterogeneous items and
    budget limits. <i>ACM Transactions on Economics and Computation</i>. 2015;4(1).
    doi:<a href="https://doi.org/10.1145/2818351">10.1145/2818351</a>
  apa: Dütting, P., Henzinger, M. H., &#38; Starnberger, M. (2015). Auctions for heterogeneous
    items and budget limits. <i>ACM Transactions on Economics and Computation</i>.
    Association for Computing Machinery. <a href="https://doi.org/10.1145/2818351">https://doi.org/10.1145/2818351</a>
  chicago: Dütting, Paul, Monika H Henzinger, and Martin Starnberger. “Auctions for
    Heterogeneous Items and Budget Limits.” <i>ACM Transactions on Economics and Computation</i>.
    Association for Computing Machinery, 2015. <a href="https://doi.org/10.1145/2818351">https://doi.org/10.1145/2818351</a>.
  ieee: P. Dütting, M. H. Henzinger, and M. Starnberger, “Auctions for heterogeneous
    items and budget limits,” <i>ACM Transactions on Economics and Computation</i>,
    vol. 4, no. 1. Association for Computing Machinery, 2015.
  ista: Dütting P, Henzinger MH, Starnberger M. 2015. Auctions for heterogeneous items
    and budget limits. ACM Transactions on Economics and Computation. 4(1), 4.
  mla: Dütting, Paul, et al. “Auctions for Heterogeneous Items and Budget Limits.”
    <i>ACM Transactions on Economics and Computation</i>, vol. 4, no. 1, 4, Association
    for Computing Machinery, 2015, doi:<a href="https://doi.org/10.1145/2818351">10.1145/2818351</a>.
  short: P. Dütting, M.H. Henzinger, M. Starnberger, ACM Transactions on Economics
    and Computation 4 (2015).
date_created: 2022-07-27T12:09:15Z
date_published: 2015-12-05T00:00:00Z
date_updated: 2022-09-09T12:08:37Z
day: '05'
doi: 10.1145/2818351
extern: '1'
external_id:
  arxiv:
  - '1209.6448'
intvolume: '         4'
issue: '1'
keyword:
- Algorithmic game theory
- auction theory
- Clinching auction
- Pareto optimality
- Budget limits
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1209.6448
month: '12'
oa: 1
oa_version: Preprint
publication: ACM Transactions on Economics and Computation
publication_identifier:
  eissn:
  - 2167-8383
  issn:
  - 2167-8375
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Auctions for heterogeneous items and budget limits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2015'
...