-
LTL-D*: Incrementally Optimal Replanning for Feasible and Infeasible Tasks in Linear Temporal Logic Specifications
Authors:
Jiming Ren,
Haris Miller,
Karen M. Feigh,
Samuel Coogan,
Ye Zhao
Abstract:
This paper presents an incremental replanning algorithm, dubbed LTL-D*, for temporal-logic-based task planning in a dynamically changing environment. Unexpected changes in the environment may lead to failures in satisfying a task specification in the form of a Linear Temporal Logic (LTL). In this study, the considered failures are categorized into two classes: (i) the desired LTL specification can…
▽ More
This paper presents an incremental replanning algorithm, dubbed LTL-D*, for temporal-logic-based task planning in a dynamically changing environment. Unexpected changes in the environment may lead to failures in satisfying a task specification in the form of a Linear Temporal Logic (LTL). In this study, the considered failures are categorized into two classes: (i) the desired LTL specification can be satisfied via replanning, and (ii) the desired LTL specification is infeasible to meet strictly and can only be satisfied in a "relaxed" fashion. To address these failures, the proposed algorithm finds an optimal replanning solution that minimally violates desired task specifications. In particular, our approach leverages the D* Lite algorithm and employs a distance metric within the synthesized automaton to quantify the degree of the task violation and then replan incrementally. This ensures plan optimality and reduces planning time, especially when frequent replanning is required. Our approach is implemented in a robot navigation simulation to demonstrate a significant improvement in the computational efficiency for replanning by two orders of magnitude.
△ Less
Submitted 1 April, 2024;
originally announced April 2024.
-
Bipedal Safe Navigation over Uncertain Rough Terrain: Unifying Terrain Map** and Locomotion Stability
Authors:
Kasidit Muenprasitivej,
Jesse Jiang,
Abdulaziz Shamsah,
Samuel Coogan,
Ye Zhao
Abstract:
We study the problem of bipedal robot navigation in complex environments with uncertain and rough terrain. In particular, we consider a scenario in which the robot is expected to reach a desired goal location by traversing an environment with uncertain terrain elevation. Such terrain uncertainties induce not only untraversable regions but also robot motion perturbations. Thus, the problems of terr…
▽ More
We study the problem of bipedal robot navigation in complex environments with uncertain and rough terrain. In particular, we consider a scenario in which the robot is expected to reach a desired goal location by traversing an environment with uncertain terrain elevation. Such terrain uncertainties induce not only untraversable regions but also robot motion perturbations. Thus, the problems of terrain map** and locomotion stability are intertwined. We evaluate three different kernels for Gaussian process (GP) regression to learn the terrain elevation. We also learn the motion deviation resulting from both the terrain as well as the discrepancy between the reduced-order Prismatic Inverted Pendulum Model used for planning and the full-order locomotion dynamics. We propose a hierarchical locomotion-dynamics-aware sampling-based navigation planner. The global navigation planner plans a series of local waypoints to reach the desired goal locations while respecting locomotion stability constraints. Then, a local navigation planner is used to generate a sequence of dynamically feasible footsteps to reach local waypoints. We develop a novel trajectory evaluation metric to minimize motion deviation and maximize information gain of the terrain elevation map. We evaluate the efficacy of our planning framework on Digit bipedal robot simulation in MuJoCo.
△ Less
Submitted 15 April, 2024; v1 submitted 24 March, 2024;
originally announced March 2024.
-
Efficient Reachable Sets on Lie Groups Using Lie Algebra Monotonicity and Tangent Intervals
Authors:
Akash Harapanahalli,
Samuel Coogan
Abstract:
In this paper, we efficiently compute overapproximated reachable sets for control systems evolving on Lie groups, building off results from monotone systems theory and geometric integration theory. We propose to consider intervals living in the Lie algebra, which through the exponential map, describe real sets on the Lie group. A local equivalence between the original system and a system evolving…
▽ More
In this paper, we efficiently compute overapproximated reachable sets for control systems evolving on Lie groups, building off results from monotone systems theory and geometric integration theory. We propose to consider intervals living in the Lie algebra, which through the exponential map, describe real sets on the Lie group. A local equivalence between the original system and a system evolving on the Lie algebra allows existing interval reachability techniques to apply in the tangent space. Using interval bounds of the Baker-Campbell-Hausdorff formula, a Runge-Kutta-Munthe-Kaas reachability algorithm is proposed, providing reachable set estimates for arbitrary time horizons at little computational cost. The algorithm is demonstrated on through consensus on a torus and attitude control on $SO(3)$.
△ Less
Submitted 24 March, 2024;
originally announced March 2024.
-
Evaluating Frontier Models for Dangerous Capabilities
Authors:
Mary Phuong,
Matthew Aitchison,
Elliot Catt,
Sarah Cogan,
Alexandre Kaskasoli,
Victoria Krakovna,
David Lindner,
Matthew Rahtz,
Yannis Assael,
Sarah Hodkinson,
Heidi Howard,
Tom Lieberum,
Ramana Kumar,
Maria Abi Raad,
Albert Webson,
Lewis Ho,
Sharon Lin,
Sebastian Farquhar,
Marcus Hutter,
Gregoire Deletang,
Anian Ruoss,
Seliem El-Sayed,
Sasha Brown,
Anca Dragan,
Rohin Shah
, et al. (2 additional authors not shown)
Abstract:
To understand the risks posed by a new AI system, we must understand what it can and cannot do. Building on prior work, we introduce a programme of new "dangerous capability" evaluations and pilot them on Gemini 1.0 models. Our evaluations cover four areas: (1) persuasion and deception; (2) cyber-security; (3) self-proliferation; and (4) self-reasoning. We do not find evidence of strong dangerous…
▽ More
To understand the risks posed by a new AI system, we must understand what it can and cannot do. Building on prior work, we introduce a programme of new "dangerous capability" evaluations and pilot them on Gemini 1.0 models. Our evaluations cover four areas: (1) persuasion and deception; (2) cyber-security; (3) self-proliferation; and (4) self-reasoning. We do not find evidence of strong dangerous capabilities in the models we evaluated, but we flag early warning signs. Our goal is to help advance a rigorous science of dangerous capability evaluation, in preparation for future models.
△ Less
Submitted 5 April, 2024; v1 submitted 20 March, 2024;
originally announced March 2024.
-
Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context
Authors:
Gemini Team,
Petko Georgiev,
Ving Ian Lei,
Ryan Burnell,
Libin Bai,
Anmol Gulati,
Garrett Tanzer,
Damien Vincent,
Zhufeng Pan,
Shibo Wang,
Soroosh Mariooryad,
Yifan Ding,
Xinyang Geng,
Fred Alcober,
Roy Frostig,
Mark Omernick,
Lexi Walker,
Cosmin Paduraru,
Christina Sorokin,
Andrea Tacchetti,
Colin Gaffney,
Samira Daruki,
Olcan Sercinoglu,
Zach Gleicher,
Juliette Love
, et al. (1092 additional authors not shown)
Abstract:
In this report, we introduce the Gemini 1.5 family of models, representing the next generation of highly compute-efficient multimodal models capable of recalling and reasoning over fine-grained information from millions of tokens of context, including multiple long documents and hours of video and audio. The family includes two new models: (1) an updated Gemini 1.5 Pro, which exceeds the February…
▽ More
In this report, we introduce the Gemini 1.5 family of models, representing the next generation of highly compute-efficient multimodal models capable of recalling and reasoning over fine-grained information from millions of tokens of context, including multiple long documents and hours of video and audio. The family includes two new models: (1) an updated Gemini 1.5 Pro, which exceeds the February version on the great majority of capabilities and benchmarks; (2) Gemini 1.5 Flash, a more lightweight variant designed for efficiency with minimal regression in quality. Gemini 1.5 models achieve near-perfect recall on long-context retrieval tasks across modalities, improve the state-of-the-art in long-document QA, long-video QA and long-context ASR, and match or surpass Gemini 1.0 Ultra's state-of-the-art performance across a broad set of benchmarks. Studying the limits of Gemini 1.5's long-context ability, we find continued improvement in next-token prediction and near-perfect retrieval (>99%) up to at least 10M tokens, a generational leap over existing models such as Claude 3.0 (200k) and GPT-4 Turbo (128k). Finally, we highlight real-world use cases, such as Gemini 1.5 collaborating with professionals on completing their tasks achieving 26 to 75% time savings across 10 different job categories, as well as surprising new capabilities of large language models at the frontier; when given a grammar manual for Kalamang, a language with fewer than 200 speakers worldwide, the model learns to translate English to Kalamang at a similar level to a person who learned from the same content.
△ Less
Submitted 14 June, 2024; v1 submitted 8 March, 2024;
originally announced March 2024.
-
$\texttt{immrax}$: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX
Authors:
Akash Harapanahalli,
Saber Jafarpour,
Samuel Coogan
Abstract:
We present an implementation of interval analysis and mixed monotone interval reachability analysis as function transforms in Python, fully composable with the computational framework JAX. The resulting toolbox inherits several key features from JAX, including computational efficiency through Just-In-Time Compilation, GPU acceleration for quick parallelized computations, and Automatic Differentiab…
▽ More
We present an implementation of interval analysis and mixed monotone interval reachability analysis as function transforms in Python, fully composable with the computational framework JAX. The resulting toolbox inherits several key features from JAX, including computational efficiency through Just-In-Time Compilation, GPU acceleration for quick parallelized computations, and Automatic Differentiability. We demonstrate the toolbox's performance on several case studies, including a reachability problem on a vehicle model controlled by a neural network, and a robust closed-loop optimal control problem for a swinging pendulum.
△ Less
Submitted 30 April, 2024; v1 submitted 21 January, 2024;
originally announced January 2024.
-
Gemini: A Family of Highly Capable Multimodal Models
Authors:
Gemini Team,
Rohan Anil,
Sebastian Borgeaud,
Jean-Baptiste Alayrac,
Jiahui Yu,
Radu Soricut,
Johan Schalkwyk,
Andrew M. Dai,
Anja Hauth,
Katie Millican,
David Silver,
Melvin Johnson,
Ioannis Antonoglou,
Julian Schrittwieser,
Amelia Glaese,
Jilin Chen,
Emily Pitler,
Timothy Lillicrap,
Angeliki Lazaridou,
Orhan Firat,
James Molloy,
Michael Isard,
Paul R. Barham,
Tom Hennigan,
Benjamin Lee
, et al. (1325 additional authors not shown)
Abstract:
This report introduces a new family of multimodal models, Gemini, that exhibit remarkable capabilities across image, audio, video, and text understanding. The Gemini family consists of Ultra, Pro, and Nano sizes, suitable for applications ranging from complex reasoning tasks to on-device memory-constrained use-cases. Evaluation on a broad range of benchmarks shows that our most-capable Gemini Ultr…
▽ More
This report introduces a new family of multimodal models, Gemini, that exhibit remarkable capabilities across image, audio, video, and text understanding. The Gemini family consists of Ultra, Pro, and Nano sizes, suitable for applications ranging from complex reasoning tasks to on-device memory-constrained use-cases. Evaluation on a broad range of benchmarks shows that our most-capable Gemini Ultra model advances the state of the art in 30 of 32 of these benchmarks - notably being the first model to achieve human-expert performance on the well-studied exam benchmark MMLU, and improving the state of the art in every one of the 20 multimodal benchmarks we examined. We believe that the new capabilities of the Gemini family in cross-modal reasoning and language understanding will enable a wide variety of use cases. We discuss our approach toward post-training and deploying Gemini models responsibly to users through services including Gemini, Gemini Advanced, Google AI Studio, and Cloud Vertex AI.
△ Less
Submitted 17 June, 2024; v1 submitted 18 December, 2023;
originally announced December 2023.
-
Interval Signal Temporal Logic from Natural Inclusion Functions
Authors:
Luke Baird,
Akash Harapanahalli,
Samuel Coogan
Abstract:
We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (\ISTL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the $\min$ and $\max$ functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL…
▽ More
We propose an interval extension of Signal Temporal Logic (STL) called Interval Signal Temporal Logic (\ISTL). Given an STL formula, we consider an interval inclusion function for each of its predicates. Then, we use minimal inclusion functions for the $\min$ and $\max$ functions to recursively build an interval robustness that is a natural inclusion function for the robustness of the original STL formula. The resulting interval semantics accommodate, for example, uncertain signals modeled as a signal of intervals and uncertain predicates modeled with appropriate inclusion functions. In many cases, verification or synthesis algorithms developed for STL apply to \ISTL with minimal theoretic and algorithmic changes, and existing code can be readily extended using interval arithmetic packages at negligible computational expense. To demonstrate \ISTL, we present an example of offline monitoring from an uncertain signal trace obtained from a hardware experiment and an example of robust online control synthesis enforcing an STL formula with uncertain predicates.
△ Less
Submitted 11 December, 2023; v1 submitted 19 September, 2023;
originally announced September 2023.
-
A Contracting Dynamical System Perspective toward Interval Markov Decision Processes
Authors:
Saber Jafarpour,
Samuel Coogan
Abstract:
Interval Markov decision processes are a class of Markov models where the transition probabilities between the states belong to intervals. In this paper, we study the problem of efficient estimation of the optimal policies in Interval Markov Decision Processes (IMDPs) with continuous action-space. Given an IMDP, we show that the pessimistic (resp. the optimistic) value iterations, i.e., the value…
▽ More
Interval Markov decision processes are a class of Markov models where the transition probabilities between the states belong to intervals. In this paper, we study the problem of efficient estimation of the optimal policies in Interval Markov Decision Processes (IMDPs) with continuous action-space. Given an IMDP, we show that the pessimistic (resp. the optimistic) value iterations, i.e., the value iterations under the assumption of a competitive adversary (resp. cooperative agent), are monotone dynamical systems and are contracting with respect to the $\ell_{\infty}$-norm. Inspired by this dynamical system viewpoint, we introduce another IMDP, called the action-space relaxation IMDP. We show that the action-space relaxation IMDP has two key features: (i) its optimal value is an upper bound for the optimal value of the original IMDP, and (ii) its value iterations can be efficiently solved using tools and techniques from convex optimization. We then consider the policy optimization problems at each step of the value iterations as a feedback controller of the value function. Using this system-theoretic perspective, we propose an iteration-distributed implementation of the value iterations for approximating the optimal value of the action-space relaxation IMDP.
△ Less
Submitted 16 September, 2023;
originally announced September 2023.
-
Forward Invariance in Neural Network Controlled Systems
Authors:
Akash Harapanahalli,
Saber Jafarpour,
Samuel Coogan
Abstract:
We present a framework based on interval analysis and monotone systems theory to certify and search for forward invariant sets in nonlinear systems with neural network controllers. The framework (i) constructs localized first-order inclusion functions for the closed-loop system using Jacobian bounds and existing neural network verification tools; (ii) builds a dynamical embedding system where its…
▽ More
We present a framework based on interval analysis and monotone systems theory to certify and search for forward invariant sets in nonlinear systems with neural network controllers. The framework (i) constructs localized first-order inclusion functions for the closed-loop system using Jacobian bounds and existing neural network verification tools; (ii) builds a dynamical embedding system where its evaluation along a single trajectory directly corresponds with a nested family of hyper-rectangles provably converging to an attractive set of the original system; (iii) utilizes linear transformations to build families of nested paralleletopes with the same properties. The framework is automated in Python using our interval analysis toolbox $\texttt{npinterval}$, in conjunction with the symbolic arithmetic toolbox $\texttt{sympy}$, demonstrated on an $8$-dimensional leader-follower system.
△ Less
Submitted 9 December, 2023; v1 submitted 16 September, 2023;
originally announced September 2023.
-
Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops
Authors:
Saber Jafarpour,
Akash Harapanahalli,
Samuel Coogan
Abstract:
In this paper, we propose a computationally efficient framework for interval reachability of systems with neural network controllers. Our approach leverages inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system, where a single trajectory over-approximates the original system's behavior under uncerta…
▽ More
In this paper, we propose a computationally efficient framework for interval reachability of systems with neural network controllers. Our approach leverages inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system, where a single trajectory over-approximates the original system's behavior under uncertainty. We propose two methods for constructing closed-loop embedding systems, which account for the interactions between the system and the controller in different ways. The interconnection-based approach considers the worst-case evolution of each coordinate separately by substituting the neural network inclusion function into the open-loop inclusion function. The interaction-based approach uses novel Jacobian-based inclusion functions to capture the first-order interactions between the open-loop system and the controller by leveraging state-of-the-art neural network verifiers. Finally, we implement our approach in a Python framework called ReachMM to demonstrate its efficiency and scalability on benchmarks and examples ranging to $200$ state dimensions.
△ Less
Submitted 27 June, 2024; v1 submitted 27 July, 2023;
originally announced July 2023.
-
A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems
Authors:
Akash Harapanahalli,
Saber Jafarpour,
Samuel Coogan
Abstract:
In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of map**s. The toolbox offers efficient computation of natural inclusion functions using compiled C code, as well as a familiar interfac…
▽ More
In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of map**s. The toolbox offers efficient computation of natural inclusion functions using compiled C code, as well as a familiar interface in numpy with its canonical features, such as n-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in formal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.
△ Less
Submitted 27 June, 2023;
originally announced June 2023.
-
GreenEVT: Greensboro Electric Vehicle Testbed
Authors:
Gustav Nilsson,
Alejandro D. Owen Aquino,
Samuel Coogan,
Daniel K. Molzahn
Abstract:
The ongoing electrification of the transportation fleet will increase the load on the electric power grid. Since both the transportation network and the power grid already experience periods of significant stress, joint analyses of both infrastructures will most likely be necessary to ensure acceptable operation in the future. To enable such analyses, this paper presents an open-source testbed tha…
▽ More
The ongoing electrification of the transportation fleet will increase the load on the electric power grid. Since both the transportation network and the power grid already experience periods of significant stress, joint analyses of both infrastructures will most likely be necessary to ensure acceptable operation in the future. To enable such analyses, this paper presents an open-source testbed that jointly simulates high-fidelity models of both the electric distribution system and the transportation network. The testbed utilizes two open-source simulators, OpenDSS to simulate the electric distribution system and the microscopic traffic simulator SUMO to simulate the traffic dynamics. Electric vehicle charging links the electric distribution system and the transportation network models at vehicle locations determined using publicly available parcel data. Leveraging high-fidelity synthetic electric distribution system data from the SMART-DS project and transportation system data from OpenStreetMap, this testbed models the city of Greensboro, NC down to the household level. Moreover, the methodology and the supporting scripts released with the testbed allow adaption to other areas where high-fidelity geolocated OpenDSS datasets are available. After describing the components and usage of the testbed, we exemplify applications enabled by the testbed via two scenarios modeling the extreme stresses encountered during evacuations.
△ Less
Submitted 22 May, 2023;
originally announced May 2023.
-
Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems
Authors:
Akash Harapanahalli,
Saber Jafarpour,
Samuel Coogan
Abstract:
In this paper, we present a contraction-guided adaptive partitioning algorithm for improving interval-valued robust reachable set estimates in a nonlinear feedback loop with a neural network controller and disturbances. Based on an estimate of the contraction rate of over-approximated intervals, the algorithm chooses when and where to partition. Then, by leveraging a decoupling of the neural netwo…
▽ More
In this paper, we present a contraction-guided adaptive partitioning algorithm for improving interval-valued robust reachable set estimates in a nonlinear feedback loop with a neural network controller and disturbances. Based on an estimate of the contraction rate of over-approximated intervals, the algorithm chooses when and where to partition. Then, by leveraging a decoupling of the neural network verification step and reachability partitioning layers, the algorithm can provide accuracy improvements for little computational cost. This approach is applicable with any sufficiently accurate open-loop interval-valued reachability estimation technique and any method for bounding the input-output behavior of a neural network. Using contraction-based robustness analysis, we provide guarantees of the algorithm's performance with mixed monotone reachability. Finally, we demonstrate the algorithm's performance through several numerical simulations and compare it with existing methods in the literature. In particular, we report a sizable improvement in the accuracy of reachable set estimation in a fraction of the runtime as compared to state-of-the-art methods.
△ Less
Submitted 9 December, 2023; v1 submitted 7 April, 2023;
originally announced April 2023.
-
Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers
Authors:
Saber Jafarpour,
Akash Harapanahalli,
Samuel Coogan
Abstract:
This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a l…
▽ More
This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system.
We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method's strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the art verification algorithm for linear discretized systems.
△ Less
Submitted 7 August, 2023; v1 submitted 19 January, 2023;
originally announced January 2023.
-
Monotonicity and Contraction on Polyhedral Cones
Authors:
Saber Jafarpour,
Samuel Coogan
Abstract:
In this note, we study monotone dynamical systems with respect to polyhedral cones. Using the half-space representation and the vertex representation, we propose three equivalent conditions to certify monotonicity of a dynamical system with respect to a polyhedral cone. We then introduce the notion of gauge norm associated with a cone and provide closed-from formulas for computing gauge norms asso…
▽ More
In this note, we study monotone dynamical systems with respect to polyhedral cones. Using the half-space representation and the vertex representation, we propose three equivalent conditions to certify monotonicity of a dynamical system with respect to a polyhedral cone. We then introduce the notion of gauge norm associated with a cone and provide closed-from formulas for computing gauge norms associated with polyhedral cones. A key feature of gauge norms is that contractivity of monotone systems with respect to them can be efficiently characterized using simple inequalities. This result generalizes the well-known criteria for Hurwitzness of Metzler matrices and provides a scalable approach to search for Lyapunov functions of monotone systems with respect to polyhedral cones. Finally, we study the applications of our results in transient stability of dynamic flow networks and in scalable control design with safety guarantees.
△ Less
Submitted 7 August, 2023; v1 submitted 20 October, 2022;
originally announced October 2022.
-
Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach
Authors:
Saber Jafarpour,
Alexander Davydov,
Matthew Abate,
Francesco Bullo,
Samuel Coogan
Abstract:
This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks based upon non-Euclidean contraction theory. The basic idea is to cast the robustness analysis of a neural network as a reachability problem and use (i) the $\ell_{\infty}$-norm input-output Lipschitz constant and (ii) the tight inclusion function of the network to ove…
▽ More
This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks based upon non-Euclidean contraction theory. The basic idea is to cast the robustness analysis of a neural network as a reachability problem and use (i) the $\ell_{\infty}$-norm input-output Lipschitz constant and (ii) the tight inclusion function of the network to over-approximate its reachable sets. First, for a given implicit neural network, we use $\ell_{\infty}$-matrix measures to propose sufficient conditions for its well-posedness, design an iterative algorithm to compute its fixed points, and provide upper bounds for its $\ell_\infty$-norm input-output Lipschitz constant. Second, we introduce a related embedded network and show that the embedded network can be used to provide an $\ell_\infty$-norm box over-approximation of the reachable sets of the original network. Moreover, we use the embedded network to design an iterative algorithm for computing the upper bounds of the original system's tight inclusion function. Third, we use the upper bounds of the Lipschitz constants and the upper bounds of the tight inclusion functions to design two algorithms for the training and robustness verification of implicit neural networks. Finally, we apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.
△ Less
Submitted 7 August, 2022;
originally announced August 2022.
-
Safe Schedule Verification for Urban Air Mobility Networks with Node Closures
Authors:
Qinshuang Wei,
Gustav Nilsson,
Samuel Coogan
Abstract:
In Urban Air Mobility (UAM) networks, takeoff and landing sites, called vertiports, are likely to experience intermittent closures due to, e.g., adverse weather. To ensure safety, all in-flight Urban Air Vehicles (UAVs) in a UAM network must therefore have alternative landing sites with sufficient landing capacity in the event of a vertiport closure. In this paper, we study the problem of safety v…
▽ More
In Urban Air Mobility (UAM) networks, takeoff and landing sites, called vertiports, are likely to experience intermittent closures due to, e.g., adverse weather. To ensure safety, all in-flight Urban Air Vehicles (UAVs) in a UAM network must therefore have alternative landing sites with sufficient landing capacity in the event of a vertiport closure. In this paper, we study the problem of safety verification of UAM schedules in the face of vertiport closures. We first provide necessary and sufficient conditions for a given UAM schedule to be safe in the sense that, if a vertiport closure occurs, then all UAVs will be able to safely land at a backup landing site. Next, we convert these conditions to an efficient algorithm for verifying safety of a UAM schedule via a linear program by using properties of totally unimodular matrices. Our algorithm allows for uncertain travel time between UAM vertiports and scales quadratically with the number of scheduled UAVs. We demonstrate our algorithm on a UAM network with up to 1,000 UAVs.
△ Less
Submitted 26 June, 2022;
originally announced June 2022.
-
Leveraging Heterogeneous Capabilities in Multi-Agent Systems for Environmental Conflict Resolution
Authors:
Michael Enqi Cao,
Jonas Warnke,
Yunhai Han,
Xinpei Ni,
Ye Zhao,
Samuel Coogan
Abstract:
In this paper, we introduce a high-level controller synthesis framework that enables teams of heterogeneous agents to assist each other in resolving environmental conflicts that appear at runtime. This conflict resolution method is built upon temporal-logic-based reactive synthesis to guarantee safety and task completion under specific environment assumptions. In heterogeneous multi-agent systems,…
▽ More
In this paper, we introduce a high-level controller synthesis framework that enables teams of heterogeneous agents to assist each other in resolving environmental conflicts that appear at runtime. This conflict resolution method is built upon temporal-logic-based reactive synthesis to guarantee safety and task completion under specific environment assumptions. In heterogeneous multi-agent systems, every agent is expected to complete its own tasks in service of a global team objective. However, at runtime, an agent may encounter un-modeled obstacles (e.g., doors or walls) that prevent it from achieving its own task. To address this problem, we employ the capabilities of other heterogeneous agents to resolve the obstacle. A controller framework is proposed to redirect agents with the capability of resolving the appropriate obstacles to the required target when such a situation is detected. Three case studies involving a bipedal robot Digit and a quadcopter are used to evaluate the controller performance in action. Additionally, we implement the proposed framework on a physical multi-agent robotic system to demonstrate its viability for real world applications.
△ Less
Submitted 1 September, 2022; v1 submitted 3 June, 2022;
originally announced June 2022.
-
Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks
Authors:
Alexander Davydov,
Saber Jafarpour,
Matthew Abate,
Francesco Bullo,
Samuel Coogan
Abstract:
We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs). INNs are a class of implicit learning models that use implicit equations as layers and have been shown to exhibit several notable benefits over traditional deep neural networks. We first establish that tight inclusion functions of neural networks, which provide the tightest rectangular over-a…
▽ More
We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs). INNs are a class of implicit learning models that use implicit equations as layers and have been shown to exhibit several notable benefits over traditional deep neural networks. We first establish that tight inclusion functions of neural networks, which provide the tightest rectangular over-approximation of an input-output map, lead to sharper robustness guarantees than the well-studied robustness measures of local Lipschitz constants. Like Lipschitz constants, tight inclusions functions are computationally challenging to obtain, and we thus propose using mixed monotonicity and contraction theory to obtain computationally efficient estimates of tight inclusion functions for INNs. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs. We design a novel optimization problem for training robust INNs and we provide empirical evidence that suitably-trained INNs can be more robust than comparably-trained feedforward networks.
△ Less
Submitted 31 March, 2022;
originally announced April 2022.
-
Resilience of Input Metering in Dynamic Flow Networks
Authors:
Saber Jafarpour,
Samuel Coogan
Abstract:
In this paper, we study robustness of input metering policies in dynamic flow networks in the presence of transient disturbances and attacks. We consider a compartmental model for dynamic flow networks with a First-In-First-Out (FIFO) routing rule as found in, e.g., transportation networks. We model the effect of the transient disturbance as an abrupt change to the state of the network and use the…
▽ More
In this paper, we study robustness of input metering policies in dynamic flow networks in the presence of transient disturbances and attacks. We consider a compartmental model for dynamic flow networks with a First-In-First-Out (FIFO) routing rule as found in, e.g., transportation networks. We model the effect of the transient disturbance as an abrupt change to the state of the network and use the notion of the region of attraction to measure the resilience of the network to these changes. For constant and periodic input metering, we introduce the notion of monotone-invariant points to establish inner-estimates for the regions of attraction of free-flow equilibrium points and free-flow periodic orbits using monotone systems theory. These results are applicable to, e.g., networks with cycles, which have not been considered in prior literature on dynamic flow networks with FIFO routing. Finally, we propose two approaches for finding suitable monotone-invariant points in the flow networks with FIFO rules.
△ Less
Submitted 14 March, 2022;
originally announced March 2022.
-
Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstraction
Authors:
Jesse Jiang,
Ye Zhao,
Samuel Coogan
Abstract:
We study the problem of refining satisfiability bounds for partially-known stochastic systems against planning specifications defined using syntactically co-safe Linear Temporal Logic (scLTL). We propose an abstraction-based approach that iteratively generates high-confidence Interval Markov Decision Process (IMDP) abstractions of the system from high-confidence bounds on the unknown component of…
▽ More
We study the problem of refining satisfiability bounds for partially-known stochastic systems against planning specifications defined using syntactically co-safe Linear Temporal Logic (scLTL). We propose an abstraction-based approach that iteratively generates high-confidence Interval Markov Decision Process (IMDP) abstractions of the system from high-confidence bounds on the unknown component of the dynamics obtained via Gaussian process regression. In particular, we develop a synthesis strategy to sample the unknown dynamics by finding paths which avoid specification-violating states using a product IMDP. We further provide a heuristic to choose among various candidate paths to maximize the information gain. Finally, we propose an iterative algorithm to synthesize a satisfying control policy for the product IMDP system. We demonstrate our work with a case study on mobile robot navigation.
△ Less
Submitted 6 May, 2022; v1 submitted 2 February, 2022;
originally announced February 2022.
-
Robustness Certificates for Implicit Neural Networks: A Mixed Monotone Contractive Approach
Authors:
Saber Jafarpour,
Matthew Abate,
Alexander Davydov,
Francesco Bullo,
Samuel Coogan
Abstract:
Implicit neural networks are a general class of learning models that replace the layers in traditional feedforward models with implicit algebraic equations. Compared to traditional learning models, implicit networks offer competitive performance and reduced memory consumption. However, they can remain brittle with respect to input adversarial perturbations.
This paper proposes a theoretical and…
▽ More
Implicit neural networks are a general class of learning models that replace the layers in traditional feedforward models with implicit algebraic equations. Compared to traditional learning models, implicit networks offer competitive performance and reduced memory consumption. However, they can remain brittle with respect to input adversarial perturbations.
This paper proposes a theoretical and computational framework for robustness verification of implicit neural networks; our framework blends together mixed monotone systems theory and contraction theory. First, given an implicit neural network, we introduce a related embedded network and show that, given an $\ell_\infty$-norm box constraint on the input, the embedded network provides an $\ell_\infty$-norm box overapproximation for the output of the given network. Second, using $\ell_{\infty}$-matrix measures, we propose sufficient conditions for well-posedness of both the original and embedded system and design an iterative algorithm to compute the $\ell_{\infty}$-norm box robustness margins for reachability and classification problems. Third, of independent value, we propose a novel relative classifier variable that leads to tighter bounds on the certified adversarial robustness in classification problems. Finally, we perform numerical simulations on a Non-Euclidean Monotone Operator Network (NEMON) trained on the MNIST dataset. In these simulations, we compare the accuracy and run time of our mixed monotone contractive approach with the existing robustness verification approaches in the literature for estimating the certified adversarial robustness.
△ Less
Submitted 9 December, 2021;
originally announced December 2021.
-
The Strong Integral Input-to-State Stability Property in Dynamical Flow Networks
Authors:
Gustav Nilsson,
Samuel Coogan
Abstract:
Dynamical flow networks serve as macroscopic models for, e.g., transportation networks, queuing networks, and distribution networks. While the flow dynamics in such networks follow the conservation of mass on the links, the outflow from each link is often non-linear due to, e.g., flow capacity constraints and simultaneous service rate constraints. Such non-linear constraints imply a limit on the m…
▽ More
Dynamical flow networks serve as macroscopic models for, e.g., transportation networks, queuing networks, and distribution networks. While the flow dynamics in such networks follow the conservation of mass on the links, the outflow from each link is often non-linear due to, e.g., flow capacity constraints and simultaneous service rate constraints. Such non-linear constraints imply a limit on the magnitude of exogenous inflow that is able to be accommodated by the network before it becomes overloaded and its state trajectory diverges. This paper shows how the Strong integral Input-to-State Stability (Strong iISS) property allows for quantifying the effects of the exogenous inflow on the flow dynamics. The Strong iISS property enables a unified stability analysis of classes of dynamical flow networks that were only partly analyzable before, such as networks with cycles, multi-commodity flow networks and networks with non-monotone flow dynamics. We present sufficient conditions on the maximum magnitude of exogenous inflow to guarantee input-to-state stability for a dynamical flow network, and we also present cases when this sufficient condition is necessary. The conditions are exemplified on a few existing dynamical flow network models, specifically, fluid queuing models with time-varying exogenous inflows and multi-commodity flow models.
△ Less
Submitted 18 November, 2021;
originally announced November 2021.
-
Sensitivity to User Mischaracterizations in Electric Vehicle Charging
Authors:
Cesar Santoyo,
Gustav Nilsson,
Samuel Coogan
Abstract:
In this paper, we consider electric vehicle charging facilities that offer various levels of service for varying prices such that rational users choose a level of service that minimizes the total cost to themselves including an opportunity cost that incorporates users' value of time. In this setting, we study the sensitivity of the expected occupancy at the facility to mischaracterizations of user…
▽ More
In this paper, we consider electric vehicle charging facilities that offer various levels of service for varying prices such that rational users choose a level of service that minimizes the total cost to themselves including an opportunity cost that incorporates users' value of time. In this setting, we study the sensitivity of the expected occupancy at the facility to mischaracterizations of user profiles and uncharacterized heterogeneity. For user profile mischaracterizations, we first provide a fundamental upper bound for the difference between the expected occupancy under any two different distributions on a user's impatience (i.e., value of time) that only depends on the minimum and maximum charging rate offered by the charging facility. Next, we consider the case when a user's impatience is a discrete random variable and study the sensitivity of the expected occupancy to the probability masses and attained values of the random variable. We show that the expected occupancy varies linearly with respect to the probability masses and is piecewise constant with respect to the attained values. Furthermore, we study the effects on the expected occupancy from the occurrence of heterogeneous user populations. In particular, we quantify the effect on the expected occupancy from the existence of sub-populations that may only select a subset of the offered service levels. Lastly, we quantify the variability of early departures on the expected occupancy. These results demonstrate how the facility operator might design prices such that the expected occupancy does not vary much under small changes in the distribution of a user's impatience, variable and limited user service needs, or uncharacterized early departure, quantities which are generally difficult to characterize accurately from data. We further demonstrate our results via examples.
△ Less
Submitted 24 November, 2021; v1 submitted 16 November, 2021;
originally announced November 2021.
-
Run Time Assurance for Safety-Critical Systems: An Introduction to Safety Filtering Approaches for Complex Control Systems
Authors:
Kerianne Hobbs,
Mark Mote,
Matthew Abate,
Samuel Coogan,
Eric Feron
Abstract:
Run Time Assurance (RTA) Systems are online verification mechanisms that filter an unverified primary controller output to ensure system safety. The primary control may come from a human operator, an advanced control approach, or an autonomous control approach that cannot be verified to the same level as simpler control systems designs. The critical feature of RTA systems is their ability to alter…
▽ More
Run Time Assurance (RTA) Systems are online verification mechanisms that filter an unverified primary controller output to ensure system safety. The primary control may come from a human operator, an advanced control approach, or an autonomous control approach that cannot be verified to the same level as simpler control systems designs. The critical feature of RTA systems is their ability to alter unsafe control inputs explicitly to assure safety. In many cases, RTA systems can functionally be described as containing a monitor that watches the state of the system and output of a primary controller, and a backup controller that replaces or modifies control input when necessary to assure safety. An important quality of an RTA system is that the assurance mechanism is constructed in a way that is entirely agnostic to the underlying structure of the primary controller. By effectively decoupling the enforcement of safety constraints from performance-related objectives, RTA offers a number of useful advantages over traditional (offline) verification. This article provides a tutorial on develo** RTA systems.
△ Less
Submitted 6 June, 2022; v1 submitted 7 October, 2021;
originally announced October 2021.
-
Model Free Barrier Functions via Implicit Evading Maneuvers
Authors:
Eric Squires,
Rohit Konda,
Samuel Coogan,
Magnus Egerstedt
Abstract:
This paper demonstrates that the safety override arising from the use of a barrier function can in some cases be needlessly restrictive. In particular, we examine the case of fixed-wing collision avoidance and show that when using a barrier function, there are cases where two fixed-wing aircraft can come closer to colliding than if there were no barrier function at all. In addition, we construct c…
▽ More
This paper demonstrates that the safety override arising from the use of a barrier function can in some cases be needlessly restrictive. In particular, we examine the case of fixed-wing collision avoidance and show that when using a barrier function, there are cases where two fixed-wing aircraft can come closer to colliding than if there were no barrier function at all. In addition, we construct cases where the barrier function labels the system as unsafe even when the vehicles start arbitrarily far apart. In other words, the barrier function ensures safety but with unnecessary costs to performance. We therefore introduce model-free barrier functions which take a data driven approach to creating a barrier function. We demonstrate the effectiveness of model-free barrier functions in a collision avoidance simulation of two fixed-wing aircraft.
△ Less
Submitted 23 September, 2022; v1 submitted 27 July, 2021;
originally announced July 2021.
-
Capacity-Constrained Urban Air Mobility Scheduling
Authors:
Qinshuang Wei,
Gustav Nilsson,
Samuel Coogan
Abstract:
This paper studies the problem of scheduling urban air mobility trips when travel times are uncertain and capacity at destinations is limited. Urban air mobility, in which air transportation is used for relatively short trips within a city or region, is emerging as a possible component in future transportation networks. Destinations in urban air mobility networks, called vertiports or vertistops,…
▽ More
This paper studies the problem of scheduling urban air mobility trips when travel times are uncertain and capacity at destinations is limited. Urban air mobility, in which air transportation is used for relatively short trips within a city or region, is emerging as a possible component in future transportation networks. Destinations in urban air mobility networks, called vertiports or vertistops, typically have limited landing capacity, and, for safety, it must be guaranteed that an air vehicle will be able to land before it can be allowed to take off. We first present a tractable model of urban air mobility networks that accounts for limited landing capacity and uncertain travel times between destinations with lower and upper travel time bounds. We then establish theoretical bounds on the achievable throughput of the network. Next, we present a tractable algorithm for scheduling trips to satisfy safety constraints and arrival deadlines. The algorithm allows for dynamically updating the schedule to accommodate, e.g., new demands over time. The paper concludes with case studies that demonstrate the algorithm on two networks.
△ Less
Submitted 1 July, 2021;
originally announced July 2021.
-
On the Impact of the Capacity Drop Phenomenon for Freeway Traffic Flow Control
Authors:
Michael Enqi Cao,
Gustav Nilsson,
Samuel Coogan
Abstract:
Capacity drop is an empirically observed phenomenon in vehicular traffic flow on freeways whereby, after a critical density is reached, a state of congestion sets in, but the freeway does not become decongested again until the density drops well below the critical density. This introduces a hysteresis effect so that it is easier to enter the congested state than to leave it. However, many existing…
▽ More
Capacity drop is an empirically observed phenomenon in vehicular traffic flow on freeways whereby, after a critical density is reached, a state of congestion sets in, but the freeway does not become decongested again until the density drops well below the critical density. This introduces a hysteresis effect so that it is easier to enter the congested state than to leave it. However, many existing first-order models of traffic flow, particularly those used for control design, ignore capacity drop, leading to suboptimal controllers. In this paper, we consider a cell transmission model of traffic flow that incorporates capacity drop to study the problem of optimal freeway ramp metering. We show that, if capacity drop is ignored in the control design, then the resulting controller, obtained via a convex program, may be significantly suboptimal. We then propose an alternative model predictive controller that accounts for capacity drop via a mixed integer linear program and show that, for sufficiently large rollout horizon, this controller is optimal. We also compare these approaches to a heuristic hand-crafted controller that is viewed as a modification of an integral feedback controller to account for capacity drop. This heuristic controller outperforms the controller that ignores capacity drop but underperforms compared to the proposed alternative model predictive controller. These results suggest that it is generally important to include capacity drop in the controller design process, and we demonstrate this insight on several case studies.
△ Less
Submitted 18 June, 2021;
originally announced June 2021.
-
A Numerical Method to Compute Stability Margins of Switching Linear Systems
Authors:
Corbin Klett,
Matthew Abate,
Samuel Coogan,
Eric Feron
Abstract:
Stability margins for linear time-varying (LTV) and switched-linear systems are traditionally computed via quadratic Lyapunov functions, and these functions certify the stability of the system under study. In this work, we show how the more general class of homogeneous polynomial Lyapunov functions is used to compute stability margins with reduced conservatism, and we show how these Lyapunov funct…
▽ More
Stability margins for linear time-varying (LTV) and switched-linear systems are traditionally computed via quadratic Lyapunov functions, and these functions certify the stability of the system under study. In this work, we show how the more general class of homogeneous polynomial Lyapunov functions is used to compute stability margins with reduced conservatism, and we show how these Lyapunov functions aid in the search for periodic trajectories for marginally stable LTV systems. Our work is premised on the recent observation that the search for a homogeneous polynomial Lyapunov function for some LTV systems is easily encoded as the search for a quadratic Lyapunov function for a related LTV system, and our main contribution is an intuitive algorithm for generating upper and lower bounds on the system's stability margin. We show also how the worst-case switching scheme - which draws an LTV system closest to a periodic orbit - is generated. Three numerical examples are provided to aid the reader and demonstrate the theoretical contributions of the work.
△ Less
Submitted 4 December, 2020;
originally announced December 2020.
-
Safety With Limited Range Sensing Constraints For Fixed Wing Aircraft
Authors:
Eric Squires,
Rohit Konda,
Pietro Pierpaoli,
Samuel Coogan,
Magnus Egerstedt
Abstract:
In this paper we discuss how to use a barrier function that is subject to kinematic constraints and limited sensing in order to guarantee that fixed wing unmanned aerial vehicles (UAVs) will maintain safe distances from each other at all times despite being subject to limited range sensing constraints. Prior work has shown that a barrier function can be used to guarantee safe system operation when…
▽ More
In this paper we discuss how to use a barrier function that is subject to kinematic constraints and limited sensing in order to guarantee that fixed wing unmanned aerial vehicles (UAVs) will maintain safe distances from each other at all times despite being subject to limited range sensing constraints. Prior work has shown that a barrier function can be used to guarantee safe system operation when the state can be sensed at all times. However, in this paper we show that this construction does not guarantee safety when the UAVs are subject to limited range sensing. To resolve this issue, we introduce a method for constructing a new barrier function that accommodates limited sensing range from a previously existing barrier function that may not necessarily accommodate limited range sensing. We show that, under appropriate conditions, the newly constructed barrier function ensures system safety even in the presence of limited range sensing. We demonstrate the contribution of this paper in a scenario of 20 fixed wing aircraft, where because of the proposed algorithm, the vehicles are able to maintain safe distances from each other even though the vehicles are subject to limited range sensing.
△ Less
Submitted 9 March, 2021; v1 submitted 21 October, 2020;
originally announced October 2020.
-
Improving the Fidelity of Mixed-Monotone Reachable Set Approximations via State Transformations
Authors:
Matthew Abate,
Samuel Coogan
Abstract:
Mixed-monotone systems are separable via a decomposition function into increasing and decreasing components, and this decomposition function allows for embedding the system dynamics in a higher-order monotone embedding system. Embedding the system dynamics in this way facilitates the efficient over-approximation of reachable sets with hyperrectangles, however, unlike the monotonicity property, whi…
▽ More
Mixed-monotone systems are separable via a decomposition function into increasing and decreasing components, and this decomposition function allows for embedding the system dynamics in a higher-order monotone embedding system. Embedding the system dynamics in this way facilitates the efficient over-approximation of reachable sets with hyperrectangles, however, unlike the monotonicity property, which can be applied to compute, e.g., the tightest hyperrectangle containing a reachable set, the application of the mixed-monotonicity property generally results in conservative reachable set approximations. In this work, explore conservatism in the method and we consider, in particular, embedding systems that are monotone with respect to an alternative partial order. This alternate embedding system is constructed with a decomposition function for a related system, formed via a linear transformation of the initial state-space. We show how these alternate embedding systems allow for computing reachable sets with improved fidelity, i.e., reduced conservatism.
△ Less
Submitted 18 March, 2021; v1 submitted 2 October, 2020;
originally announced October 2020.
-
Resource Aware Pricing for Electric Vehicle Charging
Authors:
Cesar Santoyo,
Gustav Nilsson,
Samuel Coogan
Abstract:
Electric vehicle charging facilities offer electric charge and parking to users for a fee. Both parking availability and electric charge capacity are constrained resources, and as the demand for charging facilities grows with increasing electric vehicle adoption, so too does the potential for exceeding these resource limitations. In this paper, we study how prices set by the charging facility impa…
▽ More
Electric vehicle charging facilities offer electric charge and parking to users for a fee. Both parking availability and electric charge capacity are constrained resources, and as the demand for charging facilities grows with increasing electric vehicle adoption, so too does the potential for exceeding these resource limitations. In this paper, we study how prices set by the charging facility impact the likelihood that resource constraints are exceeded. Specifically, we present probabilistic bounds on the number of charging spots and the total power supply needed at a facility based on the characteristics of the arriving vehicles. We assume the charging facility either offers a set of distinct and fixed charging rates to each user or allows the user to decide a charging deadline, from which a charging rate is determined. Users arrive randomly, requiring a random amount of charge. Additionally, each user has a random impatience factor that quantifies their value of time, and a random desired time to stay at a particular location. Assuming rational user behavior, and with knowledge of the probability distribution of the random parameters, we present high-confidence bounds on the total number of vehicles parked at the station and the aggregate power use of all vehicles actively charging. We demonstrate how these bounds can be used by a charging facility to determine appropriate prices and investigate through a Monte-Carlo simulation case study the tightness of the bounds.
△ Less
Submitted 22 September, 2020;
originally announced September 2020.
-
Performance Analysis and Non-Quadratic Lyapunov Functions for Linear Time-Varying Systems
Authors:
Matthew Abate,
Corbin Klett,
Samuel Coogan,
Eric Feron
Abstract:
Performance analysis for linear time-invariant (LTI) systems has been closely tied to quadratic Lyapunov functions ever since it was shown that LTI system stability is equivalent to the existence of such a Lyapunov function. Some metrics for LTI systems, however, have resisted treatment via means of quadratic Lyapunov functions. Among these, point-wise-in-time metrics, such as peak norms, are not…
▽ More
Performance analysis for linear time-invariant (LTI) systems has been closely tied to quadratic Lyapunov functions ever since it was shown that LTI system stability is equivalent to the existence of such a Lyapunov function. Some metrics for LTI systems, however, have resisted treatment via means of quadratic Lyapunov functions. Among these, point-wise-in-time metrics, such as peak norms, are not captured accurately using these techniques, and this shortcoming has prevented the development of tools to analyze system behavior by means other than e.g. time-domain simulations. This work demonstrates how the more general class of homogeneous polynomial Lyapunov functions can be used to approximate point-wise-in-time behavior for LTI systems with greater accuracy, and we extend this to the case of linear time-varying (LTV) systems as well. Our findings rely on the recent observation that the search for homogeneous polynomial Lyapunov functions for LTV systems can be recast as a search for quadratic Lyapunov functions for a related hierarchy of time-varying Lyapunov differential equations; thus, performance guarantees for LTV systems are attainable without heavy computation. Numerous examples are provided to demonstrate the findings of this work.
△ Less
Submitted 10 September, 2020; v1 submitted 1 September, 2020;
originally announced September 2020.
-
Enforcing Safety at Runtime for Systems with Disturbances
Authors:
Matthew Abate,
Samuel Coogan
Abstract:
Safety for control systems is often posed as an invariance constraint; the system is said to be safe if state trajectories avoid some unsafe region of the statespace for all time. An assured controller is one that enforces safety online by filtering a desired control input at runtime, and control barrier functions (CBFs) provide an assured controller that renders a safe subset of the state-space f…
▽ More
Safety for control systems is often posed as an invariance constraint; the system is said to be safe if state trajectories avoid some unsafe region of the statespace for all time. An assured controller is one that enforces safety online by filtering a desired control input at runtime, and control barrier functions (CBFs) provide an assured controller that renders a safe subset of the state-space forward invariant. Recent extensions propose CBF-based assured controllers that allow the system to leave a known safe set so long as a given backup control strategy eventually returns to the safe set, however, these methods have yet to be extended to consider systems subjected to unknown disturbance inputs.
In this work, we present a problem formulation for CBF-based runtime assurance for systems with disturbances, and controllers which solve this problem must, in some way, incorporate the online computation of reachable sets. In general, computing reachable sets in the presence of disturbances is computationally costly and cannot be directly incorporated in a CBF framework. To that end, we present a particular solution to the problem, whereby reachable sets are approximated via the mixed-monotonicity property. Efficient algorithms exist for overapproximating reachable sets for mixed-monotone systems with hyperrectangles, and we show that such approximations are suitable for incorporating into a CBF-based runtime assurance framework.
△ Less
Submitted 16 August, 2020;
originally announced August 2020.
-
Continuous Reachability Task Transition Using Control Barrier Functions
Authors:
Mohit Srinivasan,
Cesar Santoyo,
Samuel Coogan
Abstract:
In this paper, a method to achieve smooth transitions between sequential reachability tasks for a continuous time mobile robotic system is presented. Control barrier functions provide formal guarantees of forward invariance of safe sets and finite-time reachability and are able to enforce task execution. Barrier functions used in quadratic programs result in implementation of controllers with real…
▽ More
In this paper, a method to achieve smooth transitions between sequential reachability tasks for a continuous time mobile robotic system is presented. Control barrier functions provide formal guarantees of forward invariance of safe sets and finite-time reachability and are able to enforce task execution. Barrier functions used in quadratic programs result in implementation of controllers with real-time performance guarantees. Existing approaches for multi-objective task execution using control barrier functions leverage discretely switched, sequential quadratic programs to achieve successive tasks. However, discrete switching can lead to control input discontinuities which can affect a robot's performance. Hence, we propose a method which ensures continuous transitions between sequential quadratic programs. In particular, a time varying component to the barrier function constraint is introduced which allows for a smooth transition between objectives. Robotic implementation results are also provided.
△ Less
Submitted 25 May, 2020;
originally announced May 2020.
-
Tight Decomposition Functions for Continuous-Time Mixed-Monotone Systems with Disturbances
Authors:
Matthew Abate,
Maxence Dutreix,
Samuel Coogan
Abstract:
The vector field of a mixed-monotone system is decomposable via a decomposition function into increasing (cooperative) and decreasing (competitive) components, and this decomposition allows for, e.g., efficient computation of reachable sets and forward invariant sets. A main challenge in this approach, however, is identifying an appropriate decomposition function. In this work, we show that any co…
▽ More
The vector field of a mixed-monotone system is decomposable via a decomposition function into increasing (cooperative) and decreasing (competitive) components, and this decomposition allows for, e.g., efficient computation of reachable sets and forward invariant sets. A main challenge in this approach, however, is identifying an appropriate decomposition function. In this work, we show that any continuous-time dynamical system with a Lipschitz continuous vector field is mixed-monotone, and we provide a construction for the decomposition function that yields the tightest approximation of reachable sets when used with the standard tools for mixed-monotone systems. Our construction is similar to that recently proposed by Yang and Ozay for computing decomposition functions of discrete-time systems [1] where we make appropriate modifications for the continuous-time setting and also extend to the case with unknown disturbance inputs. As in [1], our decomposition function construction requires solving an optimization problem for each point in the state-space; however, we demonstrate through example how tight decomposition functions can sometimes be calculated in closed form. As a second contribution, we show how under-approximations of reachable sets can be efficiently computed via the mixed-monotonicity property by considering the backward-time dynamics.
△ Less
Submitted 21 May, 2020; v1 submitted 17 March, 2020;
originally announced March 2020.
-
Computing Robustly Forward Invariant Sets for Mixed-Monotone Systems
Authors:
Matthew Abate,
Samuel Coogan
Abstract:
This work presents new tools for studying reachability and set invariance for continuous-time mixed-monotone dynamical systems subject to a disturbance input. The vector field of a mixed-monotone system is decomposable via a decomposition function into increasing and decreasing components, and this decomposition enables embedding the original dynamics in a higher-dimensional embedding system. Whil…
▽ More
This work presents new tools for studying reachability and set invariance for continuous-time mixed-monotone dynamical systems subject to a disturbance input. The vector field of a mixed-monotone system is decomposable via a decomposition function into increasing and decreasing components, and this decomposition enables embedding the original dynamics in a higher-dimensional embedding system. While the original system is subject to an unknown disturbance input, the embedding system has no disturbances and its trajectories provide bounds for finite-time reachable sets of the original dynamics. Our main contribution is to show how one can efficiently identify robustly forward invariant and attractive sets for mixed-monotone systems by studying certain equilibria of this embedding system. We show also how this approach, when applied to the backward-time dynamics, establishes different robustly forward invariant sets for the original dynamics. Lastly, we present an independent result for computing decomposition functions for systems with polynomial dynamics. These tools and results are demonstrated through several examples and a case study.
△ Less
Submitted 21 August, 2020; v1 submitted 12 March, 2020;
originally announced March 2020.
-
Synthesis of Control Barrier Functions Using a Supervised Machine Learning Approach
Authors:
Mohit Srinivasan,
Amogh Dabholkar,
Samuel Coogan,
Patricio Vela
Abstract:
Control barrier functions are mathematical constructs used to guarantee safety for robotic systems. When integrated as constraints in a quadratic programming optimization problem, instantaneous control synthesis with real-time performance demands can be achieved for robotics applications. Prevailing use has assumed full knowledge of the safety barrier functions, however there are cases where the s…
▽ More
Control barrier functions are mathematical constructs used to guarantee safety for robotic systems. When integrated as constraints in a quadratic programming optimization problem, instantaneous control synthesis with real-time performance demands can be achieved for robotics applications. Prevailing use has assumed full knowledge of the safety barrier functions, however there are cases where the safe regions must be estimated online from sensor measurements. In these cases, the corresponding barrier function must be synthesized online. This paper describes a learning framework for estimating control barrier functions from sensor data. Doing so affords system operation in unknown state space regions without compromising safety. Here, a support vector machine classifier provides the barrier function specification as determined by sets of safe and unsafe states obtained from sensor measurements. Theoretical safety guarantees are provided. Experimental ROS-based simulation results for an omnidirectional robot equipped with LiDAR demonstrate safe operation.
△ Less
Submitted 10 March, 2020;
originally announced March 2020.
-
A review of machine learning applications in wildfire science and management
Authors:
Piyush Jain,
Sean C P Coogan,
Sriram Ganapathi Subramanian,
Mark Crowley,
Steve Taylor,
Mike D Flannigan
Abstract:
Artificial intelligence has been applied in wildfire science and management since the 1990s, with early applications including neural networks and expert systems. Since then the field has rapidly progressed congruently with the wide adoption of machine learning (ML) in the environmental sciences. Here, we present a sco** review of ML in wildfire science and management. Our objective is to improv…
▽ More
Artificial intelligence has been applied in wildfire science and management since the 1990s, with early applications including neural networks and expert systems. Since then the field has rapidly progressed congruently with the wide adoption of machine learning (ML) in the environmental sciences. Here, we present a sco** review of ML in wildfire science and management. Our objective is to improve awareness of ML among wildfire scientists and managers, as well as illustrate the challenging range of problems in wildfire science available to data scientists. We first present an overview of popular ML approaches used in wildfire science to date, and then review their use in wildfire science within six problem domains: 1) fuels characterization, fire detection, and map**; 2) fire weather and climate change; 3) fire occurrence, susceptibility, and risk; 4) fire behavior prediction; 5) fire effects; and 6) fire management. We also discuss the advantages and limitations of various ML approaches and identify opportunities for future advances in wildfire science and management within a data science context. We identified 298 relevant publications, where the most frequently used ML methods included random forests, MaxEnt, artificial neural networks, decision trees, support vector machines, and genetic algorithms. There exists opportunities to apply more current ML methods (e.g., deep learning and agent based learning) in wildfire science. However, despite the ability of ML models to learn on their own, expertise in wildfire science is necessary to ensure realistic modelling of fire processes across multiple scales, while the complexity of some ML methods requires sophisticated knowledge for their application. Finally, we stress that the wildfire research and management community plays an active role in providing relevant, high quality data for use by practitioners of ML methods.
△ Less
Submitted 19 August, 2020; v1 submitted 1 March, 2020;
originally announced March 2020.
-
Abstraction-based Synthesis for Stochastic Systems with Omega-Regular Objectives
Authors:
Maxence Dutreix,
Jeongmin Huh,
Samuel Coogan
Abstract:
This paper studies the synthesis of controllers for discrete-time, continuous state stochastic systems subject to omega-regular specifications using finite-state abstractions. We present a synthesis algorithm for minimizing or maximizing the probability that a discrete-time stochastic system with finite number of modes satisfies an omega-regular property. Our approach uses a finite-state abstracti…
▽ More
This paper studies the synthesis of controllers for discrete-time, continuous state stochastic systems subject to omega-regular specifications using finite-state abstractions. We present a synthesis algorithm for minimizing or maximizing the probability that a discrete-time stochastic system with finite number of modes satisfies an omega-regular property. Our approach uses a finite-state abstraction of the underlying dynamics in the form of a Bounded-parameter Markov Decision Process (BMDP) arising from a finite partition of the system's domain. Such abstractions allow for a range of transition probabilities between states for each action. Our method analyzes the product between the abstraction and a Deterministic Rabin Automaton encoding the specification. Synthesis is decomposed into a qualitative problem, where the greatest permanent winning components of the product are created, and a quantitative problem, which requires maximizing the probability of reaching this component. We propose a metric for the quality of the controller with respect to the abstracted states and devise a domain partition refinement technique to reach a quality target. Next, we present a method for computing controllers for stochastic systems with a continuous input set. The system is assumed to be affine in input and disturbance, and we derive a technique for solving the qualitative and quantitative problems in the abstractions of such systems called Controlled Interval-valued Markov Chains. The greatest permanent component of such abstractions are found by partitioning the input space to generate a BMDP accounting for all possible qualitative transitions between states. Maximizing the probability of reaching this component is cast as an optimization problem. Quality of the synthesized controller and a refinement scheme are described for this framework.
△ Less
Submitted 21 September, 2020; v1 submitted 24 January, 2020;
originally announced January 2020.
-
Extent-Compatible Control Barrier Functions
Authors:
Mohit Srinivasan,
Matthew Abate,
Gustav Nilsson,
Samuel Coogan
Abstract:
Safety requirements in dynamical systems are commonly enforced with set invariance constraints over a safe region of the state space. Control barrier functions, which are Lyapunov-like functions for guaranteeing set invariance, are an effective tool to enforce such constraints and guarantee safety when the system is represented as a point in the state space. In this paper, we introduce extent-comp…
▽ More
Safety requirements in dynamical systems are commonly enforced with set invariance constraints over a safe region of the state space. Control barrier functions, which are Lyapunov-like functions for guaranteeing set invariance, are an effective tool to enforce such constraints and guarantee safety when the system is represented as a point in the state space. In this paper, we introduce extent-compatible control barrier functions as a tool to enforce safety for the system including its volume (extent) in the physical world. In order to implement the extent-compatible control barrier functions framework, a sum-of-squares based optimization program is proposed. Since sum-of-squares programs can be computationally prohibitive, we additionally introduce a sampling based method in order to retain the computational advantage of a traditional barrier function based quadratic program controller. We prove that the proposed sampling based controller retains the guarantee for safety. Simulation and robotic implementation results are also provided.
△ Less
Submitted 20 January, 2020;
originally announced January 2020.
-
Optimal Tolling for Heterogeneous Traffic Networks with Mixed Autonomy
Authors:
Daniel A. Lazar,
Samuel Coogan,
Ramtin Pedarsani
Abstract:
When people pick routes to minimize their travel time, the total experienced delay, or social cost, may be significantly greater than if people followed routes assigned to them by a social planner. This effect is accentuated when human drivers share roads with autonomous vehicles. When routed optimally, autonomous vehicles can make traffic networks more efficient, but when acting selfishly, the in…
▽ More
When people pick routes to minimize their travel time, the total experienced delay, or social cost, may be significantly greater than if people followed routes assigned to them by a social planner. This effect is accentuated when human drivers share roads with autonomous vehicles. When routed optimally, autonomous vehicles can make traffic networks more efficient, but when acting selfishly, the introduction of autonomous vehicles can actually worsen congestion. We seek to mitigate this effect by influencing routing choices via tolling. We consider a network of parallel roads with affine latency functions that are heterogeneous, meaning that the increase in capacity due to to the presence of autonomous vehicles may vary from road to road. We show that if human drivers and autonomous users have the same tolls, the social cost may be arbitrarily worse than when optimally routed. We then prove qualities of the optimal routing and use them to design tolls that are guaranteed to minimize social cost at equilibrium. To the best of our knowledge, this is the first tolling scheme that yields a unique socially optimal equilibrium for parallel heterogeneous network with affine latency functions.
△ Less
Submitted 25 September, 2019;
originally announced September 2019.
-
A Barrier Function Approach to Finite-Time Stochastic System Verification and Control
Authors:
Cesar Santoyo,
Maxence Dutreix,
Samuel Coogan
Abstract:
This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite-time horizon. We use stochastic control barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the expected value of the barrier function over the time horizon is recast as a sum-of…
▽ More
This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite-time horizon. We use stochastic control barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the expected value of the barrier function over the time horizon is recast as a sum-of-squares optimization problem for efficient numerical computation. Unlike prior works, the proposed certificate condition includes a state-dependent upper bound on the evolution of the expectation. We present formulations for both continuous-time and discrete-time systems. Moreover, for systems for which the drift dynamics are affine-in-control, we propose a method for synthesizing polynomial state feedback controllers that achieve a specified probability of safety. Several case studies are presented which benchmark and illustrate the performance of our verification and control method in the continuous-time and discrete-time domains.
△ Less
Submitted 9 September, 2019;
originally announced September 2019.
-
Mixed Autonomy in Ride-Sharing Networks
Authors:
Qinshuang Wei,
Ramtin Pedarsani,
Samuel Coogan
Abstract:
We consider ride-sharing networks served by human-driven vehicles (HVs) and autonomous vehicles (AVs). We propose a model for ride-sharing in this mixed autonomy setting for a multi-location network in which a ride-sharing platform sets prices for riders, compensations for drivers of HVs, and operates AVs for a fixed price with the goal of maximizing profits. When there are more vehicles than ride…
▽ More
We consider ride-sharing networks served by human-driven vehicles (HVs) and autonomous vehicles (AVs). We propose a model for ride-sharing in this mixed autonomy setting for a multi-location network in which a ride-sharing platform sets prices for riders, compensations for drivers of HVs, and operates AVs for a fixed price with the goal of maximizing profits. When there are more vehicles than riders at a location, we consider three vehicle-to-rider assignment possibilities: rides are assigned to HVs first; rides are assigned to AVs first; rides are assigned in proportion to the number of available HVs and AVs. Next, for each of these priority possibilities, we establish a nonconvex optimization problem characterizing the optimal profits for a network operating at a steady-state equilibrium. We then provide a convex problem which we show to have the same optimal profits, allowing for efficient computation of equilibria, and we show that all three priority possibilities result in the same maximum profits for the platform. Next, we show that, in some cases, there is a regime for which the platform will choose to mix HVs and AVs in order to maximize its profit, while in other cases, the platform will use only HVs or only AVs, depending on the relative cost of AVs. For a specific class of networks, we fully characterize these thresholds analytically and demonstrate our results on an example.
△ Less
Submitted 4 February, 2020; v1 submitted 29 August, 2019;
originally announced August 2019.
-
Characterizing Safety: Minimal Barrier Functions from Scalar Comparison Systems
Authors:
Rohit Konda,
Aaron D. Ames,
Samuel Coogan
Abstract:
Verifying set invariance has classical solutions stemming from the seminal work by Nagumo, and defining sets via a smooth barrier function constraint inequality results in computable flow conditions for guaranteeing set invariance. While a majority of these historic results on set invariance consider flow conditions on the boundary, recent results on control barrier functions extended these condit…
▽ More
Verifying set invariance has classical solutions stemming from the seminal work by Nagumo, and defining sets via a smooth barrier function constraint inequality results in computable flow conditions for guaranteeing set invariance. While a majority of these historic results on set invariance consider flow conditions on the boundary, recent results on control barrier functions extended these conditions to the entire set, although they required regularity conditions on the barrier function. This paper fully characterizes set invariance through \emph{minimal barrier functions} by directly appealing to a comparison result to define a flow condition over the entire domain of the system. A considerable benefit of this approach is the removal of regularity assumptions of the barrier function. This paper also outlines necessary and sufficient conditions for a valid differential inequality condition, giving the minimum conditions for this type of approach. We also show when minimal barrier functions are necessary and sufficient for set invariance.
△ Less
Submitted 24 May, 2020; v1 submitted 25 August, 2019;
originally announced August 2019.
-
Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications
Authors:
Mohit Srinivasan,
Samuel Coogan
Abstract:
In this paper, we propose a framework for the control of mobile robots subject to temporal logic specifications using barrier functions. Complex task specifications can be conveniently encoded using linear temporal logic. In particular, we consider a fragment of linear temporal logic which encompasses a large class of motion planning specifications for a robotic system. Control barrier functions h…
▽ More
In this paper, we propose a framework for the control of mobile robots subject to temporal logic specifications using barrier functions. Complex task specifications can be conveniently encoded using linear temporal logic. In particular, we consider a fragment of linear temporal logic which encompasses a large class of motion planning specifications for a robotic system. Control barrier functions have recently emerged as a convenient tool to guarantee reachability and safety for a system. In addition, they can be encoded as affine constraints in a quadratic program. In this paper, a fully automatic framework which translates a user defined specification in temporal logic to a sequence of barrier function based quadratic programs is presented. In addition, with the aim of alleviating infeasibility scenarios, we propose methods for composition of barrier functions as well as a prioritization based control method to guarantee feasibility of the controller. We prove that the resulting system trajectory synthesized by the proposed controller satisfies the given specification. Robotic simulation and experimental results are provided in addition to the theoretical framework.
△ Less
Submitted 28 March, 2020; v1 submitted 13 August, 2019;
originally announced August 2019.
-
Monitor-Based Runtime Assurance for Temporal Logic Specifications
Authors:
Matthew Abate,
Eric Feron,
Samuel Coogan
Abstract:
This paper introduces the safety controller architecture as a runtime assurance mechanism for system specifications expressed as safety properties in Linear Temporal Logic (LTL). The safety controller has three fundamental components: a performance controller, a backup controller, and an assurance mechanism. The assurance mechanism uses a monitor, constructed as a finite state machine (FSM), to an…
▽ More
This paper introduces the safety controller architecture as a runtime assurance mechanism for system specifications expressed as safety properties in Linear Temporal Logic (LTL). The safety controller has three fundamental components: a performance controller, a backup controller, and an assurance mechanism. The assurance mechanism uses a monitor, constructed as a finite state machine (FSM), to analyze a suggested performance control input and search for system trajectories that are bad prefixes of the system specification. A fault flag from the assurance mechanism denotes a potentially dangerous future system state and triggers a sequence of inputs that is guaranteed to keep the system safe for all time. A case study is presented which details the construction and implementation of a safety controller on a non-deterministic cyber-physical system.
△ Less
Submitted 8 August, 2019;
originally announced August 2019.
-
A Sequential Composition Framework for Coordinating Multi-Robot Behaviors
Authors:
Pietro Pierpaoli,
Anqi Li,
Mohit Srinivasan,
Xiaoyi Cai,
Samuel Coogan,
Magnus Egerstedt
Abstract:
A number of coordinated behaviors have been proposed for achieving specific tasks for multi-robot systems. However, since most applications require more than one such behavior, one needs to be able to compose together sequences of behaviors while respecting local information flow constraints. Specifically, when the inter-agent communication depends on inter-robot distances, these constraints trans…
▽ More
A number of coordinated behaviors have been proposed for achieving specific tasks for multi-robot systems. However, since most applications require more than one such behavior, one needs to be able to compose together sequences of behaviors while respecting local information flow constraints. Specifically, when the inter-agent communication depends on inter-robot distances, these constraints translate into particular configurations that must be reached in finite time in order for the system to be able to transition between the behaviors. To this end, we develop a distributed framework based on finite-time convergence control barrier functions that enables a team of robots to adjust its configuration in order to meet the communication requirements for the different tasks. In order to demonstrate the significance of the proposed framework, we implemented a full-scale scenario where a team of eight planar robots explore an urban environment in order to localize and rescue a subject.
△ Less
Submitted 2 March, 2020; v1 submitted 17 July, 2019;
originally announced July 2019.
-
Lyapunov Differential Equation Hierarchy and Polynomial Lyapunov Functions for Switched Linear Systems
Authors:
Matthew Abate,
Corbin Klett,
Samuel Coogan,
Eric Feron
Abstract:
This work studies the problem of searching for homogeneous polynomial Lyapunov functions for stable switched linear systems. Specifically, we show an equivalence between polynomial Lyapunov functions for systems of this class and quadratic Lyapunov functions for a related hierarchy of Lyapunov differential equations. This creates an intuitive procedure for checking the stability properties of swit…
▽ More
This work studies the problem of searching for homogeneous polynomial Lyapunov functions for stable switched linear systems. Specifically, we show an equivalence between polynomial Lyapunov functions for systems of this class and quadratic Lyapunov functions for a related hierarchy of Lyapunov differential equations. This creates an intuitive procedure for checking the stability properties of switched linear systems and a computationally competitive algorithm is presented for generating high-order homogeneous polynomial Lyapunov functions in this manner. Additionally, we provide a comparison between polynomial Lyapunov functions generated with our proposed approach and polynomial Lyapunov functions generated with a more traditional sum-of-squares based approach.
△ Less
Submitted 18 February, 2020; v1 submitted 11 June, 2019;
originally announced June 2019.