DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.8

Bidding Games with Charging

Authors: Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger, and Kaushik Mallik

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the "charges." Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?

Cite as

Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger, and Kaushik Mallik. Bidding Games with Charging. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2024.8,
  author =	{Avni, Guy and Kafshdar Goharshady, Ehsan and Henzinger, Thomas A. and Mallik, Kaushik},
  title =	{{Bidding Games with Charging}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.8},
  URN =		{urn:nbn:de:0030-drops-207807},
  doi =		{10.4230/LIPIcs.CONCUR.2024.8},
  annote =	{Keywords: Bidding games on graphs, \omega-regular objectives}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2024.2

Abstraction-Based Decision Making for Statistical Properties (Invited Talk)

Authors: Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

Sequential decision-making in probabilistic environments is a fundamental problem with many applications in AI and economics. In this paper, we present an algorithm for synthesizing sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the general setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, this paper presents the first PTIME synthesis algorithms. We introduce the notion of statistical abstraction, which clusters statistically indistinguishable input-output sequences into equivalence classes. This abstraction allows for a dynamic programming algorithm whose complexity grows polynomially with the considered horizon, making the statistical case exponentially more efficient than the general case. We evaluate our algorithm on three different application scenarios of a client-server protocol, where multiple clients compete via bidding to gain access to the service offered by the server. The synthesized policies optimize profit while guaranteeing that none of the server’s clients is disproportionately starved of the service.

Cite as

Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. Abstraction-Based Decision Making for Statistical Properties (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cano_et_al:LIPIcs.FSCD.2024.2,
  author =	{Cano, Filip and Henzinger, Thomas A. and K\"{o}nighofer, Bettina and Kueffner, Konstantin and Mallik, Kaushik},
  title =	{{Abstraction-Based Decision Making for Statistical Properties}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.2},
  URN =		{urn:nbn:de:0030-drops-203310},
  doi =		{10.4230/LIPIcs.FSCD.2024.2},
  annote =	{Keywords: Abstract interpretation, Sequential decision making, Counter machines}
}

Search Results

Documents authored by Mallik, Kaushik

Bidding Games with Charging

Abstract

Cite as

Abstraction-Based Decision Making for Statistical Properties (Invited Talk)

Abstract

Cite as

Thanks for your feedback!

Could not send message