15 citations · 61 across the 32 of their papers we have counts for
38 papers
MENTOR: Procedural Shielding of Tool-Using LLM Agents
Ashwani Anand, Ivi Chatzi, Ritam Raha +1
Tool-using LLM agents are increasingly used to automate workflows governed by procedural manuals, such as company rules for booking travel or procuring hardware. These manuals are…
Towards Actionable Strategy Certificates in Stochastic Parity Games
Christel Baier, Diane Cauquil, Calvin Chau +2
We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a singl…
Sound Probabilistic Safety Bounds for Large Language Models
Mahdi Nazeri, Anne-Kathrin Schmuck, Sadegh Soudjani +1
We propose a novel framework for computing rigorous bounds on the probability that a large language model (LLM) generates harmful output to a given prompt. We study a new applicati…
Context-Triggered Robust MPC for Temporal Logic Specifications
Arash Bahari Kordabad, Satya Prakash Nayak, Sadegh Soudjani +1
We consider the problem of synthesizing robust feedback controllers for discrete-time linear systems that ensure the satisfaction of context-dependent linear temporal logic specifi…
MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
Ashwani Anand, Ivi Chatzi, Ritam Raha +1
Tool-using large language model (LLM) agents are increasingly deployed in settings where their reliable behavior is governed by strict procedural manuals. Ensuring that such agents…
Concurrent Permissive Strategy Templates
Ashwani Anand, Christel Baier, Calvin Chau +4
Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semanti…
Context-Triggered Contingency Games for Strategic Multi-Agent Interaction
Kilian Schweppe, Anne-Kathrin Schmuck
We address the challenge of reliable and efficient interaction in autonomous multi-agent systems, where agents must balance long-term strategic objectives with short-term dynamic a…
Universal Safety Controllers with Learned Prophecies
Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak +1
\emph{Universal Safety Controllers (USCs)} are a promising logical control framework that guarantees the satisfaction of a given temporal safety specification when applied to any r…
Incremental Data-Driven Policy Synthesis via Game Abstractions
Irmak Sağlam, Mahdi Nazeri, Alessandro Abate +2
We address the synthesis of control policies for unknown discrete-time stochastic dynamical systems to satisfy temporal logic objectives. We present a data-driven, abstraction-base…
Maximal Adaptation, Minimal Guidance: Permissive Reactive Robot Task Planning with Humans in the Loop
Oz Gitelson, Satya Prakash Nayak, Ritam Raha +1
We present a novel framework for human-robot \emph{logical} interaction that enables robots to reliably satisfy (infinite horizon) temporal logic tasks while effectively collaborat…
Data-Driven Abstraction and Synthesis for Stochastic Systems with Unknown Dynamics
Mahdi Nazeri, Thom Badings, Anne-Kathrin Schmuck +2
We study the automated abstraction-based synthesis of correct-by-construction control policies for stochastic dynamical systems with unknown dynamics. Our approach is to learn an a…
Follow the STARs: Dynamic -Regular Shielding of Learned Policies
Ashwani Anand, Satya Prakash Nayak, Ritam Raha +1
This paper presents a novel dynamic post-shielding framework that enforces the full class of -regular correctness properties over pre-computed probabilistic policies. This const…
Quantitative Strategy Templates
Ashwani Anand, Satya Prakash Nayak, Ritam Raha +2
This paper presents (permissive) \emph{Quantitative Strategy Templates} (QaSTels) to succinctly represent infinitely many winning strategies in two-player energy and mean-payoff ga…
Synthesis of Universal Safety Controllers
Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak +1
The goal of logical controller synthesis is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic sp…
Fair Quantitative Games
Ashwani Anand, Satya Prakash Nayak, Ritam Raha +2
We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objec…
Localized Attractor Computations for Infinite-State Games (Full Version)
Anne-Kathrin Schmuck, Philippe Heim, Rayna Dimitrova +1
Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to constru…
Most General Winning Secure Equilibria Synthesis in Graph Games
Satya Prakash Nayak, Anne-Kathrin Schmuck
This paper considers the problem of co-synthesis in -player games over a finite graph where each player has an individual -regular specification . In this context, a sec…
Solving Two-Player Games under Progress Assumptions
Anne-Kathrin Schmuck, K. S. Thejaswini, Irmak Sağlam +1
This paper considers the problem of solving infinite two-player games over finite graphs under various classes of progress assumptions motivated by applications in cyber-physical s…
Doubly Fair Parity Games
Daniel Hausmann, Nir Piterman, Irmak Sağlam +1
We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph and a set of fa…
Contract-Based Distributed Synthesis in Two-Objective Parity Games
Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck
We present a novel method to compute in non-zerosum two-player games over finite graphs where each player has a different -regular winning…
Synthesizing Permissive Winning Strategy Templates for Parity Games
Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck
We present a novel method to compute \emph{permissive winning strategies} in two-player games over finite graphs with -regular winning conditions. Given a game graph and a…
Context-triggered Abstraction-based Control Design
Satya Prakash Nayak, Lucas Neves Egidio, Matteo Della Rossa +2
We consider the problem of automatically synthesizing a hybrid controller for non-linear dynamical systems which ensures that the closed-loop fulfills an arbitrary \emph{Linear Tem…
Computing Adequately Permissive Assumptions for Synthesis
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak +1
We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' ne…
Abstraction-Based Output-Feedback Control with State-Based Specifications
Anne-Kathrin Schmuck, Mehrdad Zareian
We consider abstraction-based design of output-feedback controllers for non-linear dynamical systems against specifications over state-based predicates in linear-time temporal logi…