Author name cluster

Suguman Bansal

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.

10 papers

2 author rows

AAAI Conference 2024 Short Paper

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

Yash Kankariya
Suguman Bansal

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.

PDF Details DOI

ICML Conference 2024 Conference Paper

Reinforcement Learning from Reachability Specifications: PAC Guarantees with Expected Conditional Distance

Jakub Svoboda
Suguman Bansal
Krishnendu Chatterjee

Reinforcement Learning (RL) from temporal logical specifications is a fundamental problem in sequential decision making. One of the basic and core such specification is the reachability specification that requires a target set to be eventually visited. Despite strong empirical results for RL from such specifications, the theoretical guarantees are bleak, including the impossibility of Probably Approximately Correct (PAC) guarantee for reachability specifications. Given the impossibility result, in this work we consider the problem of RL from reachability specifications along with the information of expected conditional distance (ECD). We present (a) lower bound results which establish the necessity of ECD information for PAC guarantees and (b) an algorithm that establishes PAC-guarantees given the ECD information. To the best of our knowledge, this is the first RL from reachability specifications that does not make any assumptions on the underlying environment to learn policies.

Details

Highlights Conference 2023 Conference Abstract

Model Checking Linear Temporal Logic over Finite Traces

Suguman Bansal

Recent years have witnessed a growing interest in reasoning about the finite-horizon counterpart of $\ltl$, called $\ltlf$, for systems of unbounded but finite horizons. While the problems of satisfiability and synthesis from $\ltlf$ specifications have been studied extensively, the verification problem has surprisingly been overlooked. To this end, this work presents the \emph{first} study of model-checking from $\ltlf$ specifications. We observe that there are striking differences between $\ltlf$ and $\ltl$ model checking. Most significantly, under the same non-terminating semantics of models, $\ltlf$ model checking is $\expspace$-complete, making it exponentially harder than $\ltl$ model checking. This is unexpected since one of the attributes behind the success of $\ltlf$ is that problems over $\ltlf$ have so far been {\em perceived} to be at most as hard as thoseon $\ltl$, if not easier. For instance, (a). reasoning about $\ltlf$ deals with automata over finite words whereas $\ltl$ requires automata over infinitewords, (b). the complexity of reactive synthesis and satisfiability from $\ltlf$ and $\ltl$ are identical, and so on. We also show that under \emph{terminating} semantics, $\ltlf$ model checking is \pspace-complete. Thus, demonstrating the importance of semantics in model checking for finite-horizon temporal specifications. Contributed talk given by Suguman Bansal

Details

IJCAI Conference 2023 Conference Paper

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

PDF Details DOI

PRL Workshop 2022 Workshop Paper

Compositional Reinforcement Learning from Logical Specifications

Kishor Jothimurugan
Suguman Bansal
Osbert Bastani
Rajeev Alur

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 specification and use a suitable reinforcement learning algorithm to learn a policy that maximizes the expected reward. These approaches, however, scale poorly to complex tasks that require high-level planning. In this work, we develop a compositional learning approach, called D I RL, that interleaves highlevel planning and reinforcement learning. First, D I RL encodes the specification as an abstract graph; intuitively, vertices and edges of the graph correspond to regions of the state space and simpler sub-tasks, respectively. Our approach then incorporates reinforcement learning to learn neural network policies for each edge (sub-task) within a Dijkstra-style planning algorithm to compute a high-level plan in the graph. An evaluation of the proposed approach on a set of challenging control benchmarks with continuous state and action spaces demonstrates that it outperforms state-of-the-art baselines.

PDF Details

AAAI Conference 2022 Conference Paper

Synthesis from Satisficing and Temporal Goals

Suguman Bansal
Lydia Kavraki
Moshe Y. Vardi
Andrew Wells

Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic (LTL) with soft constraints expressed by discounted-sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from LTL synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining LTL synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from LTL and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.

PDF Details

NeurIPS Conference 2021 Conference Paper

Compositional Reinforcement Learning from Logical Specifications

Kishor Jothimurugan
Suguman Bansal
Osbert Bastani
Rajeev Alur

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 specification and use a suitable reinforcement learning algorithm to learn a policy that maximizes the expected reward. These approaches, however, scale poorly to complex tasks that require high-level planning. In this work, we develop a compositional learning approach, called DIRL, that interleaves high-level planning and reinforcement learning. First, DIRL encodes the specification as an abstract graph; intuitively, vertices and edges of the graph correspond to regions of the state space and simpler sub-tasks, respectively. Our approach then incorporates reinforcement learning to learn neural network policies for each edge (sub-task) within a Dijkstra-style planning algorithm to compute a high-level plan in the graph. An evaluation of the proposed approach on a set of challenging control benchmarks with continuous state and action spaces demonstrates that it outperforms state-of-the-art baselines.

PDF Details

Highlights Conference 2021 Conference Abstract

Synthesis for Temporal and Satisficing Goals

Suguman Bansal

Reactive synthesis from high-level specifications that combine {\em hard} constraints expressed in Linear Temporal Logic ( ) with {\em soft} constraints expressed by discounted-sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.

Details

Highlights Conference 2020 Conference Abstract

Automata-Based Quantitative Reasoning

Suguman Bansal

Existing solution approaches for problems in {\em quantitative analysis} suffer from two challenges that adversely impact their theoretical understanding, and large-scale applicability due to limitations on scalability. These are the {\em lack of generalizability}, and {\em separation-of-techniques}. Lack of generalizability refers to the issue that solution approaches are often specialized to the underlying {\em 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 {\em structural phase}, which reasons about the structure of the quantitative system(s) using techniques from automata or graphs; and a {\em numerical phase}, which reasons about the quantitative dimension/cost model using numerical methods. The techniques used in both phases are so unlike each other that they are difficult to combine, forcing the phases to be performed sequentially, thereby impacting scalability. This abstract summarizes my thesis work~\cite{PhDThesis}, which contributes towards a novel framework that addresses the aforementioned challenges. The introduced framework, called {\em comparator automata} or {\em 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 hold the ability to integrate quantitative with qualitative objectives.

Details

AAAI Conference 2020 Conference Paper

Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

Suguman Bansal
Yong Li
Lucas Tabajara
Moshe Vardi

LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its ﬁnite-horizon behavior. So far, the conversion of LTLf formulas to deterministic ﬁnite-state automata (DFAs) has been identiﬁed as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well. Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent state-space explosion. Current conversion approaches, however, which are based either on explicit-state representation or symbolic-state representation, fail to address these necessities adequately at scale: Explicit-state approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolic-state representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blow-up. This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the state-space, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach.

PDF Details