Search Results

Documents authored by Avni, Guy

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
DOI: 10.4230/LIPIcs.CONCUR.2023.16
A Game of Pawns

Authors: Guy Avni, Pranav Ghorpade, and Shibashis Guha

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce and study pawn games, a class of two-player zero-sum turn-based graph games. A turn-based graph game proceeds by placing a token on an initial vertex, and whoever controls the vertex on which the token is located, chooses its next location. This leads to a path in the graph, which determines the winner. Traditionally, the control of vertices is predetermined and fixed. The novelty of pawn games is that control of vertices changes dynamically throughout the game as follows. Each vertex of a pawn game is owned by a pawn. In each turn, the pawns are partitioned between the two players, and the player who controls the pawn that owns the vertex on which the token is located, chooses the next location of the token. Control of pawns changes dynamically throughout the game according to a fixed mechanism. Specifically, we define several grabbing-based mechanisms in which control of at most one pawn transfers at the end of each turn. We study the complexity of solving pawn games, where we focus on reachability objectives and parameterize the problem by the mechanism that is being used and by restrictions on pawn ownership of vertices. On the positive side, even though pawn games are exponentially-succinct turn-based games, we identify several natural classes that can be solved in PTIME. On the negative side, we identify several EXPTIME-complete classes, where our hardness proofs are based on a new class of games called Lock & Key games, which may be of independent interest.
Cite as

Guy Avni, Pranav Ghorpade, and Shibashis Guha. A Game of Pawns. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2023.16,
  author =	{Avni, Guy and Ghorpade, Pranav and Guha, Shibashis},
  title =	{{A Game of Pawns}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.16},
  URN =		{urn:nbn:de:0030-drops-190100},
  doi =		{10.4230/LIPIcs.CONCUR.2023.16},
  annote =	{Keywords: Graph games, Reachability games, Pawn games, Dynamic vertex control}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.30
Computing Threshold Budgets in Discrete-Bidding Games

Authors: Guy Avni and Suman Sadhukhan

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
In a two-player zero-sum graph game, the players move a token throughout the graph to produce an infinite play, which determines the winner of the game. Bidding games are graph games in which in each turn, an auction (bidding) determines which player moves the token: the players have budgets, and in each turn, both players simultaneously submit bids that do not exceed their available budgets, the higher bidder moves the token, and pays the bid to the lower bidder. We distinguish between continuous- and discrete-bidding games. In the latter, the granularity of the players' bids is restricted, e.g., bids must be given in cents. Continuous-bidding games are well understood, however, from a practical standpoint, discrete-bidding games are more appealing. In this paper we focus on discrete-bidding games. We study the problem of finding threshold budgets; namely, a necessary and sufficient initial budget for winning the game. Previously, the properties of threshold budgets were only studied for reachability games. For parity discrete-bidding games, thresholds were known to exist, but their structure was not understood. We describe two algorithms for finding threshold budgets in parity discrete-bidding games. The first algorithm is a fixed-point algorithm, and it reveals the structure of the threshold budgets in these games. Second, we show that the problem of finding threshold budgets is in NP and coNP for parity discrete-bidding games. Previously, only exponential-time algorithms where known for reachability and parity objectives. A corollary of this proof is a construction of strategies that use polynomial-size memory.
Cite as

Guy Avni and Suman Sadhukhan. Computing Threshold Budgets in Discrete-Bidding Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.FSTTCS.2022.30,
  author =	{Avni, Guy and Sadhukhan, Suman},
  title =	{{Computing Threshold Budgets in Discrete-Bidding Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.30},
  URN =		{urn:nbn:de:0030-drops-174222},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.30},
  annote =	{Keywords: Discrete bidding games, Richman games, parity games, reachability games}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.3
An Updated Survey of Bidding Games on Graphs (Invited Talk)

Authors: Guy Avni and Thomas A. Henzinger

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We summarize how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. An Updated Survey of Bidding Games on Graphs (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 3:1-3:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2022.3,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{An Updated Survey of Bidding Games on Graphs}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{3:1--3:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert 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.MFCS.2022.3},
  URN =		{urn:nbn:de:0030-drops-168017},
  doi =		{10.4230/LIPIcs.MFCS.2022.3},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.2
A Survey of Bidding Games on Graphs (Invited Paper)

Authors: Guy Avni and Thomas A. Henzinger

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. A Survey of Bidding Games on Graphs (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2020.2,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{A Survey of Bidding Games on Graphs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.2},
  URN =		{urn:nbn:de:0030-drops-128147},
  doi =		{10.4230/LIPIcs.CONCUR.2020.2},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.11
Bidding Mechanisms in Graph Games

Authors: Guy Avni, Thomas A. Henzinger, and Đorđe Žikelić

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the "bank" rather than the other player. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding.
Cite as

Guy Avni, Thomas A. Henzinger, and Đorđe Žikelić. Bidding Mechanisms in Graph Games. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2019.11,
  author =	{Avni, Guy and Henzinger, Thomas A. and \v{Z}ikeli\'{c}, {\D}or{\d}e},
  title =	{{Bidding Mechanisms in Graph Games}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{11:1--11:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.11},
  URN =		{urn:nbn:de:0030-drops-109553},
  doi =		{10.4230/LIPIcs.MFCS.2019.11},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, taxman bidding, mean-payoff games, random-turn games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.20
Determinacy in Discrete-Bidding Infinite-Duration Games

Authors: Milad Aghajohari, Guy Avni, and Thomas A. Henzinger

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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.
Cite as

Milad Aghajohari, Guy Avni, and Thomas A. Henzinger. Determinacy in Discrete-Bidding Infinite-Duration Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{aghajohari_et_al:LIPIcs.CONCUR.2019.20,
  author =	{Aghajohari, Milad and Avni, Guy and Henzinger, Thomas A.},
  title =	{{Determinacy in Discrete-Bidding Infinite-Duration Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.20},
  URN =		{urn:nbn:de:0030-drops-109226},
  doi =		{10.4230/LIPIcs.CONCUR.2019.20},
  annote =	{Keywords: Bidding games, Richman games, determinacy, concurrent games, discrete bidding}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.23
Timed Network Games with Clocks

Authors: Guy Avni, Shibashis Guha, and Orna Kupferman

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertices. The cost of traversing an edge depends on the load; namely, number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in determining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, actual sharing and congestion of resources crucially depends on time. In [G. Avni et al., 2017], we introduced timed network games, which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. Each edge in the network is guarded by the time intervals in which it can be traversed, which forces the players to spend time in the vertices. In this work we significantly extend the way time can be referred to in timed network games. In the model we study, the network is equipped with clocks, and, as in timed automata, edges are guarded by constraints on the values of the clocks, and their traversal may involve a reset of some clocks. We argue that the stronger model captures many realistic networks. The addition of clocks breaks the techniques we developed in [G. Avni et al., 2017] and we develop new techniques in order to show that positive results on classic network games carry over to the stronger timed setting.
Cite as

Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games with Clocks. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2018.23,
  author =	{Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =	{{Timed Network Games with Clocks}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.23},
  URN =		{urn:nbn:de:0030-drops-96053},
  doi =		{10.4230/LIPIcs.MFCS.2018.23},
  annote =	{Keywords: Network games, Timed automata, Nash equilibrium, Equilibrium inefficiency}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.37
Timed Network Games

Authors: Guy Avni, Shibashis Guha, and Orna Kupferman

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games, which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed.
Cite as

Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2017.37,
  author =	{Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =	{{Timed Network Games}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.37},
  URN =		{urn:nbn:de:0030-drops-80675},
  doi =		{10.4230/LIPIcs.MFCS.2017.37},
  annote =	{Keywords: Network Games, Timed Automata, Nash Equilibrium, Equilibrium Inefficiency}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.21
Infinite-Duration Bidding Games

Authors: Guy Avni, Thomas A. Henzinger, and Ventsislav Chonev

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
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. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games [Lazarus1999,Lazarus2012]. There, a central question is the existence and computation of threshold budgets; namely, a value t \in [0,1] such that if \PO's budget exceeds t, he can win the game, and if \PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games.
Cite as

Guy Avni, Thomas A. Henzinger, and Ventsislav Chonev. Infinite-Duration Bidding Games. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2017.21,
  author =	{Avni, Guy and Henzinger, Thomas A. and Chonev, Ventsislav},
  title =	{{Infinite-Duration Bidding Games}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.21},
  URN =		{urn:nbn:de:0030-drops-77741},
  doi =		{10.4230/LIPIcs.CONCUR.2017.21},
  annote =	{Keywords: Bidding Games, Parity Games, Mean-Payoff Games, Richman Games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.365
Congestion Games with Multisets of Resources and Applications in Synthesis

Authors: Guy Avni, Orna Kupferman, and Tami Tamir

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
In classical congestion games, players' strategies are subsets of resources. We introduce and study multiset congestion games, where players' strategies are multisets of resources. Thus, in each strategy a player may need to use each resource a different number of times, and his cost for using the resource depends on the load that he and the other players generate on the resource. Beyond the theoretical interest in examining the effect of a repeated use of resources, our study enables better understanding of non-cooperative systems and environments whose behavior is not covered by previously studied models. Indeed, congestion games with multiset-strategies arise, for example, in production planing and network formation with tasks that are more involved than reachability. We study in detail the application of synthesis from component libraries: different users synthesize systems by gluing together components from a component library. A component may be used in several systems and may be used several times in a system. The performance of a component and hence the system's quality depends on the load on it. Our results reveal how the richer setting of multisets congestion games affects the stability and equilibrium efficiency compared to standard congestion games. In particular, while we present very simple instances with no pure Nash equilibrium and prove tighter and simpler lower bounds for equilibrium inefficiency, we are also able to show that some of the positive results known for affine and weighted congestion games apply to the richer setting of multisets.
Cite as

Guy Avni, Orna Kupferman, and Tami Tamir. Congestion Games with Multisets of Resources and Applications in Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 365-379, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.FSTTCS.2015.365,
  author =	{Avni, Guy and Kupferman, Orna and Tamir, Tami},
  title =	{{Congestion Games with Multisets of Resources and Applications in Synthesis}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{365--379},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.365},
  URN =		{urn:nbn:de:0030-drops-56358},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.365},
  annote =	{Keywords: Congestion games, Multiset strategies, Equilibrium existence and computation, Equilibrium inefficiency}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.325
Repairing Multi-Player Games

Authors: Shaull Almagor, Guy Avni, and Orna Kupferman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Synthesis is the automated construction of systems from their specifications. Modern systems often consist of interacting components, each having its own objective. The interaction among the components is modeled by a multi-player game. Strategies of the components induce a trace in the game, and the objective of each component is to force the game into a trace that satisfies its specification. This is modeled by augmenting the game with omega-regular winning conditions. Unlike traditional synthesis games, which are zero-sum, here the objectives of the components do not necessarily contradict each other. Accordingly, typical questions about these games concern their stability - whether the players reach an equilibrium, and their social welfare - maximizing the set of (possibly weighted) specifications that are satisfied. We introduce and study repair of multi-player games. Given a game, we study the possibility of modifying the objectives of the players in order to obtain stability or to improve the social welfare. Specifically, we solve the problem of modifying the winning conditions in a given concurrent multi-player game in a way that guarantees the existence of a Nash equilibrium. Each modification has a value, reflecting both the cost of strengthening or weakening the underlying specifications, as well as the benefit of satisfying specifications in the obtained equilibrium. We seek optimal modifications, and we study the problem for various omega-regular objectives and various cost and benefit functions. We analyze the complexity of the problem in the general setting as well as in one with a fixed number of players. We also study two additional types of repair, namely redirection of transitions and control of a subset of the players.
Cite as

Shaull Almagor, Guy Avni, and Orna Kupferman. Repairing Multi-Player Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 325-339, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2015.325,
  author =	{Almagor, Shaull and Avni, Guy and Kupferman, Orna},
  title =	{{Repairing Multi-Player Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{325--339},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.325},
  URN =		{urn:nbn:de:0030-drops-53741},
  doi =		{10.4230/LIPIcs.CONCUR.2015.325},
  annote =	{Keywords: Nash equilibrium, concurrent games, repair}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact