-
Recursively Feasible Shrinking-Horizon MPC in Dynamic Environments with Conformal Prediction Guarantees
Authors:
Charis Stamouli,
Lars Lindemann,
George J. Pappas
Abstract:
In this paper, we focus on the problem of shrinking-horizon Model Predictive Control (MPC) in uncertain dynamic environments. We consider controlling a deterministic autonomous system that interacts with uncontrollable stochastic agents during its mission. Employing tools from conformal prediction, existing works derive high-confidence prediction regions for the unknown agent trajectories, and int…
▽ More
In this paper, we focus on the problem of shrinking-horizon Model Predictive Control (MPC) in uncertain dynamic environments. We consider controlling a deterministic autonomous system that interacts with uncontrollable stochastic agents during its mission. Employing tools from conformal prediction, existing works derive high-confidence prediction regions for the unknown agent trajectories, and integrate these regions in the design of suitable safety constraints for MPC. Despite guaranteeing probabilistic safety of the closed-loop trajectories, these constraints do not ensure feasibility of the respective MPC schemes for the entire duration of the mission. We propose a shrinking-horizon MPC that guarantees recursive feasibility via a gradual relaxation of the safety constraints as new prediction regions become available online. This relaxation enforces the safety constraints to hold over the least restrictive prediction region from the set of all available prediction regions. In a comparative case study with the state of the art, we empirically show that our approach results in tighter prediction regions and verify recursive feasibility of our MPC scheme.
△ Less
Submitted 17 May, 2024;
originally announced May 2024.
-
Probabilistic tube-based control synthesis of stochastic multi-agent systems under signal temporal logic
Authors:
Eleftherios E. Vlahakis,
Lars Lindemann,
Pantelis Sopasakis,
Dimos V. Dimarogonas
Abstract:
We consider the control design of stochastic discrete-time linear multi-agent systems (MASs) under a global signal temporal logic (STL) specification to be satisfied at a predefined probability. By decomposing the dynamics into deterministic and error components, we construct a probabilistic reachable tube (PRT) as the Cartesian product of reachable sets of the individual error systems driven by d…
▽ More
We consider the control design of stochastic discrete-time linear multi-agent systems (MASs) under a global signal temporal logic (STL) specification to be satisfied at a predefined probability. By decomposing the dynamics into deterministic and error components, we construct a probabilistic reachable tube (PRT) as the Cartesian product of reachable sets of the individual error systems driven by disturbances lying in confidence regions (CRs) with a fixed probability. By bounding the PRT probability with the specification probability, we tighten all state constraints induced by the STL specification by solving tractable optimization problems over segments of the PRT, and convert the underlying stochastic problem into a deterministic one. This approach reduces conservatism compared to tightening guided by the STL structure. Additionally, we propose a recursively feasible algorithm to attack the resulting problem by decomposing it into agent-level subproblems, which are solved iteratively according to a scheduling policy. We demonstrate our method on a ten-agent system, where existing approaches are impractical.
△ Less
Submitted 5 May, 2024;
originally announced May 2024.
-
Reactive Temporal Logic-based Planning and Control for Interactive Robotic Tasks
Authors:
Farhad Nawaz,
Shaoting Peng,
Lars Lindemann,
Nadia Figueroa,
Nikolai Matni
Abstract:
Robots interacting with humans must be safe, reactive and adapt online to unforeseen environmental and task changes. Achieving these requirements concurrently is a challenge as interactive planners lack formal safety guarantees, while safe motion planners lack flexibility to adapt. To tackle this, we propose a modular control architecture that generates both safe and reactive motion plans for huma…
▽ More
Robots interacting with humans must be safe, reactive and adapt online to unforeseen environmental and task changes. Achieving these requirements concurrently is a challenge as interactive planners lack formal safety guarantees, while safe motion planners lack flexibility to adapt. To tackle this, we propose a modular control architecture that generates both safe and reactive motion plans for human-robot interaction by integrating temporal logic-based discrete task level plans with continuous Dynamical System (DS)-based motion plans. We formulate a reactive temporal logic formula that enables users to define task specifications through structured language, and propose a planning algorithm at the task level that generates a sequence of desired robot behaviors while being adaptive to environmental changes. At the motion level, we incorporate control Lyapunov functions and control barrier functions to compute stable and safe continuous motion plans for two types of robot behaviors: (i) complex, possibly periodic motions given by autonomous DS and (ii) time-critical tasks specified by Signal Temporal Logic~(STL). Our methodology is demonstrated on the Franka robot arm performing wi** tasks on a whiteboard and a mannequin that is compliant to human interactions and adaptive to environmental changes.
△ Less
Submitted 30 April, 2024;
originally announced April 2024.
-
Robust STL Control Synthesis under Maximal Disturbance Sets
Authors:
Joris Verhagen,
Lars Lindemann,
Jana Tumova
Abstract:
This work addresses maximally robust control synthesis under unknown disturbances. We consider a general nonlinear system, subject to a Signal Temporal Logic (STL) specification, and wish to jointly synthesize the maximal possible disturbance bounds and the corresponding controllers that ensure the STL specification is satisfied under these bounds. Many works have considered STL satisfaction under…
▽ More
This work addresses maximally robust control synthesis under unknown disturbances. We consider a general nonlinear system, subject to a Signal Temporal Logic (STL) specification, and wish to jointly synthesize the maximal possible disturbance bounds and the corresponding controllers that ensure the STL specification is satisfied under these bounds. Many works have considered STL satisfaction under given bounded disturbances. Yet, to the authors' best knowledge, this is the first work that aims to maximize the permissible disturbance set and find the corresponding controllers that ensure satisfying the STL specification with maximum disturbance robustness. We extend the notion of disturbance-robust semantics for STL, which is a property of a specification, dynamical system, and controller, and provide an algorithm to get the maximal disturbance robust controllers satisfying an STL specification using Hamilton-Jacobi reachability. We show its soundness and provide a simulation example with an Autonomous Underwater Vehicle (AUV).
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
Risk-Aware Robotics: Tail Risk Measures in Planning, Control, and Verification
Authors:
Prithvi Akella,
Anushri Dixit,
Mohamadreza Ahmadi,
Lars Lindemann,
Margaret P. Chapman,
George J. Pappas,
Aaron D. Ames,
Joel W. Burdick
Abstract:
The need for a systematic approach to risk assessment has increased in recent years due to the ubiquity of autonomous systems that alter our day-to-day experiences and their need for safety, e.g., for self-driving vehicles, mobile service robots, and bipedal robots. These systems are expected to function safely in unpredictable environments and interact seamlessly with humans, whose behavior is no…
▽ More
The need for a systematic approach to risk assessment has increased in recent years due to the ubiquity of autonomous systems that alter our day-to-day experiences and their need for safety, e.g., for self-driving vehicles, mobile service robots, and bipedal robots. These systems are expected to function safely in unpredictable environments and interact seamlessly with humans, whose behavior is notably challenging to forecast. We present a survey of risk-aware methodologies for autonomous systems. We adopt a contemporary risk-aware approach to mitigate rare and detrimental outcomes by advocating the use of tail risk measures, a concept borrowed from financial literature. This survey will introduce these measures and explain their relevance in the context of robotic systems for planning, control, and verification applications.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Communication-Constrained STL Task Decomposition through Convex Optimization
Authors:
Gregorio Marchesini,
Siyuan Liu,
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
In this work, we propose a method to decompose signal temporal logic (STL) tasks for multi-agent systems subject to constraints imposed by the communication graph. Specifically, we propose to decompose tasks defined over multiple agents which require multi-hop communication, by a set of sub-tasks defined over the states of agents with 1-hop distance over the communication graph. To this end, we pa…
▽ More
In this work, we propose a method to decompose signal temporal logic (STL) tasks for multi-agent systems subject to constraints imposed by the communication graph. Specifically, we propose to decompose tasks defined over multiple agents which require multi-hop communication, by a set of sub-tasks defined over the states of agents with 1-hop distance over the communication graph. To this end, we parameterize the predicates of the tasks to be decomposed as suitable hyper-rectangles. Then, we show that by solving a constrained convex optimization, optimal parameters maximising the volume of the predicate's super-level sets can be computed for the decomposed tasks. In addition, we provide a formal definition of conflicting conjunctions of tasks for the considered STL fragment and a formal procedure to exclude such conjunctions from the solution set of possible decompositions. The proposed approach is demonstrated through simulations.
△ Less
Submitted 27 February, 2024;
originally announced February 2024.
-
Conformalized Adaptive Forecasting of Heterogeneous Trajectories
Authors:
Yanfei Zhou,
Lars Lindemann,
Matteo Sesia
Abstract:
This paper presents a new conformal method for generating simultaneous forecasting bands guaranteed to cover the entire path of a new random trajectory with sufficiently high probability. Prompted by the need for dependable uncertainty estimates in motion planning applications where the behavior of diverse objects may be more or less unpredictable, we blend different techniques from online conform…
▽ More
This paper presents a new conformal method for generating simultaneous forecasting bands guaranteed to cover the entire path of a new random trajectory with sufficiently high probability. Prompted by the need for dependable uncertainty estimates in motion planning applications where the behavior of diverse objects may be more or less unpredictable, we blend different techniques from online conformal prediction of single and multiple time series, as well as ideas for addressing heteroscedasticity in regression. This solution is both principled, providing precise finite-sample guarantees, and effective, often leading to more informative predictions than prior methods.
△ Less
Submitted 15 May, 2024; v1 submitted 14 February, 2024;
originally announced February 2024.
-
Conformal Predictive Programming for Chance Constrained Optimization
Authors:
Yiqi Zhao,
Xinyi Yu,
Jyotirmoy V. Deshmukh,
Lars Lindemann
Abstract:
Motivated by the advances in conformal prediction (CP), we propose conformal predictive programming (CPP), an approach to solve chance constrained optimization (CCO) problems, i.e., optimization problems with nonlinear constraint functions affected by arbitrary random parameters. CPP utilizes samples from these random parameters along with the quantile lemma -- which is central to CP -- to transfo…
▽ More
Motivated by the advances in conformal prediction (CP), we propose conformal predictive programming (CPP), an approach to solve chance constrained optimization (CCO) problems, i.e., optimization problems with nonlinear constraint functions affected by arbitrary random parameters. CPP utilizes samples from these random parameters along with the quantile lemma -- which is central to CP -- to transform the CCO problem into a deterministic optimization problem. We then present two tractable reformulations of CPP by: (1) writing the quantile as a linear program along with its KKT conditions (CPP-KKT), and (2) using mixed integer programming (CPP-MIP). CPP comes with marginal probabilistic feasibility guarantees for the CCO problem that are conceptually different from existing approaches, e.g., the sample approximation and the scenario approach. While we explore algorithmic similarities with the sample approximation approach, we emphasize that the strength of CPP is that it can easily be extended to incorporate different variants of CP. To illustrate this, we present robust conformal predictive programming to deal with distribution shifts in the uncertain parameters of the CCO problem.
△ Less
Submitted 11 February, 2024;
originally announced February 2024.
-
Low-Complexity Control for a Class of Uncertain MIMO Nonlinear Systems under Generalized Time-Varying Output Constraints
Authors:
Farhad Mehdifar,
Lars Lindemann,
Charalampos P. Bechlioulis,
Dimos V. Dimarogonas
Abstract:
This paper introduces a novel control framework to address the satisfaction of multiple time-varying output constraints in uncertain high-order MIMO nonlinear control systems. Unlike existing methods, which often assume that the constraints are always decoupled and feasible, our approach can handle coupled time-varying constraints even in the presence of potential infeasibilities. First, it is sho…
▽ More
This paper introduces a novel control framework to address the satisfaction of multiple time-varying output constraints in uncertain high-order MIMO nonlinear control systems. Unlike existing methods, which often assume that the constraints are always decoupled and feasible, our approach can handle coupled time-varying constraints even in the presence of potential infeasibilities. First, it is shown that satisfying multiple constraints essentially boils down to ensuring the positivity of a scalar variable, representing the signed distance from the boundary of the time-varying output-constrained set. To achieve this, a single consolidating constraint is designed that, when satisfied, guarantees convergence to and invariance of the time-varying output-constrained set within a user-defined finite time. Next, a novel robust and low-complexity feedback controller is proposed to ensure the satisfaction of the consolidating constraint. Additionally, we provide a mechanism for online modification of the consolidating constraint to find a least violating solution when the constraints become mutually infeasible for some time. Finally, simulation examples of trajectory and region tracking for a mobile robot validate the proposed approach.
△ Less
Submitted 13 January, 2024; v1 submitted 8 January, 2024;
originally announced January 2024.
-
Multi-Modal Conformal Prediction Regions with Simple Structures by Optimizing Convex Shape Templates
Authors:
Renukanandan Tumu,
Matthew Cleaveland,
Rahul Mangharam,
George J. Pappas,
Lars Lindemann
Abstract:
Conformal prediction is a statistical tool for producing prediction regions for machine learning models that are valid with high probability. A key component of conformal prediction algorithms is a \emph{non-conformity score function} that quantifies how different a model's prediction is from the unknown ground truth value. Essentially, these functions determine the shape and the size of the confo…
▽ More
Conformal prediction is a statistical tool for producing prediction regions for machine learning models that are valid with high probability. A key component of conformal prediction algorithms is a \emph{non-conformity score function} that quantifies how different a model's prediction is from the unknown ground truth value. Essentially, these functions determine the shape and the size of the conformal prediction regions. While prior work has gone into creating score functions that produce multi-model prediction regions, such regions are generally too complex for use in downstream planning and control problems. We propose a method that optimizes parameterized \emph{shape template functions} over calibration data, which results in non-conformity score functions that produce prediction regions with minimum volume. Our approach results in prediction regions that are \emph{multi-modal}, so they can properly capture residuals of distributions that have multiple modes, and \emph{practical}, so each region is convex and can be easily incorporated into downstream tasks, such as a motion planner using conformal prediction regions. Our method applies to general supervised learning tasks, while we illustrate its use in time-series prediction. We provide a toolbox and present illustrative case studies of F16 fighter jets and autonomous vehicles, showing an up to $68\%$ reduction in prediction region area compared to a circular baseline region.
△ Less
Submitted 25 June, 2024; v1 submitted 12 December, 2023;
originally announced December 2023.
-
Signal Temporal Logic Control Synthesis among Uncontrollable Dynamic Agents with Conformal Prediction
Authors:
Xinyi Yu,
Yiqi Zhao,
Xiang Yin,
Lars Lindemann
Abstract:
The control of dynamical systems under temporal logic specifications among uncontrollable dynamic agents is challenging due to the agents' a-priori unknown behavior. Existing works have considered the problem where either all agents are controllable, the agent models are deterministic and known, or no safety guarantees are provided. We propose a predictive control synthesis framework that guarante…
▽ More
The control of dynamical systems under temporal logic specifications among uncontrollable dynamic agents is challenging due to the agents' a-priori unknown behavior. Existing works have considered the problem where either all agents are controllable, the agent models are deterministic and known, or no safety guarantees are provided. We propose a predictive control synthesis framework that guarantees, with high probability, the satisfaction of signal temporal logic (STL) tasks that are defined over the system and uncontrollable stochastic agents. We use trajectory predictors and conformal prediction to construct probabilistic prediction regions for each uncontrollable agent that are valid over multiple future time steps. Specifically, we reduce conservatism and increase data efficiency compared to existing works by constructing a normalized prediction region over all agents and time steps. We then formulate a worst-case mixed integer program (MIP) that accounts for all agent realizations within the prediction region to obtain control inputs that provably guarantee task satisfaction with high probability. To efficiently solve this MIP, we propose an equivalent MIP program based on KKT conditions of the original one. We illustrate our control synthesis framework on two case studies.
△ Less
Submitted 7 December, 2023;
originally announced December 2023.
-
Sleep When Everything Looks Fine: Self-Triggered Monitoring for Signal Temporal Logic Tasks
Authors:
Chuwei Wang,
Xinyi Yu,
Jianing Zhao,
Lars Lindemann,
Xiang Yin
Abstract:
Online monitoring is a widely used technique in assessing if the performance of the system satisfies some desired requirements during run-time operation. Existing works on online monitoring usually assume that the monitor can acquire system information periodically at each time instant. However, such a periodic mechanism may be unnecessarily energy-consuming as it essentially requires to turn on s…
▽ More
Online monitoring is a widely used technique in assessing if the performance of the system satisfies some desired requirements during run-time operation. Existing works on online monitoring usually assume that the monitor can acquire system information periodically at each time instant. However, such a periodic mechanism may be unnecessarily energy-consuming as it essentially requires to turn on sensors consistently. In this paper, we proposed a novel self-triggered mechanism for model-based online monitoring of discrete-time dynamical system under specifications described by signal temporal logic (STL) formulae. Specifically, instead of sampling the system state at each time instant, a self-triggered monitor can actively determine when the next system state is sampled in addition to its monitoring decision regarding the satisfaction of the task. We propose an effective algorithm for synthesizing such a self-triggered monitor that can correctly evaluate a given STL formula on-the-fly while maximizing the time interval between two observations. We show that, compared with the standard online monitor with periodic information, the proposed self-triggered monitor can significantly reduce observation burden while ensuring that no information of the STL formula is lost. Case studies are provided to illustrate the proposed monitoring mechanism.
△ Less
Submitted 26 November, 2023;
originally announced November 2023.
-
Robust Conformal Prediction for STL Runtime Verification under Distribution Shift
Authors:
Yiqi Zhao,
Bardh Hoxha,
Georgios Fainekos,
Jyotirmoy V. Deshmukh,
Lars Lindemann
Abstract:
Cyber-physical systems (CPS) designed in simulators behave differently in the real-world. Once they are deployed in the real-world, we would hence like to predict system failures during runtime. We propose robust predictive runtime verification (RPRV) algorithms under signal temporal logic (STL) tasks for general stochastic CPS. The RPRV problem faces several challenges: (1) there may not be suffi…
▽ More
Cyber-physical systems (CPS) designed in simulators behave differently in the real-world. Once they are deployed in the real-world, we would hence like to predict system failures during runtime. We propose robust predictive runtime verification (RPRV) algorithms under signal temporal logic (STL) tasks for general stochastic CPS. The RPRV problem faces several challenges: (1) there may not be sufficient data of the behavior of the deployed CPS, (2) predictive models are based on a distribution over system trajectories encountered during the design phase, i.e., there may be a distribution shift during deployment. To address these challenges, we assume to know an upper bound on the statistical distance (in terms of an f-divergence) between the distributions at deployment and design time, and we utilize techniques based on robust conformal prediction. Motivated by our results in [1], we construct an accurate and an interpretable RPRV algorithm. We use a trajectory prediction model to estimate the system behavior at runtime and robust conformal prediction to obtain probabilistic guarantees by accounting for distribution shifts. We precisely quantify the relationship between calibration data, desired confidence, and permissible distribution shift. To the best of our knowledge, these are the first statistically valid algorithms under distribution shift in this setting. We empirically validate our algorithms on a Franka manipulator within the NVIDIA Isaac sim environment.
△ Less
Submitted 9 March, 2024; v1 submitted 15 November, 2023;
originally announced November 2023.
-
Distributed Sequential Receding Horizon Control of Multi-Agent Systems under Recurring Signal Temporal Logic
Authors:
Eleftherios E. Vlahakis,
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
We consider the synthesis problem of a multi-agent system under signal temporal logic (STL) specifications representing bounded-time tasks that need to be satisfied recurrently over an infinite horizon. Motivated by the limited approaches to handling recurring STL systematically, we tackle the infinite-horizon control problem with a receding horizon scheme equipped with additional STL constraints…
▽ More
We consider the synthesis problem of a multi-agent system under signal temporal logic (STL) specifications representing bounded-time tasks that need to be satisfied recurrently over an infinite horizon. Motivated by the limited approaches to handling recurring STL systematically, we tackle the infinite-horizon control problem with a receding horizon scheme equipped with additional STL constraints that introduce minimal complexity and a backward-reachability-based terminal condition that is straightforward to construct and ensures recursive feasibility. Subsequently, we decompose the global receding horizon optimization problem into agent-level programs the objectives of which are to minimize local cost functions subject to local and joint STL constraints. We propose a scheduling policy that allows individual agents to sequentially optimize their control actions while maintaining recursive feasibility. This results in a distributed strategy that can operate online as a model predictive controller. Last, we illustrate the effectiveness of our method via a multi-agent system example assigned a surveillance task.
△ Less
Submitted 26 April, 2024; v1 submitted 12 November, 2023;
originally announced November 2023.
-
Temporally Robust Multi-Agent STL Motion Planning in Continuous Time
Authors:
Joris Verhagen,
Lars Lindemann,
Jana Tumova
Abstract:
Signal Temporal Logic (STL) is a formal language over continuous-time signals (such as trajectories of a multi-agent system) that allows for the specification of complex spatial and temporal system requirements (such as staying sufficiently close to each other within certain time intervals). To promote robustness in multi-agent motion planning with such complex requirements, we consider motion pla…
▽ More
Signal Temporal Logic (STL) is a formal language over continuous-time signals (such as trajectories of a multi-agent system) that allows for the specification of complex spatial and temporal system requirements (such as staying sufficiently close to each other within certain time intervals). To promote robustness in multi-agent motion planning with such complex requirements, we consider motion planning with the goal of maximizing the temporal robustness of their joint STL specification, i.e. maximizing the permissible time shifts of each agent's trajectory while still satisfying the STL specification. Previous methods presented temporally robust motion planning and control in a discrete-time Mixed Integer Linear Programming (MILP) optimization scheme. In contrast, we parameterize the trajectory by continuous Bézier curves, where the curvature and the time-traversal of the trajectory are parameterized individually. We show an algorithm generating continuous-time temporally robust trajectories and prove soundness of our approach. Moreover, we empirically show that our parametrization realizes this with a considerable speed-up compared to state-of-the-art methods based on constant interval time discretization.
△ Less
Submitted 16 October, 2023;
originally announced October 2023.
-
Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference
Authors:
Navid Hashemi,
Xin Qin,
Lars Lindemann,
Jyotirmoy V. Deshmukh
Abstract:
We consider data-driven reachability analysis of discrete-time stochastic dynamical systems using conformal inference. We assume that we are not provided with a symbolic representation of the stochastic system, but instead have access to a dataset of $K$-step trajectories. The reachability problem is to construct a probabilistic flowpipe such that the probability that a $K$-step trajectory can vio…
▽ More
We consider data-driven reachability analysis of discrete-time stochastic dynamical systems using conformal inference. We assume that we are not provided with a symbolic representation of the stochastic system, but instead have access to a dataset of $K$-step trajectories. The reachability problem is to construct a probabilistic flowpipe such that the probability that a $K$-step trajectory can violate the bounds of the flowpipe does not exceed a user-specified failure probability threshold. The key ideas in this paper are: (1) to learn a surrogate predictor model from data, (2) to perform reachability analysis using the surrogate model, and (3) to quantify the surrogate model's incurred error using conformal inference in order to give probabilistic reachability guarantees. We focus on learning-enabled control systems with complex closed-loop dynamics that are difficult to model symbolically, but where state transition pairs can be queried, e.g., using a simulator. We demonstrate the applicability of our method on examples from the domain of learning-enabled cyber-physical systems.
△ Less
Submitted 17 September, 2023;
originally announced September 2023.
-
Conformance Testing for Stochastic Cyber-Physical Systems
Authors:
Xin Qin,
Navid Hashemi,
Lars Lindemann,
Jyotirmoy V. Deshmukh
Abstract:
Conformance is defined as a measure of distance between the behaviors of two dynamical systems. The notion of conformance can accelerate system design when models of varying fidelities are available on which analysis and control design can be done more efficiently. Ultimately, conformance can capture distance between design models and their real implementations and thus aid in robust system design…
▽ More
Conformance is defined as a measure of distance between the behaviors of two dynamical systems. The notion of conformance can accelerate system design when models of varying fidelities are available on which analysis and control design can be done more efficiently. Ultimately, conformance can capture distance between design models and their real implementations and thus aid in robust system design. In this paper, we are interested in the conformance of stochastic dynamical systems. We argue that probabilistic reasoning over the distribution of distances between model trajectories is a good measure for stochastic conformance. Additionally, we propose the non-conformance risk to reason about the risk of stochastic systems not being conformant. We show that both notions have the desirable transference property, meaning that conformant systems satisfy similar system specifications, i.e., if the first model satisfies a desirable specification, the second model will satisfy (nearly) the same specification. Lastly, we propose how stochastic conformance and the non-conformance risk can be estimated from data using statistical tools such as conformal prediction. We present empirical evaluations of our method on an F-16 aircraft, an autonomous vehicle, a spacecraft, and Dubin's vehicle.
△ Less
Submitted 12 August, 2023;
originally announced August 2023.
-
Efficient STL Control Synthesis under Asynchronous Temporal Robustness Constraints
Authors:
Xinyi Yu,
Xiang Yin,
Lars Lindemann
Abstract:
In time-critical systems, such as air traffic control systems, it is crucial to design control policies that are robust to timing uncertainty. Recently, the notion of Asynchronous Temporal Robustness (ATR) was proposed to capture the robustness of a system trajectory against individual time shifts in its sub-trajectories. In a multi-robot system, this may correspond to individual robots being dela…
▽ More
In time-critical systems, such as air traffic control systems, it is crucial to design control policies that are robust to timing uncertainty. Recently, the notion of Asynchronous Temporal Robustness (ATR) was proposed to capture the robustness of a system trajectory against individual time shifts in its sub-trajectories. In a multi-robot system, this may correspond to individual robots being delayed or early. Control synthesis under ATR constraints is challenging and has not yet been addressed. In this paper, we propose an efficient control synthesis method under ATR constraints which are defined with respect to simple safety or complex signal temporal logic specifications. Given an ATR bound, we compute a sequence of control inputs so that the specification is satisfied by the system as long as each sub-trajectory is shifted not more than the ATR bound. We avoid combinatorially exploring all shifted sub-trajectories by first identifying redundancy between them. We capture this insight by the notion of instant-shift pair sets, and then propose an optimization program that enforces the specification only over the instant-shift pair sets. We show soundness and completeness of our method and analyze its computational complexity. Finally, we present various illustrative case studies.
△ Less
Submitted 24 July, 2023;
originally announced July 2023.
-
Control of Nonlinear Systems Under Multiple Time-Varying Output Constraints: A Single Funnel Approach
Authors:
Farhad Mehdifar,
Lars Lindemann,
Charalampos P. Bechlioulis,
Dimos V. Dimarogonas
Abstract:
This paper proposes a novel control framework for handling (potentially coupled) multiple time-varying output constraints for uncertain nonlinear systems. First, it is shown that the satisfaction of multiple output constraints boils down to ensuring the positiveness of a scalar variable (the signed distance from the time-varying output-constrained set's boundary). Next, a single funnel constraint…
▽ More
This paper proposes a novel control framework for handling (potentially coupled) multiple time-varying output constraints for uncertain nonlinear systems. First, it is shown that the satisfaction of multiple output constraints boils down to ensuring the positiveness of a scalar variable (the signed distance from the time-varying output-constrained set's boundary). Next, a single funnel constraint is designed properly, whose satisfaction ensures convergence to and invariance of the time-varying output-constrained set. Then a robust and low-complexity funnel-based feedback controller is designed employing the prescribed performance control method. Finally, a simulation example clarifies and verifies the proposed approach.
△ Less
Submitted 11 August, 2023; v1 submitted 12 July, 2023;
originally announced July 2023.
-
Combined Left and Right Temporal Robustness for Control under STL Specifications
Authors:
Alëna Rodionova,
Lars Lindemann,
Manfred Morari,
George J. Pappas
Abstract:
Many modern autonomous systems, particularly multi-agent systems, are time-critical and need to be robust against timing uncertainties. Previous works have studied left and right time robustness of signal temporal logic specifications by considering time shifts in the predicates that are either only to the left or only to the right. We propose a combined notion of temporal robustness which simulta…
▽ More
Many modern autonomous systems, particularly multi-agent systems, are time-critical and need to be robust against timing uncertainties. Previous works have studied left and right time robustness of signal temporal logic specifications by considering time shifts in the predicates that are either only to the left or only to the right. We propose a combined notion of temporal robustness which simultaneously considers left and right time shifts. For instance, in a scenario where a robot plans a trajectory around a pedestrian, this combined notion can now capture uncertainty of the pedestrian arriving earlier or later than anticipated. We first derive desirable properties of this new notion with respect to left and right time shifts and then design control laws for linear systems that maximize temporal robustness using mixed-integer linear programming. Finally, we present two case studies to illustrate how the proposed temporal robustness accounts for timing uncertainties.
△ Less
Submitted 8 June, 2023;
originally announced June 2023.
-
Conformal Predictive Safety Filter for RL Controllers in Dynamic Environments
Authors:
Kegan J. Strawn,
Nora Ayanian,
Lars Lindemann
Abstract:
The interest in using reinforcement learning (RL) controllers in safety-critical applications such as robot navigation around pedestrians motivates the development of additional safety mechanisms. Running RL-enabled systems among uncertain dynamic agents may result in high counts of collisions and failures to reach the goal. The system could be safer if the pre-trained RL policy was uncertainty-in…
▽ More
The interest in using reinforcement learning (RL) controllers in safety-critical applications such as robot navigation around pedestrians motivates the development of additional safety mechanisms. Running RL-enabled systems among uncertain dynamic agents may result in high counts of collisions and failures to reach the goal. The system could be safer if the pre-trained RL policy was uncertainty-informed. For that reason, we propose conformal predictive safety filters that: 1) predict the other agents' trajectories, 2) use statistical techniques to provide uncertainty intervals around these predictions, and 3) learn an additional safety filter that closely follows the RL controller but avoids the uncertainty intervals. We use conformal prediction to learn uncertainty-informed predictive safety filters, which make no assumptions about the agents' distribution. The framework is modular and outperforms the existing controllers in simulation. We demonstrate our approach with multiple experiments in a collision avoidance gym environment and show that our approach minimizes the number of collisions without making overly-conservative predictions.
△ Less
Submitted 22 August, 2023; v1 submitted 4 June, 2023;
originally announced June 2023.
-
Conformal Prediction Regions for Time Series using Linear Complementarity Programming
Authors:
Matthew Cleaveland,
Insup Lee,
George J. Pappas,
Lars Lindemann
Abstract:
Conformal prediction is a statistical tool for producing prediction regions of machine learning models that are valid with high probability. However, applying conformal prediction to time series data leads to conservative prediction regions. In fact, to obtain prediction regions over $T$ time steps with confidence $1-δ$, {previous works require that each individual prediction region is valid} with…
▽ More
Conformal prediction is a statistical tool for producing prediction regions of machine learning models that are valid with high probability. However, applying conformal prediction to time series data leads to conservative prediction regions. In fact, to obtain prediction regions over $T$ time steps with confidence $1-δ$, {previous works require that each individual prediction region is valid} with confidence $1-δ/T$. We propose an optimization-based method for reducing this conservatism to enable long horizon planning and verification when using learning-enabled time series predictors. Instead of considering prediction errors individually at each time step, we consider a parameterized prediction error over multiple time steps. By optimizing the parameters over an additional dataset, we find prediction regions that are not conservative. We show that this problem can be cast as a mixed integer linear complementarity program (MILCP), which we then relax into a linear complementarity program (LCP). Additionally, we prove that the relaxed LP has the same optimal cost as the original MILCP. Finally, we demonstrate the efficacy of our method on case studies using pedestrian trajectory predictors and F16 fighter jet altitude predictors.
△ Less
Submitted 8 January, 2024; v1 submitted 3 April, 2023;
originally announced April 2023.
-
Safe Perception-Based Control under Stochastic Sensor Uncertainty using Conformal Prediction
Authors:
Shuo Yang,
George J. Pappas,
Rahul Mangharam,
Lars Lindemann
Abstract:
We consider perception-based control using state estimates that are obtained from high-dimensional sensor measurements via learning-enabled perception maps. However, these perception maps are not perfect and result in state estimation errors that can lead to unsafe system behavior. Stochastic sensor noise can make matters worse and result in estimation errors that follow unknown distributions. We…
▽ More
We consider perception-based control using state estimates that are obtained from high-dimensional sensor measurements via learning-enabled perception maps. However, these perception maps are not perfect and result in state estimation errors that can lead to unsafe system behavior. Stochastic sensor noise can make matters worse and result in estimation errors that follow unknown distributions. We propose a perception-based control framework that i) quantifies estimation uncertainty of perception maps, and ii) integrates these uncertainty representations into the control design. To do so, we use conformal prediction to compute valid state estimation regions, which are sets that contain the unknown state with high probability. We then devise a sampled-data controller for continuous-time systems based on the notion of measurement robust control barrier functions. Our controller uses idea from self-triggered control and enables us to avoid using stochastic calculus. Our framework is agnostic to the choice of the perception map, independent of the noise distribution, and to the best of our knowledge the first to provide probabilistic safety guarantees in such a setting. We demonstrate the effectiveness of our proposed perception-based controller for a LiDAR-enabled F1/10th car.
△ Less
Submitted 25 August, 2023; v1 submitted 31 March, 2023;
originally announced April 2023.
-
Physics Constrained Motion Prediction with Uncertainty Quantification
Authors:
Renukanandan Tumu,
Lars Lindemann,
Truong Nghiem,
Rahul Mangharam
Abstract:
Predicting the motion of dynamic agents is a critical task for guaranteeing the safety of autonomous systems. A particular challenge is that motion prediction algorithms should obey dynamics constraints and quantify prediction uncertainty as a measure of confidence. We present a physics-constrained approach for motion prediction which uses a surrogate dynamical model to ensure that predicted traje…
▽ More
Predicting the motion of dynamic agents is a critical task for guaranteeing the safety of autonomous systems. A particular challenge is that motion prediction algorithms should obey dynamics constraints and quantify prediction uncertainty as a measure of confidence. We present a physics-constrained approach for motion prediction which uses a surrogate dynamical model to ensure that predicted trajectories are dynamically feasible. We propose a two-step integration consisting of intent and trajectory prediction subject to dynamics constraints. We also construct prediction regions that quantify uncertainty and are tailored for autonomous driving by using conformal prediction, a popular statistical tool. Physics Constrained Motion Prediction achieves a 41% better ADE, 56% better FDE, and 19% better IoU over a baseline in experiments using an autonomous racing dataset.
△ Less
Submitted 23 May, 2023; v1 submitted 2 February, 2023;
originally announced February 2023.
-
Leveraging Contextual Relatedness to Identify Suicide Documentation in Clinical Notes through Zero Shot Learning
Authors:
Terri Elizabeth Workman,
Joseph L. Goulet,
Cynthia A. Brandt,
Allison R. Warren,
Jacob Eleazer,
Melissa Skanderson,
Luke Lindemann,
John R. Blosnich,
John O Leary,
Qing Zeng Treitler
Abstract:
Identifying suicidality including suicidal ideation, attempts, and risk factors in electronic health record data in clinical notes is difficult. A major difficulty is the lack of training samples given the small number of true positive instances among the increasingly large number of patients being screened. This paper describes a novel methodology that identifies suicidality in clinical notes by…
▽ More
Identifying suicidality including suicidal ideation, attempts, and risk factors in electronic health record data in clinical notes is difficult. A major difficulty is the lack of training samples given the small number of true positive instances among the increasingly large number of patients being screened. This paper describes a novel methodology that identifies suicidality in clinical notes by addressing this data sparsity issue through zero-shot learning. U.S. Veterans Affairs clinical notes served as data. The training dataset label was determined using diagnostic codes of suicide attempt and self-harm. A base string associated with the target label of suicidality was used to provide auxiliary information by narrowing the positive training cases to those containing the base string. A deep neural network was trained by map** the training documents contents to a semantic space. For comparison, we trained another deep neural network using the identical training dataset labels and bag-of-words features. The zero shot learning model outperformed the baseline model in terms of AUC, sensitivity, specificity, and positive predictive value at multiple probability thresholds. In applying a 0.90 probability threshold, the methodology identified notes not associated with a relevant ICD 10 CM code that documented suicidality, with 94 percent accuracy. This new method can effectively identify suicidality without requiring manual annotation.
△ Less
Submitted 9 January, 2023;
originally announced January 2023.
-
Adaptive Conformal Prediction for Motion Planning among Dynamic Agents
Authors:
Anushri Dixit,
Lars Lindemann,
Skylar Wei,
Matthew Cleaveland,
George J. Pappas,
Joel W. Burdick
Abstract:
This paper proposes an algorithm for motion planning among dynamic agents using adaptive conformal prediction. We consider a deterministic control system and use trajectory predictors to predict the dynamic agents' future motion, which is assumed to follow an unknown distribution. We then leverage ideas from adaptive conformal prediction to dynamically quantify prediction uncertainty from an onlin…
▽ More
This paper proposes an algorithm for motion planning among dynamic agents using adaptive conformal prediction. We consider a deterministic control system and use trajectory predictors to predict the dynamic agents' future motion, which is assumed to follow an unknown distribution. We then leverage ideas from adaptive conformal prediction to dynamically quantify prediction uncertainty from an online data stream. Particularly, we provide an online algorithm uses delayed agent observations to obtain uncertainty sets for multistep-ahead predictions with probabilistic coverage. These uncertainty sets are used within a model predictive controller to safely navigate among dynamic agents. While most existing data-driven prediction approached quantify prediction uncertainty heuristically, we quantify the true prediction uncertainty in a distribution-free, adaptive manner that even allows to capture changes in prediction quality and the agents' motion. We empirically evaluate of our algorithm on a simulation case studies where a drone avoids a flying frisbee.
△ Less
Submitted 30 November, 2022;
originally announced December 2022.
-
Conformal Prediction for STL Runtime Verification
Authors:
Lars Lindemann,
Xin Qin,
Jyotirmoy V. Deshmukh,
George J. Pappas
Abstract:
We are interested in predicting failures of cyber-physical systems during their operation. Particularly, we consider stochastic systems and signal temporal logic specifications, and we want to calculate the probability that the current system trajectory violates the specification. The paper presents two predictive runtime verification algorithms that predict future system states from the current o…
▽ More
We are interested in predicting failures of cyber-physical systems during their operation. Particularly, we consider stochastic systems and signal temporal logic specifications, and we want to calculate the probability that the current system trajectory violates the specification. The paper presents two predictive runtime verification algorithms that predict future system states from the current observed system trajectory. As these predictions may not be accurate, we construct prediction regions that quantify prediction uncertainty by using conformal prediction, a statistical tool for uncertainty quantification. Our first algorithm directly constructs a prediction region for the satisfaction measure of the specification so that we can predict specification violations with a desired confidence. The second algorithm constructs prediction regions for future system states first, and uses these to obtain a prediction region for the satisfaction measure. To the best of our knowledge, these are the first formal guarantees for a predictive runtime verification algorithm that applies to widely used trajectory predictors such as RNNs and LSTMs, while being computationally simple and making no assumptions on the underlying distribution. We present numerical experiments of an F-16 aircraft and a self-driving car.
△ Less
Submitted 10 March, 2023; v1 submitted 2 November, 2022;
originally announced November 2022.
-
Safe Planning in Dynamic Environments using Conformal Prediction
Authors:
Lars Lindemann,
Matthew Cleaveland,
Gihyun Shim,
George J. Pappas
Abstract:
We propose a framework for planning in unknown dynamic environments with probabilistic safety guarantees using conformal prediction. Particularly, we design a model predictive controller (MPC) that uses i) trajectory predictions of the dynamic environment, and ii) prediction regions quantifying the uncertainty of the predictions. To obtain prediction regions, we use conformal prediction, a statist…
▽ More
We propose a framework for planning in unknown dynamic environments with probabilistic safety guarantees using conformal prediction. Particularly, we design a model predictive controller (MPC) that uses i) trajectory predictions of the dynamic environment, and ii) prediction regions quantifying the uncertainty of the predictions. To obtain prediction regions, we use conformal prediction, a statistical tool for uncertainty quantification, that requires availability of offline trajectory data - a reasonable assumption in many applications such as autonomous driving. The prediction regions are valid, i.e., they hold with a user-defined probability, so that the MPC is provably safe. We illustrate the results in the self-driving car simulator CARLA at a pedestrian-filled intersection. The strength of our approach is compatibility with state of the art trajectory predictors, e.g., RNNs and LSTMs, while making no assumptions on the underlying trajectory-generating distribution. To the best of our knowledge, these are the first results that provide valid safety guarantees in such a setting.
△ Less
Submitted 8 June, 2023; v1 submitted 18 October, 2022;
originally announced October 2022.
-
Risk Verification of Stochastic Systems with Neural Network Controllers
Authors:
Matthew Cleaveland,
Lars Lindemann,
Radoslav Ivanov,
George Pappas
Abstract:
Motivated by the fragility of neural network (NN) controllers in safety-critical applications, we present a data-driven framework for verifying the risk of stochastic dynamical systems with NN controllers. Given a stochastic control system, an NN controller, and a specification equipped with a notion of trace robustness (e.g., constraint functions or signal temporal logic), we collect trajectories…
▽ More
Motivated by the fragility of neural network (NN) controllers in safety-critical applications, we present a data-driven framework for verifying the risk of stochastic dynamical systems with NN controllers. Given a stochastic control system, an NN controller, and a specification equipped with a notion of trace robustness (e.g., constraint functions or signal temporal logic), we collect trajectories from the system that may or may not satisfy the specification. In particular, each of the trajectories produces a robustness value that indicates how well (severely) the specification is satisfied (violated). We then compute risk metrics over these robustness values to estimate the risk that the NN controller will not satisfy the specification. We are further interested in quantifying the difference in risk between two systems, and we show how the risk estimated from a nominal system can provide an upper bound the risk of a perturbed version of the system. In particular, the tightness of this bound depends on the closeness of the systems in terms of the closeness of their system trajectories. For Lipschitz continuous and incrementally input-to-state stable systems, we show how to exactly quantify system closeness with varying degrees of conservatism, while we estimate system closeness for more general systems from data in our experiments. We demonstrate our risk verification approach on two case studies, an underwater vehicle and an F1/10 autonomous car.
△ Less
Submitted 10 November, 2022; v1 submitted 26 August, 2022;
originally announced September 2022.
-
Chordal Sparsity for SDP-based Neural Network Verification
Authors:
Anton Xue,
Lars Lindemann,
Rajeev Alur
Abstract:
Neural networks are central to many emerging technologies, but verifying their correctness remains a major challenge. It is known that network outputs can be sensitive and fragile to even small input perturbations, thereby increasing the risk of unpredictable and undesirable behavior. Fast and accurate verification of neural networks is therefore critical to their widespread adoption, and in recen…
▽ More
Neural networks are central to many emerging technologies, but verifying their correctness remains a major challenge. It is known that network outputs can be sensitive and fragile to even small input perturbations, thereby increasing the risk of unpredictable and undesirable behavior. Fast and accurate verification of neural networks is therefore critical to their widespread adoption, and in recent years, various methods have been developed as a response to this problem. In this paper, we focus on improving semidefinite programming (SDP) based techniques for neural network verification. Such techniques offer the power of expressing complex geometric constraints while retaining a convex problem formulation, but scalability remains a major issue in practice. Our starting point is the DeepSDP framework proposed by Fazlyab et al., which uses quadratic constraints to abstract the verification problem into a large-scale SDP. However, solving this SDP quickly becomes intractable when the network grows. Our key observation is that by leveraging chordal sparsity, we can decompose the primary computational bottleneck of DeepSDP -- a large linear matrix inequality (LMI) -- into an equivalent collection of smaller LMIs. We call our chordally sparse optimization program Chordal-DeepSDP and prove that its construction is identically expressive as that of DeepSDP. Moreover, we show that additional analysis of Chordal-DeepSDP allows us to further rewrite its collection of LMIs in a second level of decomposition that we call Chordal-DeepSDP-2 -- which results in another significant computational gain. Finally, we provide numerical experiments on real networks of learned cart-pole dynamics, showcasing the computational advantage of Chordal-DeepSDP and Chordal-DeepSDP-2 over DeepSDP.
△ Less
Submitted 8 January, 2024; v1 submitted 7 June, 2022;
originally announced June 2022.
-
Risk of Stochastic Systems for Temporal Logic Specifications
Authors:
Lars Lindemann,
Lejun Jiang,
Nikolai Matni,
George J. Pappas
Abstract:
The wide availability of data coupled with the computational advances in artificial intelligence and machine learning promise to enable many future technologies such as autonomous driving. While there has been a variety of successful demonstrations of these technologies, critical system failures have repeatedly been reported. Even if rare, such system failures pose a serious barrier to adoption wi…
▽ More
The wide availability of data coupled with the computational advances in artificial intelligence and machine learning promise to enable many future technologies such as autonomous driving. While there has been a variety of successful demonstrations of these technologies, critical system failures have repeatedly been reported. Even if rare, such system failures pose a serious barrier to adoption without a rigorous risk assessment. This paper presents a framework for the systematic and rigorous risk verification of systems. We consider a wide range of system specifications formulated in signal temporal logic (STL) and model the system as a stochastic process, permitting discrete-time and continuous-time stochastic processes. We then define the STL robustness risk as the risk of lacking robustness against failure. This definition is motivated as system failures are often caused by missing robustness to modeling errors, system disturbances, and distribution shifts in the underlying data generating process. Within the definition, we permit general classes of risk measures and focus on tail risk measures such as the value-at-risk and the conditional value-at-risk. While the STL robustness risk is in general hard to compute, we propose the approximate STL robustness risk as a more tractable notion that upper bounds the STL robustness risk. We show how the approximate STL robustness risk can accurately be estimated from system trajectory data. For discrete-time stochastic processes, we show under which conditions the approximate STL robustness risk can even be computed exactly. We illustrate our verification algorithm in the autonomous driving simulator CARLA and show how a least risky controller can be selected among four neural network lane kee** controllers for five meaningful system specifications.
△ Less
Submitted 8 October, 2022; v1 submitted 28 May, 2022;
originally announced May 2022.
-
Risk-Bounded Temporal Logic Control of Continuous-Time Stochastic Systems
Authors:
Sleiman Safaoui,
Lars Lindemann,
Iman Shames,
Tyler H. Summers
Abstract:
Motivated by the recent interest in risk-aware control, we study a continuous-time control synthesis problem to bound the risk that a stochastic linear system violates a given specification. We use risk signal temporal logic as a specification formalism in which distributionally robust risk predicates are considered and equipped with the usual Boolean and temporal operators. Our control approach r…
▽ More
Motivated by the recent interest in risk-aware control, we study a continuous-time control synthesis problem to bound the risk that a stochastic linear system violates a given specification. We use risk signal temporal logic as a specification formalism in which distributionally robust risk predicates are considered and equipped with the usual Boolean and temporal operators. Our control approach relies on reformulating these risk predicates as deterministic predicates over mean and covariance states of the system. We then obtain a timed sequence of sets of mean and covariance states from the timed automata representation of the specification. To avoid an explosion in the number of automata states, we propose heuristics to find candidate sequences effectively. To execute and check dynamic feasibility of these sequences, we present a sampled-data control technique based on time discretization and constraint tightening that allows to perform timed transitions while satisfying the continuous-time constraints.
△ Less
Submitted 8 April, 2022;
originally announced April 2022.
-
Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networks
Authors:
Anton Xue,
Lars Lindemann,
Alexander Robey,
Hamed Hassani,
George J. Pappas,
Rajeev Alur
Abstract:
Lipschitz constants of neural networks allow for guarantees of robustness in image classification, safety in controller design, and generalizability beyond the training data. As calculating Lipschitz constants is NP-hard, techniques for estimating Lipschitz constants must navigate the trade-off between scalability and accuracy. In this work, we significantly push the scalability frontier of a semi…
▽ More
Lipschitz constants of neural networks allow for guarantees of robustness in image classification, safety in controller design, and generalizability beyond the training data. As calculating Lipschitz constants is NP-hard, techniques for estimating Lipschitz constants must navigate the trade-off between scalability and accuracy. In this work, we significantly push the scalability frontier of a semidefinite programming technique known as LipSDP while achieving zero accuracy loss. We first show that LipSDP has chordal sparsity, which allows us to derive a chordally sparse formulation that we call Chordal-LipSDP. The key benefit is that the main computational bottleneck of LipSDP, a large semidefinite constraint, is now decomposed into an equivalent collection of smaller ones: allowing Chordal-LipSDP to outperform LipSDP particularly as the network depth grows. Moreover, our formulation uses a tunable sparsity parameter that enables one to gain tighter estimates without incurring a significant computational cost. We illustrate the scalability of our approach through extensive numerical experiments.
△ Less
Submitted 8 January, 2024; v1 submitted 2 April, 2022;
originally announced April 2022.
-
Temporal Robustness of Temporal Logic Specifications: Analysis and Control Design
Authors:
Alëna Rodionova,
Lars Lindemann,
Manfred Morari,
George J. Pappas
Abstract:
We study the temporal robustness of temporal logic specifications and show how to design temporally robust control laws for time-critical control systems. This topic is of particular interest in connected systems and interleaving processes such as multi-robot and human-robot systems where uncertainty in the behavior of individual agents and humans can induce timing uncertainty. Despite the importa…
▽ More
We study the temporal robustness of temporal logic specifications and show how to design temporally robust control laws for time-critical control systems. This topic is of particular interest in connected systems and interleaving processes such as multi-robot and human-robot systems where uncertainty in the behavior of individual agents and humans can induce timing uncertainty. Despite the importance of time-critical systems, temporal robustness of temporal logic specifications has not been studied, especially from a control design point of view. We define synchronous and asynchronous temporal robustness and show that these notions quantify the robustness with respect to synchronous and asynchronous time shifts in the predicates of the temporal logic specification. It is further shown that the synchronous temporal robustness upper bounds the asynchronous temporal robustness. We then study the control design problem in which we aim to design a control law that maximizes the temporal robustness of a dynamical system. Our solution consists of a Mixed-Integer Linear Programming (MILP) encoding that can be used to obtain a sequence of optimal control inputs. While asynchronous temporal robustness is arguably more nuanced than synchronous temporal robustness, we show that control design using synchronous temporal robustness is computationally more efficient. This trade-off can be exploited by the designer depending on the particular application at hand. We conclude the paper with a variety of case studies.
△ Less
Submitted 29 March, 2022;
originally announced March 2022.
-
Temporal Robustness of Stochastic Signals
Authors:
Lars Lindemann,
Alena Rodionova,
George J. Pappas
Abstract:
We study the temporal robustness of stochastic signals. This topic is of particular interest in interleaving processes such as multi-agent systems where communication and individual agents induce timing uncertainty. For a deterministic signal and a given specification, we first introduce the synchronous and the asynchronous temporal robustness to quantify the signal's robustness with respect to sy…
▽ More
We study the temporal robustness of stochastic signals. This topic is of particular interest in interleaving processes such as multi-agent systems where communication and individual agents induce timing uncertainty. For a deterministic signal and a given specification, we first introduce the synchronous and the asynchronous temporal robustness to quantify the signal's robustness with respect to synchronous and asynchronous time shifts in its sub-signals. We then define the temporal robustness risk by investigating the temporal robustness of the realizations of a stochastic signal. This definition can be interpreted as the risk associated with a stochastic signal to not satisfy a specification robustly in time. In this definition, general forms of specifications such as signal temporal logic specifications are permitted. We show how the temporal robustness risk is estimated from data for the value-at-risk. The usefulness of the temporal robustness risk is underlined by both theoretical and empirical evidence. In particular, we provide various numerical case studies including a T-intersection scenario in autonomous driving.
△ Less
Submitted 12 March, 2022; v1 submitted 5 February, 2022;
originally announced February 2022.
-
Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations
Authors:
Lars Lindemann,
Alexander Robey,
Lejun Jiang,
Satyajeet Das,
Stephen Tu,
Nikolai Matni
Abstract:
This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We assume that a model of the system dynamics and a state estimator are available along with corresponding error bounds, e.g., estimated from data in practice. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety, as defined through control…
▽ More
This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We assume that a model of the system dynamics and a state estimator are available along with corresponding error bounds, e.g., estimated from data in practice. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety, as defined through controlled forward invariance of a safe set. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior, e.g., data collected from a human operator or an expert controller. When the parametrization of the ROCBF is linear, then we show that, under mild assumptions, the optimization problem is convex. Along with the optimization problem, we provide verifiable conditions in terms of the density of the data, smoothness of the system model and state estimator, and the size of the error bounds that guarantee validity of the obtained ROCBF. Towards obtaining a practical control algorithm, we propose an algorithmic implementation of our theoretical framework that accounts for assumptions made in our framework in practice. We validate our algorithm in the autonomous driving simulator CARLA and demonstrate how to learn safe control laws from simulated RGB camera images.
△ Less
Submitted 2 April, 2024; v1 submitted 18 November, 2021;
originally announced November 2021.
-
Reactive and Risk-Aware Control for Signal Temporal Logic
Authors:
Lars Lindemann,
George J. Pappas,
Dimos V. Dimarogonas
Abstract:
The deployment of autonomous systems in uncertain and dynamic environments has raised fundamental questions. Addressing these is pivotal to build fully autonomous systems and requires a systematic integration of planning and control. We first propose reactive risk signal interval temporal logic (ReRiSITL) as an extension of signal temporal logic (STL) to formulate complex spatiotemporal specificat…
▽ More
The deployment of autonomous systems in uncertain and dynamic environments has raised fundamental questions. Addressing these is pivotal to build fully autonomous systems and requires a systematic integration of planning and control. We first propose reactive risk signal interval temporal logic (ReRiSITL) as an extension of signal temporal logic (STL) to formulate complex spatiotemporal specifications. Unlike STL, ReRiSITL allows to consider uncontrollable propositions that may model humans as well as random environmental events such as sensor failures. Additionally, ReRiSITL allows to incorporate risk measures, such as (but not limited to) the Conditional Value-at-Risk, to measure the risk of violating certain spatial specifications. Second, we propose an algorithm to check if an ReRiSITL specification is satisfiable. For this purpose, we abstract the ReRiSITL specification into a timed signal transducer and devise a game-based approach. Third, we propose a reactive planning and control framework for dynamical control systems under ReRiSITL specifications.
△ Less
Submitted 30 August, 2021;
originally announced August 2021.
-
Robust Motion Planning in the Presence of Estimation Uncertainty
Authors:
Lars Lindemann,
Matthew Cleaveland,
Yiannis Kantaros,
George J. Pappas
Abstract:
Motion planning is a fundamental problem and focuses on finding control inputs that enable a robot to reach a goal region while safely avoiding obstacles. However, in many situations, the state of the system may not be known but only estimated using, for instance, a Kalman filter. This results in a novel motion planning problem where safety must be ensured in the presence of state estimation uncer…
▽ More
Motion planning is a fundamental problem and focuses on finding control inputs that enable a robot to reach a goal region while safely avoiding obstacles. However, in many situations, the state of the system may not be known but only estimated using, for instance, a Kalman filter. This results in a novel motion planning problem where safety must be ensured in the presence of state estimation uncertainty. Previous approaches to this problem are either conservative or integrate state estimates optimistically which leads to non-robust solutions. Optimistic solutions require frequent replanning to not endanger the safety of the system. We propose a new formulation to this problem with the aim to be robust to state estimation errors while not being overly conservative. In particular, we formulate a stochastic optimal control problem that contains robustified risk-aware safety constraints by incorporating robustness margins to account for state estimation errors. We propose a novel sampling-based approach that builds trees exploring the reachable space of Gaussian distributions that capture uncertainty both in state estimation and in future measurements. We provide robustness guarantees and show, both in theory and simulations, that the induced robustness margins constitute a trade-off between conservatism and robustness for planning under estimation uncertainty that allows to control the frequency of replanning.
△ Less
Submitted 26 August, 2021;
originally announced August 2021.
-
Time-Robust Control for STL Specifications
Authors:
Alena Rodionova,
Lars Lindemann,
Manfred Morari,
George J. Pappas
Abstract:
We present a robust control framework for time-critical systems in which satisfying real-time constraints robustly is of utmost importance for the safety of the system. Signal Temporal Logic (STL) provides a formal means to express a large variety of real-time constraints over signals and is suited for planning and control purposes as it allows us to reason about the time robustness of such constr…
▽ More
We present a robust control framework for time-critical systems in which satisfying real-time constraints robustly is of utmost importance for the safety of the system. Signal Temporal Logic (STL) provides a formal means to express a large variety of real-time constraints over signals and is suited for planning and control purposes as it allows us to reason about the time robustness of such constraints. The time robustness of STL particularly quantifies the extent to which timing uncertainties can be tolerated without violating real-time specifications. In this paper, we first pose a control problem in which we aim to find an optimal input sequence to a control system that maximizes the time robustness of an STL constraint. We then propose a Mixed Integer Linear Program (MILP) encoding and provide correctness guarantees along with a complexity analysis of the encoding. We also show in two case studies that maximizing STL time robustness allows to account for timing uncertainties of the underlying control system.
△ Less
Submitted 13 December, 2021; v1 submitted 6 April, 2021;
originally announced April 2021.
-
STL Robustness Risk over Discrete-Time Stochastic Processes
Authors:
Lars Lindemann,
Nikolai Matni,
George J. Pappas
Abstract:
We present a framework to interpret signal temporal logic (STL) formulas over discrete-time stochastic processes in terms of the induced risk. Each realization of a stochastic process either satisfies or violates an STL formula. In fact, we can assign a robustness value to each realization that indicates how robustly this realization satisfies an STL formula. We then define the risk of a stochasti…
▽ More
We present a framework to interpret signal temporal logic (STL) formulas over discrete-time stochastic processes in terms of the induced risk. Each realization of a stochastic process either satisfies or violates an STL formula. In fact, we can assign a robustness value to each realization that indicates how robustly this realization satisfies an STL formula. We then define the risk of a stochastic process not satisfying an STL formula robustly, referred to as the STL robustness risk. In our definition, we permit general classes of risk measures such as, but not limited to, the conditional value-at-risk. While in general hard to compute, we propose an approximation of the STL robustness risk. This approximation has the desirable property of being an upper bound of the STL robustness risk when the chosen risk measure is monotone, a property satisfied by most risk measures. Motivated by the interest in data-driven approaches, we present a sampling-based method for estimating the approximate STL robustness risk from data for the value-at-risk. While we consider the value-at-risk, we highlight that such sampling-based methods are viable for other risk measures.
△ Less
Submitted 7 March, 2022; v1 submitted 3 April, 2021;
originally announced April 2021.
-
Barrier Function-based Collaborative Control of Multiple Robots under Signal Temporal Logic Tasks
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
Motivated by the recent interest in cyber-physical and autonomous robotic systems, we study the problem of dynamically coupled multi-agent systems under a set of signal temporal logic tasks. In particular, the satisfaction of each of these signal temporal logic tasks depends on the behavior of a distinct set of agents. Instead of abstracting the agent dynamics and the temporal logic tasks into a d…
▽ More
Motivated by the recent interest in cyber-physical and autonomous robotic systems, we study the problem of dynamically coupled multi-agent systems under a set of signal temporal logic tasks. In particular, the satisfaction of each of these signal temporal logic tasks depends on the behavior of a distinct set of agents. Instead of abstracting the agent dynamics and the temporal logic tasks into a discrete domain and solving the problem therein or using optimization-based methods, we derive collaborative feedback control laws. These control laws are based on a decentralized control barrier function condition that results in discontinuous control laws, as opposed to a centralized condition resembling the single-agent case. The benefits of our approach are inherent robustness properties typically present in feedback control as well as satisfaction guarantees for continuous-time multi-agent systems. More specifically, time-varying control barrier functions are used that account for the semantics of the signal temporal logic tasks at hand. For a certain fragment of signal temporal logic tasks, we further propose a systematic way to construct such control barrier functions. Finally, we show the efficacy and robustness of our framework in an experiment including a group of three omnidirectional robots.
△ Less
Submitted 4 February, 2021;
originally announced February 2021.
-
Learning Robust Hybrid Control Barrier Functions for Uncertain Systems
Authors:
Alexander Robey,
Lars Lindemann,
Stephen Tu,
Nikolai Matni
Abstract:
The need for robust control laws is especially important in safety-critical applications. We propose robust hybrid control barrier functions as a means to synthesize control laws that ensure robust safety. Based on this notion, we formulate an optimization problem for learning robust hybrid control barrier functions from data. We identify sufficient conditions on the data such that feasibility of…
▽ More
The need for robust control laws is especially important in safety-critical applications. We propose robust hybrid control barrier functions as a means to synthesize control laws that ensure robust safety. Based on this notion, we formulate an optimization problem for learning robust hybrid control barrier functions from data. We identify sufficient conditions on the data such that feasibility of the optimization problem ensures correctness of the learned robust hybrid control barrier functions. Our techniques allow us to safely expand the region of attraction of a compass gait walker that is subject to model uncertainty.
△ Less
Submitted 12 May, 2021; v1 submitted 16 January, 2021;
originally announced January 2021.
-
Decentralized Control Barrier Functions for Coupled Multi-Agent Systems under Signal Temporal Logic Tasks
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
We study the problem of controlling multi-agent systems under a set of signal temporal logic tasks. Signal temporal logic is a formalism that is used to express time and space constraints for dynamical systems. Recent methods to solve the control synthesis problem for single-agent systems under signal temporal logic tasks are, however, subject to a high computational complexity. Methods for multi-…
▽ More
We study the problem of controlling multi-agent systems under a set of signal temporal logic tasks. Signal temporal logic is a formalism that is used to express time and space constraints for dynamical systems. Recent methods to solve the control synthesis problem for single-agent systems under signal temporal logic tasks are, however, subject to a high computational complexity. Methods for multi-agent systems scale at least linearly with the number of agents and induce even higher computational burdens. We propose a computationally-efficient control strategy to solve the multi-agent control synthesis problem that results in a robust satisfaction of a set of signal temporal logic tasks. In particular, a decentralized feedback control law is proposed that is based on time-varying control barrier functions. The obtained control law is discontinuous and formal guarantees are provided by nonsmooth analysis. Simulations show the efficacy of the presented method.
△ Less
Submitted 25 November, 2020;
originally announced November 2020.
-
Event-triggered Feedback Control for Signal Temporal Logic Tasks
Authors:
Lars Lindemann,
Dipankar Maity,
John S. Baras,
Dimos V. Dimarogonas
Abstract:
A framework for the event-triggered control synthesis under signal temporal logic (STL) tasks is proposed. In our previous work, a continuous-time feedback control law was designed, using the prescribed performance control technique, to satisfy STL tasks. We replace this continuous-time feedback control law by an event-triggered controller. The event-triggering mechanism is based on a maximum trig…
▽ More
A framework for the event-triggered control synthesis under signal temporal logic (STL) tasks is proposed. In our previous work, a continuous-time feedback control law was designed, using the prescribed performance control technique, to satisfy STL tasks. We replace this continuous-time feedback control law by an event-triggered controller. The event-triggering mechanism is based on a maximum triggering interval and on a norm bound on the difference between the value of the current state and the value of the state at the last triggering instance. Simulations of a multi-agent system quantitatively show the efficacy of using an event-triggered controller to reduce communication and computation efforts.
△ Less
Submitted 25 November, 2020;
originally announced November 2020.
-
Learning Hybrid Control Barrier Functions from Data
Authors:
Lars Lindemann,
Haimin Hu,
Alexander Robey,
Hanwen Zhang,
Dimos V. Dimarogonas,
Stephen Tu,
Nikolai Matni
Abstract:
Motivated by the lack of systematic tools to obtain safe control laws for hybrid systems, we propose an optimization-based framework for learning certifiably safe control laws from data. In particular, we assume a setting in which the system dynamics are known and in which data exhibiting safe system behavior is available. We propose hybrid control barrier functions for hybrid systems as a means t…
▽ More
Motivated by the lack of systematic tools to obtain safe control laws for hybrid systems, we propose an optimization-based framework for learning certifiably safe control laws from data. In particular, we assume a setting in which the system dynamics are known and in which data exhibiting safe system behavior is available. We propose hybrid control barrier functions for hybrid systems as a means to synthesize safe control inputs. Based on this notion, we present an optimization-based framework to learn such hybrid control barrier functions from data. Importantly, we identify sufficient conditions on the data such that feasibility of the optimization problem ensures correctness of the learned hybrid control barrier functions, and hence the safety of the system. We illustrate our findings in two simulations studies, including a compass gait walker.
△ Less
Submitted 8 November, 2020;
originally announced November 2020.
-
Character Entropy in Modern and Historical Texts: Comparison Metrics for an Undeciphered Manuscript
Authors:
Luke Lindemann,
Claire Bowern
Abstract:
This paper outlines the creation of three corpora for multilingual comparison and analysis of the Voynich manuscript: a corpus of Voynich texts partitioned by Currier language, scribal hand, and transcription system, a corpus of 294 language samples compiled from Wikipedia, and a corpus of eighteen transcribed historical texts in eight languages. These corpora will be utilized in subsequent work b…
▽ More
This paper outlines the creation of three corpora for multilingual comparison and analysis of the Voynich manuscript: a corpus of Voynich texts partitioned by Currier language, scribal hand, and transcription system, a corpus of 294 language samples compiled from Wikipedia, and a corpus of eighteen transcribed historical texts in eight languages. These corpora will be utilized in subsequent work by the Voynich Working Group at Yale University.
We demonstrate the utility of these corpora for studying characteristics of the Voynich script and language, with an analysis of conditional character entropy in Voynichese. We discuss the interaction between character entropy and language, script size and type, glyph compositionality, scribal conventions and abbreviations, positional character variants, and bigram frequency.
This analysis characterizes the interaction between script compositionality, character size, and predictability. We show that substantial manipulations of glyph composition are not sufficient to align conditional entropy levels with natural languages. The unusually predictable nature of the Voynichese script is not attributable to a particular script or transcription system, underlying language, or substitution cipher. Voynichese is distinct from every comparison text in our corpora because character placement is highly constrained within the word, and this may indicate the loss of phonemic distinctions from the underlying language.
△ Less
Submitted 18 May, 2021; v1 submitted 27 October, 2020;
originally announced October 2020.
-
Provably Safe Control of Lagrangian Systems in Obstacle-Scattered Environments
Authors:
Fernando S. Barbosa,
Lars Lindemann,
Dimos V. Dimarogonas,
Jana Tumova
Abstract:
We propose a hybrid feedback control law that guarantees both safety and asymptotic stability for a class of Lagrangian systems in environments with obstacles. Rather than performing trajectory planning and implementing a trajectory-tracking feedback control law, our approach requires a sequence of locations in the environment (a path plan) and an abstraction of the obstacle-free space. The proble…
▽ More
We propose a hybrid feedback control law that guarantees both safety and asymptotic stability for a class of Lagrangian systems in environments with obstacles. Rather than performing trajectory planning and implementing a trajectory-tracking feedback control law, our approach requires a sequence of locations in the environment (a path plan) and an abstraction of the obstacle-free space. The problem of following a path plan is then interpreted as a sequence of reach-avoid problems: the system is required to consecutively reach each location of the path plan while staying within safe regions. Obstacle-free ellipsoids are used as a way of defining such safe regions, each of which encloses two consecutive locations. Feasible Control Barrier Functions (CBFs) are created directly from geometric constraints, the ellipsoids, ensuring forward-invariance, and therefore safety. Reachability to each location is guaranteed by asymptotically stabilizing Control Lyapunov Functions (CLFs). Both CBFs and CLFs are then encoded into quadratic programs (QPs) without the need of relaxation variables. Furthermore, we also propose a switching mechanism that guarantees the control law is correct and well-defined even when transitioning between QPs. Simulations show the effectiveness of the proposed approach in two complex scenarios.
△ Less
Submitted 4 September, 2020;
originally announced September 2020.
-
Control Design for Risk-Based Signal Temporal Logic Specifications
Authors:
Sleiman Safaoui,
Lars Lindemann,
Dimos V Dimarogonas,
Iman Shames,
Tyler H Summers
Abstract:
We present a general framework for risk semantics on Signal Temporal Logic (STL) specifications for stochastic dynamical systems using axiomatic risk theory. We show that under our recursive risk semantics, risk constraints on STL formulas can be expressed in terms of risk constraints on atomic predicates. We then show how this allows a (stochastic) STL risk constraint to be transformed into a ris…
▽ More
We present a general framework for risk semantics on Signal Temporal Logic (STL) specifications for stochastic dynamical systems using axiomatic risk theory. We show that under our recursive risk semantics, risk constraints on STL formulas can be expressed in terms of risk constraints on atomic predicates. We then show how this allows a (stochastic) STL risk constraint to be transformed into a risk-tightened deterministic STL constraint on a related deterministic nominal system, enabling the application of existing STL methods. For affine predicate functions and a (coherent) Distributionally Robust Value at Risk measure, we show how risk constraints on atomic predicates can be reformulated as tightened deterministic affine constraints. We demonstrate the framework using a Model Predictive Control (MPC) design with an STL risk constraint.
△ Less
Submitted 30 May, 2020;
originally announced June 2020.
-
Learning Control Barrier Functions from Expert Demonstrations
Authors:
Alexander Robey,
Haimin Hu,
Lars Lindemann,
Hanwen Zhang,
Dimos V. Dimarogonas,
Stephen Tu,
Nikolai Matni
Abstract:
Inspired by the success of imitation and inverse reinforcement learning in replicating expert behavior through optimal control, we propose a learning based approach to safe controller synthesis based on control barrier functions (CBFs). We consider the setting of a known nonlinear control affine dynamical system and assume that we have access to safe trajectories generated by an expert - a practic…
▽ More
Inspired by the success of imitation and inverse reinforcement learning in replicating expert behavior through optimal control, we propose a learning based approach to safe controller synthesis based on control barrier functions (CBFs). We consider the setting of a known nonlinear control affine dynamical system and assume that we have access to safe trajectories generated by an expert - a practical example of such a setting would be a kinematic model of a self-driving vehicle with safe trajectories (e.g., trajectories that avoid collisions with obstacles in the environment) generated by a human driver. We then propose and analyze an optimization-based approach to learning a CBF that enjoys provable safety guarantees under suitable Lipschitz smoothness assumptions on the underlying dynamical system. A strength of our approach is that it is agnostic to the parameterization used to represent the CBF, assuming only that the Lipschitz constant of such functions can be efficiently bounded. Furthermore, if the CBF parameterization is convex, then under mild assumptions, so is our learning process. We end with extensive numerical evaluations of our results on both planar and realistic examples, using both random feature and deep neural network parameterizations of the CBF. To the best of our knowledge, these are the first results that learn provably safe control barrier functions from data.
△ Less
Submitted 8 November, 2020; v1 submitted 7 April, 2020;
originally announced April 2020.
-
Control Barrier Functions for Nonholonomic Systems under Risk Signal Temporal Logic Specifications
Authors:
Lars Lindemann,
George J. Pappas,
Dimos V. Dimarogonas
Abstract:
Temporal logics provide a formalism for expressing complex system specifications. A large body of literature has addressed the verification and the control synthesis problem for deterministic systems under such specifications. For stochastic systems or systems operating in unknown environments, however, only the probability of satisfying a specification has been considered so far, neglecting the r…
▽ More
Temporal logics provide a formalism for expressing complex system specifications. A large body of literature has addressed the verification and the control synthesis problem for deterministic systems under such specifications. For stochastic systems or systems operating in unknown environments, however, only the probability of satisfying a specification has been considered so far, neglecting the risk of not satisfying the specification. Towards addressing this shortcoming, we consider, for the first time, risk metrics, such as (but not limited to) the Conditional Value-at-Risk, and propose risk signal temporal logic. Specifically, we compose risk metrics with stochastic predicates to consider the risk of violating certain spatial specifications. As a particular instance of such stochasticity, we consider control systems in unknown environments and present a determinization of the risk signal temporal logic specification to transform the stochastic control problem into a deterministic one. For unicycle-like dynamics, we then extend our previous work on deterministic time-varying control barrier functions.
△ Less
Submitted 26 August, 2020; v1 submitted 5 April, 2020;
originally announced April 2020.