Author name cluster

Shibashis Guha

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers

2 author rows

IJCAI Conference 2025 Conference Paper

Continuous-Time Reward Machines

Amin Falah
Shibashis Guha
Ashutosh Trivedi

Reinforcement Learning (RL) is a sampling-based method for sequential decision-making, in which a learning agent iteratively converges toward an optimal policy by leveraging feedback from the environment in the form of scalar reward signals. While timing information is often abstracted in discrete-time domains, time-critical learning applications—such as queuing systems, population processes, and manufacturing systems—are naturally modeled as Continuous-Time Markov Decision Processes (CTMDPs). Since the seminal work of Bradtke and Duff, model-free RL for CTMDPs has become well-understood. However, in many practical applications, practitioners possess high-quality information about system rates derived from traditional queuing theory, which learning agents could potentially exploit to accelerate convergence. Despite this, classical RL algorithms for CTMDPs typically re-learn these parameters through sampling. In this work, we propose continuous-time reward machines (CTRMs), a novel framework that embeds reward functions and real-time state-action dynamics into a unified structure. CTRMs enable RL agents to effectively navigate dense-time environments while leveraging reward shaping and counterfactual experiences for accelerated learning. Our empirical results demonstrate CTRMs' ability to improve learning efficiency in time-critical environments.

PDF Details DOI

AAMAS Conference 2025 Conference Paper

Optimising Expectation with Guarantees for Window Mean Payoff in Markov Decision Processes

Pranshu Gaba
Shibashis Guha

The window mean-payoff objective strengthens the classical meanpayoff objective by computing the mean-payoff over a finite window that slides along an infinite path. Two variants have been considered: in one variant, the maximum window length is fixed and given, while in the other, it is not fixed but is required to be bounded. In this paper, we look at the problem of synthesising strategies in Markov decision processes that maximise the window mean-payoff value in expectation, while also simultaneously guaranteeing that the value is above a certain threshold. We solve the synthesis problem for three different kinds of guarantees: sure (that needs to be satisfied in the worst-case, that is, for an adversarial environment), almost-sure (that needs to be satisfied with probability one), and probabilistic (that needs to be satisfied with at least some given probability 𝑝). We show that for the fixed window mean-payoff objective, when the window length is given in unary, all the three problems are in PTIME, while for the bounded window mean-payoff objective, they are in NP ∩ coNP, and thus have the same complexity as for maximising the expected performance without any guarantee. Moreover, we show that pure finite-memory strategies suffice for maximising the expectation with sure and almost-sure guarantees, whereas, for maximising expectation with a probabilistic guarantee, randomised strategies are necessary in general.

PDF

ICAPS Conference 2023 Conference Paper

Reinforcement Learning for Omega-Regular Specifications on Continuous-Time MDP

Amin Falah
Shibashis Guha
Ashutosh Trivedi 0001

Continuous-time Markov decision processes (CTMDPs) are canonical models to express sequential decision-making under dense-time and stochastic environments. When the stochastic evolution of the environment is only available via sampling, model-free reinforcement learning (RL) is the algorithm-of-choice to compute optimal decision sequence. RL, on the other hand, requires the learning objective to be encoded as scalar reward signals. Since doing such translations manually is both tedious and error-prone, a number of techniques have been proposed to translate high-level objectives (expressed in logic or automata formalism) to scalar rewards for discrete-time Markov decision processes. Unfortunately, no automatic translation exists for CTMDPs. We consider CTMDP environments against the learning objectives expressed as omega-regular languages. Omega-regular languages generalize regular languages to infinite-horizon specifications and can express properties given in popular linear-time logic LTL. To accommodate the dense-time nature of CTMDPs, we consider two different semantics of omega-regular objectives: 1) satisfaction semantics where the goal of the learner is to maximize the probability of spending positive time in the good states, and 2) expectation semantics where the goal of the learner is to optimize the long-run expected average time spent in the

Details

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.

Details DOI

Highlights Conference 2022 Conference Abstract

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

Shibashis Guha

Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the fundamental models for non-deterministic systems with probabilistic uncertainty. Mean payoff (a. k. a. long-run average reward) is one of the most classic objectives considered in their context. We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP; further, we extend it to unknown CTMDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability, which has been advocated in literature. In addition to providing PAC bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks. This is a joint work with Chaitanya Agarwal, Jan Křetínský, and M. Pazhamalai.

Details

MFCS Conference 2021 Conference Paper

A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct

Shibashis Guha
Ismaël Jecker
Karoliina Lehtinen
Martin Zimmermann 0002

We study the expressiveness and succinctness of good-for-games pushdown automata (GFG-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. We prove that GFG-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that GFG-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than GFG-PDA. We also study GFGness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show GFGness to be ExpTime-complete. GFG-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than GFG-VPA. Both of these lower bounds are tight. Finally, we study the complexity of resolving nondeterminism in GFG-PDA. Every GFG-PDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of GFG-VPA, but not those of GFG-PDA. GFG-PDA with finite-state resolvers are determinisable.

Details

Highlights Conference 2020 Conference Abstract

Stackelberg mean-payoff games with one epsilon-optimal adversarial follower

Shibashis Guha

Two-player Stackelberg games are non-zero sum strategic games comprising of a leader (Player 0) and a follower (Player 1). The leader announces her strategy, and the follower responds by playing an optimal response (or an epsilon-optimal response) to maximise his own payoff. The follower, while maximising his own payoff, can either be co-operative, that is, he chooses a response that maximises the payoff of the leader, or he can be adversarial, thus choosing a response that also minimises the payoff of the leader. In this work, we study Stackelberg games for two-player non-zero sum mean-payoff setting where the follower is adversarial and epsilon-optimal, for a fixed epsilon. The ASV-epsilon of Player 0 is the supremum of the values that Player 0 can obtain by announcing her strategy to Player 1 who in turn responds with an epsilon-optimal strategy. We prove that the ASV-epsilon is always achievable, possibly with an infinite memory strategy. This is in contrast with the framework of two-player Adversarial Stackelberg mean-payoff games where the epsilon is not fixed. We show that the threshold problem, i. e. given a rational constant c, deciding whether ASV-epsilon > c, is in NP, and a finite memory strategy for Player 0 suffices to achieve the threshold. We also give an EXPTime algorithm to compute the ASV-epsilon. Furthermore, we study the effect on ASV-epsilon when Player 0 is restricted to only finite memory strategies. Finally, we improve upon some of the results obtained earlier in the framework of two-player Adversarial Stackelberg mean-payoff games where the epsilon is not fixed. This is a joint work with Mrudula Balachander and Jean-François Raskin.

PDF Details

JAAMAS Journal 2019 Journal Article

Multi-player flow games

Shibashis Guha
Orna Kupferman
Gal Vardi

Abstract In the traditional maximum-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow to outgoing edges. The problem corresponds to settings in which a central authority has control on all vertices of the network. Today’s computing environment, however, involves systems with no central authority. In particular, in many applications of flow networks, the vertices correspond to decision-points controlled by different and selfish entities. For example, in communication networks, routers may belong to different companies, with different destination objectives. This suggests that the maximum-flow problem should be revisited, and examined from a game-theoretic perspective. We introduce and study multi-player flow games (MFGs, for short). Essentially, the vertices of an MFG are partitioned among the players, and a player that owns a vertex directs the flow that reaches it. Each player has a different target vertex, and the objective of each player is to maximize the flow that reaches her target vertex. We study the stability of MFGs and show that, unfortunately, an MFG need not have a Nash Equilibrium. Moreover, the price of anarchy and even the price of stability of MFGs are unbounded. That is, the reduction in the flow due to selfish behavior is unbounded. We study the problem of deciding whether a given MFG has a Nash Equilibrium and show that it is \(\Sigma _2^P\) -complete, as well as the problem of finding optimal strategies for the players (that is, best-response moves), which we show to be NP-complete. We continue with some good news and consider a variant of MFGs in which flow may be swallowed. For example, when routers in a communication network may drop messages. We show that, surprisingly, while this model seems to incentivize selfish behavior, a Nash Equilibrium that achieves the maximum flow always exists, and can be found in polynomial time. Finally, we consider MFGs in which the strategies of the players may use non-integral flows, which we show to be stronger.

Details DOI

AAMAS Conference 2018 Conference Paper

Multi-Player Flow Games

Shibashis Guha
Orna Kupferman
Gal Vardi

In the traditional maximum-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow to outgoing edges. The problem corresponds to settings in which a central authority has control on all vertices of the network. Today’s computing environment, however, involves systems with no central authority. In particular, in many applications of flow networks, the vertices correspond to decisionpoints controlled by different and selfish entities. For example, in communication networks, routers may belong to different companies, with different destination objectives. This suggests that the maximum-flow problem should be revisited, and examined from a game-theoretic perspective. We introduce and study multi-player flow games (MFGs, for short). Essentially, the vertices of an MFG are partitioned among the players, and a player that owns a vertex directs the flow that reaches it. Each player has a different target vertex, and the objective of each player is to maximize the flow that reaches her target vertex. We study the stability of MFGs and show that, unfortunately, an MFG need not have a Nash Equilibrium. Moreover, the Price of Anarchy and even the Price of Stability of MFGs are unbounded. That is, the reduction in the flow due to selfish behavior is unbounded. We study the problem of deciding whether a given MFG has a Nash Equilibrium and show that it is ΣP 2 -complete, as well as the problem of finding optimal strategies for the players (that is, best-response moves), which we show to be NP-complete. We continue with some good news and consider a variant of MFGs in which flow may be swallowed. For example, when routers in a communication network may drop messages. We show that, surprisingly, while this model seems to incentivize selfish behavior, a Nash Equilibrium that achieves the maximum flow always exists, and can be found in polynomial time. Finally, we consider MFGs in which the strategies of the players may use non-integral flows, which we show to be stronger.

PDF

Highlights Conference 2018 Conference Abstract

Safe and Optimal Scheduling of Hard and Soft Tasks

Shibashis Guha

ABSTRACT. We consider a stochastic scheduling problem with both hard and soft tasks. Each task is described by a discrete probability distribution over possible execution times, a deadline and a distribution over inter-arrival times. Our scheduling problem is \emph{non-clairvoyant} in the sense that the execution and inter-arrival times are subject to uncertainty modeled by stochastic distributions. Given an instance of our problem, we want to synthesize a schedule that is safe and efficient: safety imposes that deadline of hard tasks are never violated while efficient means that soft tasks should be completed as often as possible. To enforce that property, we impose a cost when a soft task deadline is violated and we are looking for a schedule that minimizes the expected value of the limit average of this cost. First, we show that the dynamics of such a system can be modeled as a finite Markov Decision Process (MDP). Second, we show that the problem of deciding the existence of a safe and efficient scheduler is PP-hard and in EXPTIME. Third, we have implemented our synthesis algorithm that partly relies on the probabilistic model-checker {\sc Storm} to analyze the underlying MDP. Given a set of both hard and soft tasks, we first compute the set of safe schedules, i. e. , the ones in which the hard tasks always finish their execution, then we compute the scheduler that minimizes the limit average cost among the set of all safe schedules. Finally, we compare the optimal solutions obtained with our procedure against an adaptation of the \emph{earliest deadline first} (EDF) algorithm to account for the soft task. We show that this EDF strategy can be arbitrarily worse in terms of the expected limit average cost for missing the deadlines of the soft tasks when compared to our optimal procedure.

Details

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.

Details

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.

PDF Details

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.

Details