10 citations · 16 across the 18 of their papers we have counts for
20 papers
Certifying Almost-Sure Reachability in Unknown MDPs
S Akshay, Suguman Bansal, Gaurav Mahla
{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{learning} an optimal policy against a formal specification in an unknown {\em Markov…
Q-Learning for Reachability in MEC-Free MDPs
Lu-Chin Chang, Suguman Bansal
Reinforcement learning (RL) for reachability specifications is fundamental to sequential decision-making. Prior work establishes asymptotic convergence to optimal policies, but onl…
Certificate-Guided Evaluation of Reinforcement Learning Generalization
Vignesh Subramanian, Đorđe Žikelić, Suguman Bansal
This work presents a logic-driven framework to evaluate the performance of reinforcement learning (RL) algorithms in their ability to generalize to unseen tasks. Our framework defi…
Decoupled Behavioral Cloning for Scalable Inductive Generalization in RL from Specifications
Vignesh Subramanian, Subhajit Roy, Suguman Bansal
Inductive generalization is a framework for reinforcement learning (RL) generalization in which inductively related task instances admit inductively related policies. Prior work ca…
Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality
Amogh Palasamudram, Jakub Svoboda, Suguman Bansal +1
Reinforcement learning (RL) for reachability specifications is fundamental in sequential decision-making, yet theoretical guarantees remain less explored. A recent work achieves as…
INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
Suguman Bansal, Ramneet Singh
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 INTERLEAVE is…
Inductive Generalization in Reinforcement Learning from Specifications
Vignesh Subramanian, Rohit Kushwah, Subhajit Roy +1
We present a novel inductive generalization framework for RL from logical specifications. Many interesting tasks in RL environments have a natural inductive structure. These induct…
Multi-Agent Systems with Quantitative Satisficing Goals
Senthil Rajasekaran, Suguman Bansal, Moshe Y. Vardi
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 ben…
Model Checking Strategies from Synthesis Over Finite Traces
Suguman Bansal, Yong Li, Lucas Martinelli Tabajara +2
The innovations in reactive synthesis from {\em Linear Temporal Logics over finite traces} (LTLf) will be amplified by the ability to verify the correctness of the strategies gener…
Specification-Guided Learning of Nash Equilibria with High Social Welfare
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani +1
Reinforcement learning has been shown to be an effective strategy for automatically training policies for challenging control problems. Focusing on non-cooperative multi-agent syst…
Synthesis from Satisficing and Temporal Goals
Suguman Bansal, Lydia Kavraki, Moshe Y. Vardi +1
Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic LTL with soft constraints expressed by discounted-sum (DS) reward…
A Framework for Transforming Specifications in Reinforcement Learning
Rajeev Alur, Suguman Bansal, Osbert Bastani +1
Reactive synthesis algorithms allow automatic construction of policies to control an environment modeled as a Markov Decision Process (MDP) that are optimal with respect to high-le…
Compositional Reinforcement Learning from Logical Specifications
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani +1
We study the problem of learning control policies for complex tasks given by logical specifications. Recent approaches automatically generate a reward function from a given specifi…
Adapting Behaviors via Reactive Synthesis
Gal Amram, Suguman Bansal, Dror Fried +3
In the \emph{Adapter Design Pattern}, a programmer implements a \emph{Target} interface by constructing an \emph{Adapter} that accesses an existing \emph{Adaptee} code. In this wor…
On Satisficing in Quantitative Games
Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi
Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. {\em Optimization} is one form of analysis. We argue that…
Automata-based Quantitative Verification
Suguman Bansal
Quantitative analysis of computing systems is an emerging area in automated formal analysis. Such properties address aspects such as costs and rewards, quality measures, resource c…
Synthesis of coordination programs from linear temporal logic
Suguman Bansal, Kedar S. Namjoshi, Yaniv Sa'ar
This paper presents a method for synthesizing a reactive program which coordinates the actions of a group of other reactive programs, so that the combined system satisfies a tempor…
Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications
Suguman Bansal, Yong Li, Lucas M. Tabajara +1
LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf f…
Comparator automata in quantitative verification
Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
The notion of comparison between system runs is fundamental in formal verification. This concept is implicitly present in the verification of qualitative systems, and is more prono…
Equilibria in Quantitative Concurrent Games
Shaull Almagor, Rajeev Alur, Suguman Bansal
Synthesis of finite-state controllers from high-level specifications in multi-agent systems can be reduced to solving multi-player concurrent games over finite graphs. The complexi…