Curriculum Vitae
pranshu@pranshugaba.com pranshu.gaba@tifr.res.in dblp
Up to date as of ↓ Download CV as PDF
Research interests
General
formal methods,
game theory,
automata theory,
logic,
discrete mathematics
Specific
reactive synthesis,
verification,
probabilistic systems,
Markov decision processes
Education
PhD in Theoretical Computer Science, ongoing, synopsis submitted
Tata Institute of Fundamental Research, Mumbai, India
Advisor: Shibashis Guha
Thesis: Window mean-payoff in turn-based stochastic games
Relevant courses: Automata, verification, and infinite games; Descriptive complexity; Probability; Algebraic automata theory; Computational complexity; Algebra and computation; Online algorithms
Bachelor of Science (Research) with major in Mathematics, July 2020
Indian Institute of Science, Bangalore, India
Relevant courses: Automata theory and computability; Introduction to scalable systems; Game theory; Graph theory; Combinatorics; Number theory; Measure theory
Publications
- Expectation in Stochastic Games with Prefix-independent Objectiveswith Laurent Doyen and Shibashis Guha
Accepted in CONCUR 2025, full version at arXiv
Abstract
Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective.
We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP ∩ coUP when the window length is given in unary.
Presented atSeminar talk at MPI-SWS Kaiserslautern
CONCUR 2025
Workshop on Automata and Games for Synthesis (co-located with FSTTCS 2024)
- Optimising Expectation with Guarantees for Window Mean Payoff in Markov Decision Processeswith Shibashis Guha
Accepted in AAMAS 2025, full version at arXiv
Abstract
The window mean-payoff objective strengthens the classical mean-payoff 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 \(p\)).
We show that for fixed window mean-payoff objective, all the three problems are in PTIME, while for 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.
Presented atWorkshop on Automata and Games for Synthesis (co-located with FSTTCS 2025)
Seminar talk at Masaryk University, Brno
Seminar talk at IST Austria
Highlights 2025
Seminar talk at IIT Bombay
Formal Methods Update meeting 2025
- Recognizing numberswith Arnab Sur
Accepted in ICLA 2025 (best student paper award), full version at arXiv
Abstract
The use of monoids in the study of word languages recognized by finite-state automata has been quite fruitful. In this work, we look at the same idea of “recognizability by finite monoids” for other monoids. In particular, we attempt to characterize recognizable subsets of various additive and multiplicative monoids over integers, rationals, reals, and complex numbers. While these recognizable sets satisfy properties such as closure under Boolean operations and inverse morphisms, they do not enjoy many of the nice properties that recognizable word languages do.Presented atICLA 2025
TCS Research Expo 2024
STCS Student Symposium 2024
- Stochastic Window Mean-payoff Gameswith Laurent Doyen and Shibashis Guha
Accepted in FoSSaCS 2024, full version at LMCS
Abstract
Stochastic two-player games model systems with an environment that is both adversarial and stochastic. The environment is modelled by a player (Player 2) who tries to prevent the system (Player 1) from achieving its objective. We consider window mean-payoff objectives: these are finitary versions of the traditional mean-payoff objective, obtained by replacing the long-run average of the payoffs by average payoffs computed over a finite sliding window. We present complexity bounds and algorithmic solutions for computing strategies of Player 1 to ensure that the objective is satisfied with positive probability, with probability 1, or with probability at least \(p\), regardless of the strategy of Player 2. The solution crucially relies on a reduction to the special case of non-stochastic two-player games with the same objective. We also give a general characterisation of prefix-independent objectives for which this reduction holds.Presented atACM ARCS 2025
Seminar talk at ENS Paris-Saclay
FoSSaCS 2024
STCS Student Symposium 2023
Formal Methods Update Meeting 2023
- Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processeswith Shibashis Guha
Under submission, full version at arXiv
Abstract
Given rationals α and β, the sure-almost-sure problem for a quantitative objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e. sure α satisfaction) and with probability 1 the outcome has φ-value at least β (i.e. almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε>0 one can simultaneously ensure that all outcomes have φ-value at least α and with probability at least 1−ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this.
In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that the average payoff of a finite window that slides over an infinite run be greater than a given threshold. We study two variants of window mean payoff: in the fixed variant, the window length ℓ is given, while in the bounded variant, the length is not given but is required to be bounded throughout the run. We show that the sure-almost-sure problem and the sure-limit-sure problem are both in P for the fixed variant (if ℓ is given in unary) and are both in NP ∩ coNP for the bounded variant, matching the computational complexity of sure satisfaction and almost-sure satisfaction when considered separately for these objectives. We also give bounds for the memory requirement of winning strategies for all considered problems.
Other talks and presentations
Seminar talks
- The Canadian traveller problem
Abstract
Roads in Canada often get blocked due to excessive snowfall during blizzards. On encountering a road closure, a driver needs to adapt their route on-the-fly (possibly involving backtracking) in order to minimise the time taken to reach their destination. This problem is known as the Canadian traveller problem.
Formally, given a graph with partially observable edge weights, the goal is to synthesise a strategy that minimises the total weight of a walk to the target vertex, where an edge weight is only learnt on visiting an endpoint of the edge. We look at two different variants of this problem:
[PY91] The edge weights are chosen by an adversary. We want a strategy with the best competitive ratio, that is, one that minimises the ratio of the total weight of the walk taken to that of the total weight of the walk given by an optimal offline algorithm.
[KN07] The edge weights are given by a probability distribution. We want a strategy that minimises the expected total weight of a walk to the destination.
References:
PY91 Christos Papadimitriou and Mihalis Yannakakis, Shortest paths without a map (1991)
KN07 David Karger and Evdokia Nikolova, Exact Algorithms for the Canadian Traveller Problem on Paths and Trees (2007)
Talk details - Sperner’s lemma and the equidissection of regular polygons
Abstract
Equidissection of a regular polygon is the problem of dissecting the polygon into triangles of equal area. Given a regular \(n\)-gon and a positive integer \(m\), we ask if it is possible to equidissect the \(n\)-gon into \(m\) triangles. To answer this question, we make use of Sperner’s lemma along with some elementary number theory. Sperner’s lemma is a major combinatorial result that has found applications in topics such as fixed-point computation and fair division.
We shall see Sperner’s lemma and its proof, and use it to solve the equidissection problem for regular polygons. We will also look at some polygons that cannot be equidissected into \(m\) triangles for any positive \(m\). Finally, we will go over the equidissection problem for higher-dimensional hypercubes.
References:
- Monsky, P. (1970). On Dividing A Square Into Triangles. The American Mathematical Monthly, 77(2), 161–164. https://doi.org/10.1080/00029890.1970.11992441
- Stein, S. (2004). Cutting a Polygon into Triangles of Equal Areas. The Mathematical Intelligencer 26, 17–21. https://doi.org/10.1007/BF02985395
Talk details - The connection between circuit complexity and first-order logic
Abstract
Descriptive complexity is a branch of computational complexity where complexity classes are described using forms of logic, giving machine-independent characterizations of the complexity classes. In this talk, we look at an important result in descriptive complexity:
[BIS88, Theorem 8.1] A class of structures is in DLOGTIME-uniform AC0 if and only if the class is definable in first-order logic with numerical predicates.
Here, DLOGTIME is the class of languages accepted by a deterministic random-access Turing machine in logarithmic time. A language is said to be in DLOGTIME-uniform AC0 if it can be recognized by a family of constant-depth, polynomial-size circuits with AND and OR gates, where the circuits can be constructed by a DLOGTIME machine. The proof involves showing that if a language is in DLOGTIME, then it is definable in first-order logic with numerical predicates.
Reference:
[BIS88] David A. Mix-Barrington, Neil Immerman, and Howard Straubing. 1990. On uniformity within NC1. J. Comput. Syst. Sci. 41, 3 (Dec. 1990), 274–306. https://doi.org/10.1016/0022-0000(90)90022-D
Talk details - The complexity of solving simple stochastic games
Abstract
Simple stochastic games (SSG) are zero-sum games played by two players on a directed graph with a designated target vertex. The players take turns moving a token along the edges of the game graph. The objective of player 1 is to eventually reach the target vertex, whereas the objective of player 2 is to never reach the target vertex. The SSG problem is to find the maximum probability with which player 1 wins the game. We will see that this problem is in NP ∩ coNP. We will also see 3 more problems that are polynomial-time equivalent to SSG, and thus also in NP ∩ coNP. Showing that any of these problems are in P would be a major breakthrough.
You can read the following papers for more details.
The complexity of stochastic games, Anne Condon (1992) https://www.sciencedirect.com/science/article/pii/089054019290048K
The Complexity of Solving Stochastic Games on Graphs, Daniel Andersson & Peter Bro Miltersen (2009) https://link.springer.com/chapter/10.1007/978-3-642-10631-6_13
Talk details - Courcelle’s theorem
Abstract
Given a graph, we are often interested in deciding if it satisfies a certain property. Some examples of graph properties include connectivity, bipartiteness, and planarity. Courcelle’s theorem gives parameterized upper bounds for decidability for a wide class of graph properties. Specifically, Courcelle’s theorem is a metatheorem that states that if a graph property is definable in monadic second-order logic on graphs, then the property is decidable in linear fixed-parameter tractable time with the graph treewidth as the parameter. This theorem finds many uses in automata theory and model checking. We will study the theorem and look at some of its applications.
Talk details - Total-payoff games on graphs with windows
Abstract
We look at a two-player game played on a weighted directed graph. The game begins by placing a pawn on a vertex in the graph. The players then take turns moving the pawn to an adjacent vertex in the graph, yielding an infinite walk in the graph. Each time an edge is traversed, Player 1 receives a payoff equal to the weight of the edge. An objective that has been traditionally studied for such games is the total-payoff objective.
In this objective, Player 1 wins the game if the total payoff that they receive in the long run is non-negative, whereas Player 2 wins if the total-payoff is negative. A drawback of this objective is that Player 1 may win the game, and yet there may exist arbitrarily long stretches in the play in which the total-payoff is negative. This leads us to consider a stronger objective: window total-payoff. In this objective, Player 1 wins if from every point in the play, they can ensure that the total-payoff becomes non-negative in at most \(\ell\) steps. This objective gives stronger guarantees on the payoff received by Player 1 while at the same time being easier to compute. Computing the winning regions and winning strategies for the players for the traditional total-payoff objective is only known to be in NP ∩ coNP, whereas we see polynomial time algorithms to compute the same for the window total-payoff objective.
All results presented in this talk are from the paper “Looking at mean-payoff and total-payoff through windows” by Chatterjee, Doyen, Randour, and Raskin (2015).
Talk details - Determinacy of two-player games with perfect information
Abstract
A game with perfect information is a game in which no information is hidden from the players. All players know the rules and the state of the game at all times. Some examples of games with perfect information are Chess, Checkers, Go, and Nim. In two-player zero-sum games, a player has a winning strategy if they can always win no matter how the other player plays. A game is determined if one of the players has a winning strategy. Given a two-player game with perfect information, we would like to find out if it is determined.
In today’s talk, we discuss some results on two-player games with perfect information:
- We show that all finite games are determined.
- We construct an example of an infinite game that is not determined.
- We define a topology on infinite games. We use this to show the determinacy of some special classes of infinite games.
All results are from:
[1] “Theory of Games and Economic Behavior” by von Neumann and Morgenstern, 1947.
[2] “Infinite Games with Perfect Information” by Gale and Stewart, 1953.
Talk details - Vertex connectivity of Eulerian orientations
Abstract
A directed graph is said to be \(k\)-vertex-connected if after deleting any \(k-1\) vertices, there is a directed path from every vertex to every other vertex along the directed edges. An Eulerian orientation of a graph is an orientation such that every vertex has equal indegree and outdegree. Given an \(2k\)-regular graph \(G\), we would like to know if every Eulerian orientation of \(G\) is \(k\)-vertex connected. Horsch and Szigeti showed that this property holds for complete bipartite graphs, line graphs of regular complete bipartite graphs, incidence graphs of projective planes, but not for most complete graphs. In this talk, we will go through their proofs. We will also show that this property does not hold for most regular complete multipartite graphs.
Link to paper: https://doi.org/10.1016/j.dam.2020.09.022.
Talk details
Outreach sessions
- Sperner’s lemma and its application to rent divisionwith Malhar Managoli, Shanthanu Rai, and Aindrila RakshitPresented at
Chai and Why 2025
Vigyan Vidushi 2024
- Voting mechanisms: Let's put it to a votewith Ratnakar Medepalli and Shanthanu Rai
Abstract
Election season is here and with it, many questions. Do other countries have different systems from India? Which is the best? Is it always possible to determine a winner? Why do some people not vote for their favourite candidate? Does the shape of my constituency matter? Join us to explore questions in voting and social choice.Presented atChai and Why 2024
- Beating Chinese Whispers and other communication problemswith Eeshan Modak, Varun Ramanathan, and Ashutosh Shankar
Abstract
If you’ve played the game of Chinese Whispers you’ll know just how hard it can be to avoid errors in communication. How do modern communication networks transmit messages without errors? And do it efficiently and securely? Join us to explore the principles behind effective communication on computers, through some fun activities — chessboard puzzles, card tricks and more! No hard math needed (or the knowledge of chess or cards). If you enjoy solving puzzles, then this session is for you!Presented atChai and Why 2023
- Fun with graphswith Hari Krishnan P A and Ashutosh Shankar
Abstract
What do roads, friendships and even codes all have in common? All can be modelled using a graph: a network of vertices connected by edges. Join us as we explore some interesting puzzles related to networks!Presented atChai and Why 2022
- Impartial gameswith IISc Maths departmentPresented at
IISc Open Day 2020
Experience
Reviewing
FMCAD 2026, MathOR, ATVA 2025, EC 2025, CAV 2025, CSL 2025, STACS 2025, LICS 2024
Moderating
- Discussion on Open problems and challenges in Reactive Synthesis at IndiCS Seminar on Automated Synthesis 2025
- Panel discussion on Education and Careers in Logic (ECL) at ICLA 2025
Teaching assistance
- Automata and Computability at TIFR (January – May 2025)
Conferences attended
2025
- FSTTCS 2025 in BITS Pilani, Goa, India
- IndiCS Seminar on Automated Synthesis 2025, Mysore, India
- ATVA 2025 in IIIT Bangalore, India
- Highlights 2025 in Saarland University, Saarbrücken, Germany
- CONCUR 2025 in University of Aarhus, Denmark
- Formal Methods Update meeting 2025 in DAU, Gandhinagar, India
- ACM ARCS 2025 in PSG College of Technology, Coimbatore, India
- ICLA 2025 in ISI Kolkata, India
2024
- FSTTCS 2024 in IIT Gandhinagar, India
- Winter School on Verification 2024 in IIT Delhi, India
- SAT 2024 in TCS Pune, India
- ISLA 2024 in IIT Goa, India
- ETAPS 2024 in Luxembourg (student volunteer)
2023
- FSTTCS 2023 in IIIT Hyderabad, India
- Formal Methods Update meeting 2023 in IIT Goa, India
2022
- FSTTCS 2022 in IIT Madras, Chennai, India
- FLoC 2022 in Technion, Haifa, Israel (student volunteer)