About

Suguman Bansal is an Assistant Professor in the School of Computer Science at Georgia Institute of Technology. Her research is focused on formal methods and their applications to artificial intelligence, programming languages, and machine learning. Previously, she was an NSF/CRA Computing Innovation Postdoctoral Fellow at the University of Pennsylvania, mentored by Prof. Rajeev Alur, and completed her Ph.D. at Rice University advised by Prof. Moshe Y. Vardi. She has received the 2020 NSF CI Fellowship, was named a 2021 MIT EECS Rising Star, and served as a keynote speaker at the 29th Static Analysis Symposium (SAS) in 2022.

Research topics

• Artificial Intelligence
• Computer Science
• Mathematics
• Mathematical optimization
• Theoretical computer science

Selected publications

• Specification-Guided Reinforcement Learning

  Communications of the ACM · 2026-01-28

  article

  A tutorial-style introduction to recent research on using logical specifications to encode RL tasks illustrates theoretical limitations and practical solutions.

  PublisherDOI

• INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition

  Lecture notes in computer science · 2025-01-01

  book-chapterOpen access1st authorCorresponding

  Abstract This paper presents a novel symbolic algorithm for the Maximal End Component (MEC) decomposition of a Markov Decision Process (MDP) . The key idea behind our algorithm is to interleave the computation of Strongly Connected Components (SCCs) with eager elimination of redundant state-action pairs, rather than performing these computations sequentially as done by existing state-of-the-art algorithms. Even though our approach has the same complexity as prior works, an empirical evaluation of on the standardized Quantitative Verification Benchmark Set demonstrates that it solves $$\textbf{19}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mn>19</mml:mn> </mml:math> more benchmarks (out of 368) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a $$\mathbf {3.81 \times }$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mn>3.81</mml:mn> <mml:mo>×</mml:mo> </mml:mrow> </mml:math> average speedup in runtime.

  PublisherOA PDFDOI

• Inductive Generalization in Reinforcement Learning from Specifications

  Lecture notes in computer science · 2025-10-25

  book-chapterSenior author
  PublisherDOI

• Decompositions in Compositional Translation of LTLf to DFA (Student Abstract)

  Proceedings of the AAAI Conference on Artificial Intelligence · 2024-03-24

  articleOpen accessSenior author

  Prior compositional methods in LTLf to DFA conversion have focussed on improving the composition phase. In this work, we examine improvements to the decomposition phase that result in overall improvements in LTLf to DFA translation. Our work is based on reducing the structure of the underlying Abstract Syntax Tree (AST) of a formula such that the new AST results in fewer composition operations.

  PublisherOA PDFDOI

• Inductive Generalization in Reinforcement Learning from Specifications

  arXiv (Cornell University) · 2024-06-05

  preprintOpen accessSenior author

  We present a novel inductive generalization framework for RL from logical specifications. Many interesting tasks in RL environments have a natural inductive structure. These inductive tasks have similar overarching goals but they differ inductively in low-level predicates and distributions. We present a generalization procedure that leverages this inductive relationship to learn a higher-order function, a policy generator, that generates appropriately adapted policies for instances of an inductive task in a zero-shot manner. An evaluation of the proposed approach on a set of challenging control benchmarks demonstrates the promise of our framework in generalizing to unseen policies for long-horizon tasks.

  PublisherOA PDFDOI

• Automata-Based Quantitative Reasoning

  ACM SIGLOG News · 2023-07-01

  article1st authorCorresponding

  Existing solution approaches for problems in formal quantitative analysis suffer from two challenges that adversely impact their theoretical understanding and large-scale applicability. These are the lack of generalizability , and separation-of-techniques. Lack of generalizability refers to the issue that solution approaches are often specialized to the underlying cost model that evaluates the quantitative property. Different cost models deploy such disparate algorithms that there is no transfer of knowledge from one cost model to another. Separation-of-techniques refers to the inherent dichotomy in solving problems in quantitative analysis. Most algorithms comprise of two phases: A structural phase , which reasons about the structure of the quantitative system(s) using techniques from automata or graphs; and a numerical phase , which reasons about the quantitative dimension/cost model using numerical methods. These techniques are incompatible with one another, forcing the phases to be performed sequentially, thereby impacting scalability. The article presents a novel framework that addresses the aforementioned challenges. The introduced framework, called comparator automata or comparators in short, builds on automata-theoretic foundations to generalize across a variety of cost models. The crux of comparators is that they enable automata-based methods in the numerical phase, hence eradicating the dependence on numerical methods. In doing so, comparators are able to integrate the structural and numerical phases. On the theoretical front, we demonstrate that comparator-based solutions have the advantage of generalizable results, and yield complexity-theoretic improvements over a range of problems in quantitative analysis. On the practical front, we demonstrate through empirical analysis that comparator-based solutions render more efficient, scalable, and robust performance, and demonstrate broader applicability than traditional methods for quantitative reasoning.

  PublisherDOI

• Compositional Safety LTL Synthesis

  Lecture notes in computer science · 2023-01-01 · 10 citations

  book-chapter1st author
  PublisherDOI

• Model Checking Strategies from Synthesis over Finite Traces

  Lecture notes in computer science · 2023-01-01 · 5 citations

  book-chapter1st authorCorresponding
  PublisherDOI

• Multi-Agent Systems with Quantitative Satisficing Goals

  arXiv (Cornell University) · 2023-05-01

  preprintOpen access

  In the study of reactive systems, qualitative properties are usually easier to model and analyze than quantitative properties. This is especially true in systems where mutually beneficial cooperation between agents is possible, such as multi-agent systems. The large number of possible payoffs available to agents in reactive systems with quantitative properties means that there are many scenarios in which agents deviate from mutually beneficial outcomes in order to gain negligible payoff improvements. This behavior often leads to less desirable outcomes for all agents involved. For this reason we study satisficing goals, derived from a decision-making approach aimed at meeting a good-enough outcome instead of pure optimization. By considering satisficing goals, we are able to employ efficient automata-based algorithms to find pure-strategy Nash equilibria. We then show that these algorithms extend to scenarios in which agents have multiple thresholds, providing an approximation of optimization while still retaining the possibility of mutually beneficial cooperation and efficient automata-based algorithms. Finally, we demonstrate a one-way correspondence between the existence of $ε$-equilibria and the existence of equilibria in games where agents have multiple thresholds.

  PublisherOA PDFDOI

• Multi-Agent Systems with Quantitative Satisficing Goals

  2023-08-01 · 2 citations

  articleOpen access

  In the study of reactive systems, qualitative properties are usually easier to model and analyze than quantitative properties. This is especially true in systems where mutually beneficial cooperation between agents is possible, such as multi-agent systems. The large number of possible payoffs available to agents in reactive systems with quantitative properties means that there are many scenarios in which agents deviate from mutually beneficial outcomes in order to gain negligible payoff improvements. This behavior often leads to less desirable outcomes for all agents involved. For this reason we study satisficing goals, derived from a decision-making approach aimed at meeting a good-enough outcome instead of pure optimization. By considering satisficing goals, we are able to employ efficient automata-based algorithms to find pure-strategy Nash equilibria. We then show that these algorithms extend to scenarios in which agents have multiple thresholds, providing an approximation of optimization while still retaining the possibility of mutually beneficial cooperation and efficient automata-based algorithms. Finally, we demonstrate a one-way correspondence between the existence of epsilon-equilibria and the existence of equilibria in games where agents have multiple thresholds.

  PublisherOA PDFDOI

Frequent coauthors

• Moshe Y. Vardi

  24 shared

• Rajeev Alur

  University of Pennsylvania

  15 shared

• Kishor Jothimurugan

  University of Pennsylvania

  13 shared

• Osbert Bastani

  California University of Pennsylvania

  13 shared

• Lucas M. Tabajara

  8 shared

• Gal Amram

  Tel Aviv University

  6 shared

• Swarat Chaudhuri

  6 shared

• Krishnendu Chatterjee

  Institute of Science and Technology Austria

  5 shared

Education

• PhD, Computer Science

  Rice University

  2020

• MSc, Computer Science

  Rice University

  2017

• BSc (Hons), Mathematics and Computer Science

  Chennai Mathematical Institute

  2014

Awards & honors

• 2020 NSF CI Fellowship
• 2021 MIT EECS Rising Star
• Keynote speaker at the 29th Static Analysis Symposium (SAS)…