arXiv subjects

Guy Avni

Publications and source records attributed to Guy Avni.

At least 19 recordsLinked to original sources

arXiv2026

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

A common assumption when designing an agent in a multi-agent system is that the other agents behave adversarially. This allows a designer to obtain the strongest guarantees when they have no control over nor knowledge about the other agents' behavior. However, when all agents are designed under this adversarial assumption, their actual interaction is not adversarial (e.g., when all players play defensively, no player actually attacks). In such settings, we would like to know what behavior arises in the multi-agent system. However, analyzing the interaction among agents is notoriously challenging, both mathematically and algorithmically. In this paper, we provide such an analysis, focusing on bidding games, played by two agents on a graph as follows. A token is placed on a vertex, and in each turn an auction (bidding) determines which agent moves the token, thus generating an infinite path that determines the agents' utilities. We consider mean-payoff objectives; each vertex is associated with a reward for each player, and the utility in an infinite play is the limit average of the rewards. We analyze the play that is generated when each agent follows a strategy that optimizes against an adversary, and consider the two known explicit constructions of optimal strategies. The technical challenge stems from the infinitely-many configurations of a bidding game and their complicated dynamics. We show that, under some restrictions, the generated play is ultimately periodic, and develop algorithms to compute the players' utilities in it.

cs.GT↗

arXiv2026

Multi-Player Discrete-Bidding Games; Determinacy, Equilibria, and Complexity

Games on graphs constitute a fundamental model. Applications include reactive synthesis, which reduces to solving a zero-sum two-player game, and reasoning about multi-agent systems by modeling them as a multi-player game. We study a class of graph games called bidding games in which the players are allocated a budget, and in each turn, an auction determines which player moves the token. Two-player bidding games have been extensively studied. We study, for the first time, multi-player bidding games. We focus on discrete bidding, which imposes granularity restrictions on the players' budgets and bids. The original motivation for discrete bidding is practical applications, and technically, it is appealing that the game has only finitely-many configurations. We initiate our study by considering a game between two coalitions of players. We show that under mild assumptions on the mechanism that is applied to break bidding ties, bidding games are determined: from every initial configuration, one of the coalitions has a winning strategy. Thus, we identify a sub-class of multi-player concurrent games that is determined. We extend the result to existence of a value in mean-payoff games. Using determinacy, we show that a pure Nash equilibrium always exists in qualitative games. Finally, we show that the complexity of deciding which coalition wins from a given configuration is PSPACE-hard already in reachability games and already for budgets given in unary. This is in stark contrast to two-player games, which are known to be in NP and coNP even for budgets given in binary.

cs.GT↗

arXiv2026

Decoupled Planning for Multiple Omega-Regular Objectives

We study the problem of generating paths on a graph that satisfy a collection of {\omega}-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler -- oblivious to the graph and objective -- dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions -- simple, a priori restrictions agreed upon before the graph or objectives are revealed -- that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of {\omega}-regular objectives. In particular, B\"uchi objectives admit universal composition of finite-memory policies without scheduler communication; co-B\"uchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.

cs.FL↗

arXiv2025

Mean-payoff and Energy Discrete Bidding Games

A \emph{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 \emph{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 {\em mean-payoff} and {\em energy} objectives. In contrast, mean-payoff {\em continuous}-bidding games (i.e., no granularity restrictions) are understood and exhibit a rich mathematical structure. The {\em 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.

cs.GT↗

arXiv2025

Interactive Explanations for Reinforcement-Learning Agents

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.

cs.AI↗

arXiv2024

Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives

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 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 traditional bidding games is the existence of a threshold budget, which is a necessary and sufficient budget to guarantee winning for the reachability player. For MDPs, the threshold becomes a relation between the 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 solving simple-stochastic games.

cs.GT↗

arXiv2024

Robin Hood Reachability Bidding Games

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.

cs.GT↗

arXiv2024

Bidding Games with Charging

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, and the winner is decided based on the infinite path 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 charges. Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. We show that 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?

cs.GT↗

arXiv2024

Composing Reinforcement Learning Policies, with Formal Guarantees

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.

cs.AI↗

arXiv2024

Auction-Based Scheduling

Many sequential decision-making tasks require satisfaction of multiple, partially contradictory objectives. Existing approaches are monolithic, namely all objectives are fulfilled using a single policy, which is a function that selects a sequence of actions. We present auction-based scheduling, a modular framework for multi-objective decision-making problems. Each objective is fulfilled using a separate policy, and the policies can be independently created, modified, and replaced. Understandably, different policies with conflicting goals may choose conflicting actions at a given time. In order to resolve conflicts, and compose policies, we employ a novel auction-based mechanism. We allocate a bounded budget to each policy, and at each step, the policies simultaneously bid from their available budgets for the privilege of being scheduled and choosing an action. Policies express their scheduling urgency using their bids and the bounded budgets ensure long-run scheduling fairness. We lay the foundations of auction-based scheduling using path planning problems on finite graphs with two temporal objectives. We present decentralized algorithms to synthesize a pair of policies, their initially allocated budgets, and bidding strategies. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other: (a) strong synthesis, with no assumptions and strongest guarantees, (b) assume-admissible synthesis, with weakest rationality assumptions, and (c) assume-guarantee synthesis, with explicit contract-based assumptions. For reachability objectives, we show that, surprisingly, decentralized assume-admissible synthesis is always possible when the out-degrees of all vertices are at most two.

cs.AI↗

arXiv2023

Dimension-Minimality and Primality of Counter Nets

A $k$-Counter Net ($k$-CN) is a finite-state automaton equipped with $k$ integer counters that are not allowed to become negative, but do not have explicit zero tests. This language-recognition model can be thought of as labelled vector addition systems with states, some of which are accepting. Certain decision problems for $k$-CNs become easier, or indeed decidable, when the dimension $k$ is small. Yet, little is known about the effect that the dimension $k$ has on the class of languages recognised by $k$-CNs. Specifically, it would be useful if we could simplify algorithmic reasoning by reducing the dimension of a given CN. To this end, we introduce the notion of dimension-primality for $k$-CN, whereby a $k$-CN is prime if it recognises a language that cannot be decomposed into a finite intersection of languages recognised by $d$-CNs, for some $d<k$. We show that primality is undecidable. We also study two related notions: dimension-minimality (where we seek a single language-equivalent $d$-CN of lower dimension) and language regularity. Additionally, we explore the trade-offs in expressiveness between dimension and non-determinism for CN.

cs.FL↗

arXiv2023

Reachability Poorman Discrete-Bidding Games

We consider {\em bidding games}, a class of two-player zero-sum {\em 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, {\em 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 {\em 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 {\em 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.

cs.GT↗

arXiv2023

Games on Graphs: From Logic and Automata to Algorithms

The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared in the study of automata and logic, and they later became important for program verification and synthesis. They have many more applications, in particular some of the models investigated in this book were introduced and studied in neighbouring research communities such as optimisation, reinforcement learning, model theory, and set theory.

cs.GT↗

arXiv2023

A Game of Pawns

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.

cs.GT↗

arXiv2023

ASQ-IT: Interactive Explanations for Reinforcement-Learning Agents

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 tool 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.

cs.AI↗

arXiv2022

Bidding Graph Games with Partially-Observable Budgets

Two-player zero-sum "graph games" are a central model, which proceeds as follows. A token is placed on a vertex of a graph, and the two players move it to produce an infinite "play", 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.

cs.GT↗

arXiv2022

Computing Threshold Budgets in Discrete-Bidding Games

In a two-player zero-sum graph game, the players move a token throughout a 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 (called Richman bidding). We focus on discrete-bidding games, in which, motivated by practical applications, the granularity of the players' bids is restricted, e.g., bids must be given in cents. A central quantity in bidding games is threshold budgets: a necessary and sufficient initial budget for winning the game. Previously, thresholds were shown to exist in parity games, but their structure was only understood for reachability games. Moreover, the previously-known algorithms have a worst-case exponential running time for both reachability and parity objectives, and output strategies that use exponential memory. We describe two algorithms for finding threshold budgets in parity discrete-bidding games. The first is a fixed-point algorithm. It reveals, for the first time, the structure of threshold budgets in parity discrete-bidding games. Based on this structure, we develop a second algorithm that shows that the problem of finding threshold budgets is in NP and coNP for both reachability and parity objectives. Moreover, our algorithm constructs strategies that use only linear memory. This is a corrected version of the paper (arXiv:2210.02773v4) published originally on Jan 22, 2025.

cs.FL↗

arXiv2021

Determinacy in Discrete-Bidding Infinite-Duration Games

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.

cs.GT↗