Guy Avni

CSL Conference 2026 Conference Paper

Mean-Payoff and Energy Discrete-Bidding Games

• Guy Avni
• Suman Sadhukhan

A bidding game is played on a graph as follows. A token is placed on an initial vertex and both players are allocated budgets. In each turn, the 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 focus on discrete-bidding, which are motivated by practical applications and restrict the granularity of the players' bids, e. g, bids must be given in cents. We study, for the first time, discrete-bidding games with mean-payoff and energy objectives. In contrast, mean-payoff continuous-bidding games (i. e. , no granularity restrictions) are understood and exhibit a rich mathematical structure. The threshold budget is a necessary and sufficient initial budget for winning an energy game or guaranteeing a target payoff in a mean-payoff game. We first establish existence of threshold budgets; a non-trivial property due to the concurrent moves of the players. Moreover, we identify the structure of the thresholds, which is key in obtaining compact strategies, and in turn, showing that finding threshold is in NP and coNP even in succinctly-represented games.

Highlights Conference 2025 Conference Abstract

Analyzing the Interaction of Optimal Strategies in Mean-Payoff Bidding Games

• Guy Avni

AAMAS Conference 2025 Conference Paper

Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives

• Guy Avni
• Martin Kurecka
• Kaushik Mallik
• Petr Novotný
• Suman Sadhukhan

Graph games are fundamental in strategic reasoning of multi-agent systems and their environments. We study a new family of graph games which combine stochastic environmental uncertainties and auction-based interactions among the agents, formalized as bidding games on (finite) Markov decision processes (MDP). Normally, on MDPs, a single decision-maker chooses a sequence of actions, producing a probability distribution over infinite paths. In bidding games on MDPs, two players—called the reachability and safety players—bid for the privilege of choosing the next action at each step. The reachability player’s goal is to maximize the probability of reaching a given target vertex, whereas the safety player’s goal is to minimize it. These games generalize traditional bidding games on graphs, and the existing analysis techniques do not extend. For instance, the central property of bidding games on graphs is the existence of a threshold budget, which is the necessary and sufficient budget to guarantee winning for the reachability player. For MDPs, the threshold becomes a relation between budgets and probabilities of reaching the target. We devise value-iteration algorithms that approximate thresholds and optimal policies for general MDPs, and compute the exact solutions for acyclic MDPs, and show that finding thresholds is at least as hard as simple-stochastic games.

AAMAS Conference 2025 Conference Paper

Composing Reinforcement Learning Policies, with Formal Guarantees

• Florent Delgrange
• Guy Avni
• Anna Lukina
• Christian Schilling
• Ann Nowé
• Guillermo A. Pérez

We propose a novel framework to controller design in environments with a two-level structure: a known high-level graph (“map”) in which each vertex is populated by a Markov decision process, called a “room”. The framework “separates concerns” by using different design techniques for low- and high-level tasks. We apply reactive synthesis for high-level tasks: given a specification as a logical formula over the high-level graph and a collection of low-level policies obtained together with “concise” latent structures, we construct a “planner” that selects which low-level policy to apply in each room. We develop a reinforcement learning procedure to train low-level policies on latent structures, which unlike previous approaches, circumvents a model distillation step. We pair the policy with probably approximately correct guarantees on its performance and on the abstraction quality, and lift these guarantees to the high-level task. These formal guarantees are the main advantage of the framework. Other advantages include scalability (rooms are large and their dynamics are unknown) and reusability of low-level policies. We demonstrate feasibility in challenging case studies where an agent navigates environments with moving obstacles and visual inputs.

PRL Workshop 2025 Workshop Paper

Controller Synthesis from Deep Reinforcement Learning Policies

• Florent Delgrange
• Guy Avni
• Anna Lukina
• Christian Schilling
• Ann Nowe
• Guillermo Perez

We propose a novel framework to controller design in environments with a two-level structure: a known high-level graph (“map”) in which each vertex is populated by a Markov decision process, called a “room”. The framework “separates concerns” by using different design techniques for lowand high-level tasks. We apply reactive synthesis for highlevel tasks: given a specification as a logical formula over the high-level graph and a collection of low-level policies given on “concise” latent structures, we construct a “planner” that selects which low-level policy to apply in each room. We develop a reinforcement learning procedure to train lowlevel policies on latent structures, which unlike previous approaches, circumvents a model distillation step. It pairs the policy with probably approximately correct guarantees on its performance and abstraction quality, which are lifted to guarantees on the high-level task. These formal guarantees are the main advantage of the framework. Other advantages include scalability (rooms are large and their dynamics is unknown) and reusability of low-level policies. We demonstrate feasibility in challenging case studies involving agent navigation in environments with moving obstacles and visual inputs.

AAMAS Conference 2025 Conference Paper

Robin Hood Reachability Bidding Games

• Shaull Almagor
• Guy Avni
• Neta Dafni

Two-player graph games are a fundamental model for reasoning about the interaction of agents. These games are played between two players who move a token along a graph. In bidding games, the players have some monetary budget, and at each step they bid for the privilege of moving the token. Typically, the winner of the bid either pays the loser or the bank, or a combination thereof. We introduce Robin Hood bidding games, where at the beginning of every step the richer player pays the poorer a fixed fraction of the difference of their wealth. After the bid, the winner pays the loser. Intuitively, this captures the setting where a regulating entity prevents the accumulation of wealth to some degree. We show that the central property of bidding games, namely the existence of a threshold function, is retained in Robin Hood bidding games. We show that finding the threshold can be formulated as a Mixed-Integer Linear Program. Surprisingly, we show that the games are not always determined exactly at the threshold, unlike their standard counterpart.

AIJ Journal 2024 Journal Article

ASQ-IT: Interactive explanations for reinforcement-learning agents

• Yotam Amitai
• Ofra Amir
• Guy Avni

As reinforcement learning methods increasingly amass accomplishments, the need for comprehending their solutions becomes more crucial. Most explainable reinforcement learning (XRL) methods generate a static explanation depicting their developers' intuition of what should be explained and how. In contrast, literature from the social sciences proposes that meaningful explanations are structured as a dialog between the explainer and the explainee, suggesting a more active role for the user and her communication with the agent. In this paper, we present ASQ-IT – an interactive explanation system that presents video clips of the agent acting in its environment based on queries given by the user that describe temporal properties of behaviors of interest. Our approach is based on formal methods: queries in ASQ-IT's user interface map to a fragment of Linear Temporal Logic over finite traces (LTLf), which we developed, and our algorithm for query processing is based on automata theory. User studies show that end-users can understand and formulate queries in ASQ-IT and that using ASQ-IT assists users in identifying faulty agent behaviors.

EWRL Workshop 2024 Workshop Paper

Controller Synthesis from Deep Reinforcement Learning Policies

• Florent Delgrange
• Guy Avni
• Anna Lukina
• Christian Schilling
• Ann Nowe
• Guillermo Perez

We propose a novel framework to controller design in environments with a two-level structure: a high-level graph in which each vertex is populated by a Markov decision process, called a ``room'', with several low-level objectives. We proceed as follows. First, we apply deep reinforcement learning (DRL) to obtain low-level policies for each room and objective. Second, we apply reactive synthesis to obtain a planner that selects which low-level policy to apply in each room. Reactive synthesis refers to constructing a planner for a given model of the environment that satisfies a given objective (typically specified as a temporal logic formula) by design. The main advantage of the framework is formal guarantees. In addition, the framework enables a "separation of concerns": low-level tasks are addressed using DRL, which enables scaling to large rooms of unknown dynamics, reward engineering is only done locally, and policies can be reused, whereas users can specify high-level tasks intuitively and naturally. The central challenge in synthesis is the need for a model of the rooms. We address this challenge by developing a DRL procedure to train concise "latent" policies together with latent abstract rooms, both paired with PAC guarantees on performance and abstraction quality. Unlike previous approaches, this circumvents a model distillation step. We demonstrate feasibility in a case study involving agent navigation in an environment with moving obstacles.

AAAI Conference 2023 Conference Paper

Bidding Graph Games with Partially-Observable Budgets

• Guy Avni
• Ismael Jecker
• Đorđe Žikelić

Two-player zero-sum "graph games" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In "bidding games", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with "mean-payoff" objectives in combination with "poorman" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the "value" under pure strategies does not necessarily exist in such games.

ECAI Conference 2023 Conference Paper

Reachability Poorman Discrete-Bidding Games

• Guy Avni
• Tobias Meggendorfer
• Suman Sadhukhan
• Josef Tkadlec
• Dorde Zikelic

We consider bidding games, a class of two-player zero-sum graph games. The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token, where we break bidding ties in favor of Player 1. Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, poorman discrete-bidding in which the granularity of the bids is restricted and the higher bid is paid to the bank. Previous work either did not impose granularity restrictions or considered Richman bidding (bids are paid to the opponent). While the latter mechanisms are technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on threshold budgets, which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We first show existence of thresholds. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuous-bidding and that they exhibit a periodic behavior. We identify closed-form solutions in special cases. We implement and experiment with an algorithm to find threshold budgets.

I&C Journal 2023 Journal Article

Timed network games

• Guy Avni
• Shibashis Guha
• Orna Kupferman

Network games are widely used as a model for selfish resource-allocation problems. The classical model abstracts the fact that different users may use a resource at different times and for different duration – factors that play an important role in determining the costs of the users in reality. We consider here timed network games, which add time 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. 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 resetting some clocks. We also study the fragment of network games with a single clock that is not reset and thus keeps track only of the global time elapsed.

MFCS Conference 2022 Conference Paper

An Updated Survey of Bidding Games on Graphs (Invited Talk)

• Guy Avni
• Thomas A. Henzinger

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.

Highlights Conference 2022 Conference Abstract

Computing Threshold Budgets in Discrete-Bidding Games

• Guy Avni

In a two-player zero-sum graph game, the players move a token throughout the graph to produce a finite or infinite path, which determines the winner of the game. Bidding games are graph games in which the players have budgets, and in each turn, an auction determines which player moves the token. One characterisation of bidding games refers to the allowed bids: in continuous bidding, bids can be arbitrarily small, whereas in discrete bidding, the granularity of the bids is restricted. Discrete bidding is thus more appropriate for most practical applications. We focus on qualitative objectives. Both continuous- and discrete-bidding games are known to be determined, which in bidding games is captured by the concept of a threshold budget: roughly, a budget that is necessary and sufficient for a player to win the game from a given vertex. We study the complexity of computing the threshold budgets in discrete-bidding games. For reachability objectives, threshold budgets in continuous-bidding games satisfy an average property: the budget at a vertex is the average of two of its neighbours. Moreover, there is a unique function with the average property. Uniqueness immediately implies that the complexity of finding threshold budgets is in NP and coNP. Under discrete-bidding, threshold budgets are known to satisfy a discrete version of the average property. We show, somewhat surprisingly, that there can be more than one function satisfying the average property. This complicates the search for threshold budgets. We study, for the first, time, discrete-bidding games in which the sum of budgets is given in binary and show that finding threshold budgets is in NP and NP. Our algorithm uses a careful reduction to turn-based reachability games that is based on an intricate analysis of the optimal strategies of the players. We turn to parity and B{\"u}chi objectives. Under continuous bidding, parity bidding games reduce easily to reachability games. Under discrete-bidding, however, it was known that a key property of the reduction fails. We develop a fixed-point algorithm that takes a very different approach from the one in continuous-bidding games. The algorithm reveals the structure of threshold budgets in discrete-bidding games. We are currently working on employing this structure in order to show membership in NP and coNP. In the future, we expect that our techniques will be useful in studying other variants of discrete bidding games, e. g. mean-payoff games, which exhibit interesting properties under continuous bidding but have never been studied under discrete bidding. Joint work with Guy Avni.

Highlights Conference 2021 Conference Abstract

Bidding Graph Games with Partially-Observed Budgets

• Guy Avni

In a two-player zero-sum graph game, the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. {\em Bidding games} are graph games in which the players have budgets and in each turn, an auction determines which player moves the token. The motivation for this work arises from the potential of bidding games to model stateful and ongoing auctions. For example, online advertisement campaigns that run on multiple publishers (e. g. , New York Times or Washington Post) who auction their advertisement slots in an ongoing manner (e. g. , daily). Previously, bidding games were only studied as full-information games. In most auction domains, however, it is rarely the case that buyers have full information on the budgets of their opponents. We study, for the first time, bidding games in which the budgets of the players are drawn from a probability distribution, thus a player has only partial information on the opponent’s available budget. We stress that unlike partial-information graph games, we consider games in which there is full information regarding the position of the token. We study qualitative and quantitative objectives with the canonical bidding mechanisms. Our most interesting results are for {\em mean-payoff} games with {\em poorman} bidding: whenever a player wins a bidding, the bid is paid to the “bank”. Poorman bidding is interesting in the partial information setting since in the full-information setting, unlike other bidding mechanisms, the optimal payoff a player can guarantee in a mean-payoff poorman-bidding game is strictly increasing with the initial budget. We focus on the case of {\em one-sided} partial information, which is already both surprising and technically challenging. We classify the optimal expected payoff that the partially-informed player can guarantee with any initial budget in any strongly-connected game. In addition, we classify the optimal expected payoff that the fully-informed player can guarantee in a simple strongly-connected game, which reveals surprises. First, the optimal strategy of the fully-informed player reveals immediately her true initial budget. That is, the fully-informed player cannot use the partial information of her opponent to her advantage. Second, contrary to bidding, turn-based, and stochastic games, in partial-information {\em mean-payoff} bidding games the {\em value} does not necessarily exist under pure strategies: there are cases in which the optimal expected payoff that \Max can guarantee is strictly lower than the optimal payoff \Min can guarantee. Joint work with Isma\”el Jecker and {\DJ}or{\dj}e \v{Z}ikeli\’c.

SODA Conference 2021 Conference Paper

Infinite-Duration All-Pay Bidding Games

• Guy Avni
• Ismaël Jecker
• Dorde Zikelic

In a two-player zero-sum graph game the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In bidding games, however, the players have budgets, and in each turn, we hold an “auction” (bidding) to determine which player moves the token: both players simultaneously submit bids and the higher bidder moves the token. The bidding mechanisms differ in their payment schemes. Bidding games were largely studied with variants of first-price bidding in which only the higher bidder pays his bid. We focus on all-pay bidding, where both players pay their bids. Finite-duration all-pay bidding games were studied and shown to be technically more challenging than their first-price counterparts. We study for the first time, infinite-duration all-pay bidding games. Our most interesting results are for mean-payoff objectives: we portray a complete picture for games played on strongly-connected graphs. We study both pure (deterministic) and mixed (probabilistic) strategies and completely characterize the optimal and almost-sure (with probability 1) payoffs the players can respectively guarantee. We show that mean-payoff games under all-pay bidding exhibit the intriguing mathematical properties of their first-price counterparts; namely, an equivalence with random-turn games in which in each turn, the player who moves is selected according to a (biased) coin toss. The equivalences for all-pay bidding are more intricate and unexpected than for first-price bidding.

AAAI Conference 2020 Conference Paper

All-Pay Bidding Games on Graphs

• Guy Avni
• Rasmus Ibsen-Jensen
• Josef Tkadlec

In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve.

TCS Journal 2020 Journal Article

Dynamic resource allocation games

• Guy Avni
• Thomas A. Henzinger
• Orna Kupferman

In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.

Highlights Conference 2020 Conference Abstract

Infinite-Duration All-Pay Bidding Games

• Guy Avni

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”, in each turn, we hold an ‘auction’ (bidding) to determine which player moves the token. The players simultaneously submit bids and the higher bidder moves the token. Several different payment schemes have been considered. In “first-price” bidding, only the higher bidder pays his bid, while in “all-pay” bidding, both players pay their bids. Bidding games were largely studied with variants of first-price bidding. In this work, we study, for the first time, infinite-duration all-pay bidding games, and show that they exhibit elegant mathematical properties similar to their first-price counterparts; namely, an equivalence with “random-turn games”, which is a subclass of stochastic games. This is in stark contrast with reachability all-pay bidding games, which were recently shown to be technically much more complicated than reachability first-price bidding games. Another orthogonal distinction between the bidding rules is in the recipient of the payments: in “Richman” bidding, the bids are paid to the other player, and in “poorman” bidding, the bids are paid to the ‘bank’. We show a complete picture for the four bidding mechanisms. We focus on strongly-connected games. We first address Richman bidding. A simple argument shows that deterministic strategies cannot guarantee anything with this bidding mechanism. The main technical challenge is showing that with probabilistic strategies and mean-payoff objectives, the optimal expected payoff under all-pay bidding equals the optimal (deterministic) payoff under first-price bidding. We also construct almost-sure winning strategies for parity games. We find the properties of poorman bidding surprising in light of these results. First, in contrast to Richman bidding, deterministic strategies are useful and guarantee a payoff that is only slightly lower than the optimal payoff under first-price poorman bidding. This gives rise to winning strategies in parity games. Second, we show that under probabilistic strategies, the optimal expected payoff for the player with the larger budget is higher than the optimal payoff under first-price poorman bidding. Our proofs are constructive. In addition, for both Richman and poorman bidding we revisit the constructions for first-price bidding and significantly simplify them. Joint work with Ismael Jecker and Djordje Zikelic. The full version can be found online: https: //arxiv. org/abs/2005. 06636

MFCS Conference 2019 Conference Paper

Bidding Mechanisms in Graph Games

• Guy Avni
• Thomas A. Henzinger
• Dorde Zikelic

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.

Highlights Conference 2019 Conference Abstract

Formal Methods Meets Algorithmic Game Theory

• Guy Avni

Many problems in computer science, math, and economics can naturally be described as a game. As a result, various sub-fields in these disciplines study different types of games. The tutorial describes useful and interesting recent connections between formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems. The traditional games that are studied in formal methods are called graph games and they model the interaction between a reactive system and its hostile environment. These are typically ongoing two-player zero-sum games of infinite duration. On the other hand, AGT lies in the intersection between computer science and economics. The games studied in AGT are typically multi-player, non-zero-sum, and one-shot games. We will focus on two meeting points between the two fields. The first is “bidding games”, which are graph games in which in each turn, an auction is held in order to determine which player moves next. We study the effect of using different bidding mechanisms on the properties of the game, and reveal an intriguing connection between bidding games and a fragment of stochastic games called “random-turn games”. In the the second meeting point, we will focus on “network games” (sometimes called “congestion games”), and describe various ways of enriching studies of network games in the AGT community by practical considerations that are well-studied in the formal-method community. This includes, for example, network games with rich specifications, ones with real-time and ongoing behaviors, as well as algorithms for handling network games with huge state spaces.

Highlights Conference 2019 Conference Abstract

Formal Methods Meets Algorithmic Game Theory

• Guy Avni

Many problems in computer science, math, and economics can naturally be described as a game. As a result, various sub-fields in these disciplines study different types of games. The tutorial describes useful and interesting recent connections between formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems. The traditional games that are studied in formal methods are called graph games and they model the interaction between a reactive system and its hostile environment. These are typically ongoing two-player zero-sum games of infinite duration. On the other hand, AGT lies in the intersection between computer science and economics. The games studied in AGT are typically multi-player, non-zero-sum, and one-shot games. We will focus on two meeting points between the two fields. The first is “bidding games”, which are graph games in which in each turn, an auction is held in order to determine which player moves next. We study the effect of using different bidding mechanisms on the properties of the game, and reveal an intriguing connection between bidding games and a fragment of stochastic games called “random-turn games”. In the the second meeting point, we will focus on “network games” (sometimes called “congestion games”), and describe various ways of enriching studies of network games in the AGT community by practical considerations that are well-studied in the formal-method community. This includes, for example, network games with rich specifications, ones with real-time and ongoing behaviors, as well as algorithms for handling network games with huge state spaces.

TCS Journal 2018 Journal Article

Synthesis from component libraries with costs

• Guy Avni
• Orna Kupferman

Synthesis is the automated construction of a system from its specification. In real life, hardware and software systems are rarely constructed from scratch. Rather, a system is typically constructed from a library of components. Lustig and Vardi formalized this intuition and studied LTL synthesis from component libraries. In real life, designers seek optimal systems. In this paper we add optimality considerations to the setting. We distinguish between quality considerations (for example, size – the smaller a system is, the better it is), and pricing (for example, the payment to the company who manufactured the component). We study the problem of designing systems with minimal quality-cost and price. A key point is that while the quality cost is individual – the choices of a designer are independent of choices made by other designers that use the same library, pricing gives rise to a resource-allocation game – designers that use the same component share its price, with the share being proportional to the number of uses (a component can be used several times in a design). We study both closed and open settings, and in both we solve the problem of finding an optimal design. In a setting with multiple designers, we also study the game-theoretic problems of the induced resource-allocation game.

MFCS Conference 2018 Conference Paper

Timed Network Games with Clocks

• Guy Avni
• Shibashis Guha
• Orna Kupferman

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.

IJCAI Conference 2017 Conference Paper

An Abstraction-Refinement Methodology for Reasoning about Network Games

• Guy Avni
• Shibashis Guha
• Orna Kupferman

Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an over-approximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.

MFCS Conference 2017 Conference Paper

Timed Network Games

• Guy Avni
• Shibashis Guha
• Orna Kupferman

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.

TCS Journal 2016 Journal Article

Cost-sharing scheduling games on restricted unrelated machines

• Guy Avni
• Tami Tamir

We study a very general cost-sharing scheduling game. An instance consists of k jobs and m machines and an arbitrary weighted bipartite graph denoting the jobs strategies. An edge connecting a job and a machine specifies that the job may choose the machine; edge weights correspond to processing times. Each machine has an activation cost that needs to be covered by the jobs assigned to it. Jobs assigned to a particular machine share its cost proportionally to the load they generate. Our game generalizes singleton cost-sharing games with weighted players. We provide a complete analysis of the game with respect to equilibrium existence, computation, convergence and quality – with respect to the total cost and the maximal cost. We study both unilateral and coordinated deviations. We show that the main factor in determining the stability of an instance and the quality of a stable assignment is the machines' activation-cost. Games with unit-cost machines are generalized ordinal potential games, and every instance has an optimal solution which is also a pure Nash equilibrium (PNE). On the other hand, with arbitrary-cost machines, a PNE is guaranteed to exist only for very limited instances, and the price of stability is linear in the number of players. Also, the problem of deciding whether a given game instance has a PNE is NP-complete. In our analysis of coordinated deviations, we characterize instances for which a strong equilibrium exists and can be calculated efficiently, and show tight bounds for the strong price of anarchy and the price of stability.

I&C Journal 2016 Journal Article

Network-formation games with regular objectives

• Guy Avni
• Orna Kupferman
• Tami Tamir

Classical network-formation games are played on a directed graph. Players have reachability objectives: each player has to select a path from his source to target vertices. Each edge has a cost, shared evenly by the players using it. We introduce and study network-formation games with regular objectives. In our setting, the edges are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Unlike the case of reachability objectives, here the paths selected by the players need not be simple, thus a player may traverse some edges several times. Edge costs are shared by the players with the share being proportional to the number of times the edge is traversed. We study the existence of a pure Nash equilibrium (NE), the inefficiency of a NE compared to a social-optimum solution, and computational complexity problems in this setting.