@article{10674,
  abstract     = {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.},
  author       = {Aghajohari, Milad and Avni, Guy and Henzinger, Thomas A},
  issn         = {1860-5974},
  journal      = {Logical Methods in Computer Science},
  keywords     = {computer science, computer science and game theory, logic in computer science},
  number       = {1},
  pages        = {10:1--10:23},
  publisher    = {International Federation for Computational Logic},
  title        = {{Determinacy in discrete-bidding infinite-duration games}},
  doi          = {10.23638/LMCS-17(1:10)2021},
  volume       = {17},
  year         = {2021},
}

@inproceedings{10002,
  abstract     = {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 .},
  author       = {Chatterjee, Krishnendu and Dvorak, Wolfgang and Henzinger, Monika H and Svozil, Alexander},
  booktitle    = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
  isbn         = {978-1-6654-4896-3},
  issn         = {1043-6871},
  keywords     = {Computer science, Computational modeling, Markov processes, Probabilistic logic, Formal verification, Game Theory},
  location     = {Rome, Italy},
  pages        = {1--13},
  publisher    = {Institute of Electrical and Electronics Engineers},
  title        = {{Symbolic time and space tradeoffs for probabilistic verification}},
  doi          = {10.1109/LICS52264.2021.9470739},
  year         = {2021},
}

@article{11667,
  abstract     = {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.},
  author       = {Dütting, Paul and Henzinger, Monika H and Starnberger, Martin},
  issn         = {2167-8383},
  journal      = {ACM Transactions on Economics and Computation},
  keywords     = {Theory of computation, Algorithmic game theory and mechanism design, Applied computing, Economics, Simplified mechanisms, Combinatorial auctions with item bidding, Price of anarchy},
  number       = {2},
  publisher    = {Association for Computing Machinery},
  title        = {{Valuation compressions in VCG-based combinatorial auctions}},
  doi          = {10.1145/3232860},
  volume       = {6},
  year         = {2018},
}

@article{11669,
  abstract     = {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.},
  author       = {Dütting, Paul and Henzinger, Monika H and Starnberger, Martin},
  issn         = {2167-8383},
  journal      = {ACM Transactions on Economics and Computation},
  keywords     = {Algorithmic game theory, auction theory, Clinching auction, Pareto optimality, Budget limits},
  number       = {1},
  publisher    = {Association for Computing Machinery},
  title        = {{Auctions for heterogeneous items and budget limits}},
  doi          = {10.1145/2818351},
  volume       = {4},
  year         = {2015},
}