Our work investigates the problem of instructing a Large Language Model (LLM) to navigate the vehicle to a specified goal and assesses its ability to generate low-level control actions that successfully guide the robot safely toward that goal. By leveraging historical data to construct reachable sets of states for the vehicle, our approach provides rigorous safety guarantees against unsafe behaviors without relying on explicit analytical models. This work advances the integration of formal methods into LLM-based robotics, offering a principled and practical approach to ensuring safety in next-generation autonomous systems.
Reference: Safe LLM-Controlled Robots with Formal Guarantees via Reachability Analysis
Videos: Video 1
Reachability analysis computes the set of reachable states of a model with uncertain initial states, inputs, and parameters. One major application of reachability analysis is the formal verification and controller synthesis of CPS. Most current reachability analysis heavily relies on the existence of a suitable system model, which is often not directly available in practice as systems are becoming more sophisticated. One often has an abundance of data but no model to perform reachability analysis. It is sometimes even easier to learn control policies directly from data rather than learning a model. Therefore, we aim to propose reachability analysis using data-driven approaches.
Reference: Data-Driven Reachability Analysis from Noisy Data
Reinforcement learning is capable of creating sophisticated controllers in uncertain environments. However, state-of-the-art reinforcement learning approaches lack safety guarantees, especially when the robot’s model and surrounding moving objects’ models are unknown. It is essential to ensure reasonable system performance and respect safety constraints during the process of learning policies that maximize the expectation and during deployment processes of reinforcement learning. We address this challenge by augmenting reinforcement learning with a safety layer that is based on formal data-driven verification techniques.
Reference: Safe Reinforcement Learning Using Black-Box Reachability Analysis
Videos: Video 1
A logical zonotope is constructed by XORing a binary point vector with a combination of binary vectors called generators. It can efficiently represent up to 2^n binary states of a logic-based system using only n generators. This can reduce the complexity of many exhaustive search algorithms by performing logical operations over the generators instead of iterating over the original binary vectors. Logical zonotopes are closed under XOR and NOT operations and yield over-approximations under AND and NAND operations. Since NAND is a universal gate operation, under the remaining operations, OR, NOR, and XNOR, logical zonotopes also yield over-approximations.
Reference: Logical Zonotope: A Set Representation for Binary Vectors
Representing 4 points using 2 generators.
We work on set-based estimation using partially homomorphic encryption that preserve the privacy of the measurements and sets bounding the estimates. We establish the notion of encrypted sets and intersect sets in the encrypted domain, which enables guaranteed state estimation while ensuring privacy. In particular, we show that our protocols achieve computational privacy by using the cryptographic notion of computational indistinguishability.
Reference: Privacy Preserving Set-Based Estimation Using Partially Homomorphic Encryption
The ability to perceive and comprehend a traffic situation and to predict the intent of vehicles and road users in the surroundings of the ego-vehicle is known as situational awareness. We work on a framework to improve situational awareness using set-membership estimation and vehicle-to-everything (V2X) communication. This framework provides safety guarantees, and can adapt to dynamically changing scenarios, and is integrated into an existing complex autonomous platform.
References:
Shared Situational Awareness with V2X Communication and Set-membership Estimation
A UAV snapshot for the Scania test Track