Graduate Work

M. Abate, M. Mote, M. Dor, C. Klett, S. Phillips, K. Lang, P. Tsiotras, E. Feron, and S. Coogan

Abstract

This article presents a comprehensive development and testing of a run time assurance (RTA) filter for a torque-controlled spacecraft in free rotational motion with torque actuation limits for which the objective is to enforce a line-of-sight constraint. A nondeterministic dynamical model is considered for the spacecraft that accounts for disturbance torques, and a guaranteed safe RTA filter is constructed using recent results from mixed monotone systems theory for reachable set overapproximations and optimization-based computation of invariant sets. The RTA filter ensures that the system is always within reach of an a priori safe terminal set by computing reachable sets of the dynamics online at run time. The approach is demonstrated on the Autonomous Spacecraft Testing of Robotic Operations in Space (ASTROS) platform at the Georgia Institute of Technology, Atlanta, GA, USA. In the experiment, potentially unsafe inputs are provided by a human, and the RTA filter overrides the human-commanded inputs when necessary to guarantee safety. The controller update rate for the ASTROS platform is about 10 Hz, while the RTA filter requires about 1 ms of computation time per controller update.

H. Abdelraouf, E. Feron, C. Klett, M. Abate, and S. Coogan

Abstract

A method for constructing homogeneous polynomial Lyapunov functions is presented for linear time-varying or switched-linear systems and the class of nonlinear systems that can be represented as such. The method uses a simple recursion based on the Kronecker product to generate a hierarchy of related dynamical systems, whose first element is the system under study and the second element is the well-known Lyapunov differential equation. It is then proven that a quadratic Lyapunov function for the system at one level in the hierarchy, which can be found via semidefinite programming, is a homogeneous polynomial Lyapunov function for the system at the base level in the hierarchy. Searching for Lyapunov functions of the foregoing kind is equivalent to searching for homogeneous polynomial Lyapunov functions via the formulation of sum-of-squares programs. The quadratic perspective presented in this paper enables the easy development of procedures to compute bounds on pointwise-in-time system metrics, such as peak norms, system stability margins, and many other performance measures. The applications of the theory to analyzing an aircraft model, on the one hand, and an experimental aerospace vehicle, on the other hand, are presented. The theory can be comprehended with a first course on state-space control systems and an elementary knowledge of convex programming.

K. Hobbs, M. Mote, M. Abate, S. Coogan, and E. 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 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 developing RTA systems.

Cover article.

M. Abate and S. Coogan

Abstract

Safety for dynamical systems is often posed as an invariance constraint, requiring the system trajectory to remain in some safe subset of the state-space for all time. This note presents new tools for studying reachability and set invariance for nondeterministic systems subject to a disturbance input using the theory of mixed-monotone dynamical systems. The vector field of a mixed-monotone system is characterized as being decomposable into increasing and decreasing components, which allows the dynamics to be embedded in a higher dimensional embedding system. Even though the original system is nondeterministic due to the unknown disturbance input, the embedding system has no disturbance and a single simulation of the embedding system provides bounds for reachable sets of the original dynamics. In this article, we present an efficient method for identifying robustly forward invariant and attractive sets for mixed-monotone systems by studying equilibria and their stability properties of the corresponding embedding system. We show how this approach can be applied to either the backward-time dynamics or a set of linearly transformed dynamics to establish different robustly forward invariant sets for the original dynamics, and we show also how periodic solutions to the embedding system establish invariant regions for the original dynamics as well. The findings of this work are demonstrated through two numerical examples and two case studies, including a five-dimensional planar quadrotor system.

M. Abate and S. Coogan

Abstract

A dynamical system is mixed monotone when there exists a related decomposition function that separates the system dynamics into cooperative and competitive state interactions. Such a decomposition enables, e.g. , efficient computation of robust reachable sets and forward invariant sets, but obtaining a decomposition function can be challenging. In this letter, we present a method for obtaining a decomposition function for a system that can be represented as an interconnection of subsystems with known decomposition functions. We further extend this approach using tools from interval reachability analysis to accommodate systems with outputs and we provide also conditions for when the system's unique tight decomposition function is obtained via this approach. We demonstrate this methodology for computing decomposition functions with an example of a 3-dimensional unicycle model and with a case study of a 7-dimensional nonlinear spacecraft system defined as an interconnection of subsystems and feedback controllers. Reachable sets for the systems are then computed using their decomposition functions and the standard tools from mixed monotone systems theory.

M. Srinivasan, M. Abate, G. Nilsson and S. 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-compatible control barrier functions as a tool to enforce safety for the system explicitly accounting for its volume (extent) within an ambient workspace. In order to implement the extent-compatible control barrier functions framework, we first propose a sum-of-squares optimization program that is solved pointwise in time to ensure safety. Since sum-of-squares programs can be computationally prohibitive, we next propose an approach that instead considers a finite number of points sampled on the extent boundary. The result is a quadratic program for guaranteed safety that retains the computational advantage of traditional barrier functions. While this alternative is generally more conservative than the sum-of-squares approach, we show that conservatism is reduced by increasing the number of sampled points. Simulation and robotic implementation results are provided.

M. Abate, W. Stuckey, L. Lerner, E. Feron and S. Coogan

Abstract

This paper studies the problem of controlling finite nondeterministic transition systems to satisfy constraints given as linear temporal logic properties. A controller architecture is proposed that maps finite fragments of the state trajectory history to control inputs. This approach avoids the standard controller construction that employs an onboard automaton which is fragile to memory loss or errors. In contrast, the proposed architecture requires storing only a finite sequence of previous system states in memory and is therefore resilient to memory loss. In particular, the system will operate unaltered after such a memory-loss event once the system recollects this finite sequence of system states. A generalised algorithm is outlined for controller synthesis in this manner. Additionally, we demonstrate the construction and implementation of such a memory-loss resilient controller through an experimental demonstration on a differential-drive robot that experiences memory-loss events.

M. Abate, M. Dutreix and S. 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 letter, 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 where we make appropriate modifications for the continuous-time setting and also extend to the case with unknown disturbance inputs. As in Yang's and Ozay's work, 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.

D. Wang, N. Hu, S. Huang, A. M. Nasab, K. Yang, M. Abate, X. Yu, L. Tan, W. Shan, Z. Chen

Abstract

Many biological and engineered systems can be modeled as buckled thin rods with constraints. Examples include microtubules in cytoskeleton, plant roots in soil, and oil pipes within a wellbore. However, most previous studies focused on the buckling of a rod in a homogeneous environment, an idealization which is often not realistic. Here, we study the buckling behaviors of an elastic rod embedded in a bilayer elastic matrix using a combined experimental, theoretical, and computational method. Our experiments showed, for the first time, that the buckling amplitude can increase from the end where the compressive load is applied. To interpret this new phenomenon, we built a theoretical model and identified an ansatz for the transverse displacement. Our numerical results showed that material inhomogeneity, geometry, and loading all have significant influences on the post-buckling behaviors of the rod. Moreover, our study indicated that the stiffer layer of the elastic medium can be treated as a clamped boundary. These results could find applications ranging from the penetration of needles through biological tissues to the development of underground structures.

A. Frommer, M. Abate, P. Rivera-Ortiz, and Y. Diaz-Mercado

Abstract

This paper proposes a capture strategy for a team of pursuers to capture a fast evader with uncertain dynamics in a 3D reach avoid game. The strategy involves coordinating the agents motion to spread out and cut of all possible routes to the evader's target. These routes are obtained by estimating the evader's reachable set using mixed monotone reachable set theory. The reachable set is used to determine a capture surface, over which embedded guidance reference points are provided for the pursuers through 2D coverage. The capture strategy is demonstrated via simulation. Results suggest that capture performance improves with an increase in pursuer team size. Further, the strategy is able to outperform a pure-pursuit strategy when there is a sufficient number of pursuers to fully cover the obtained capture surface.

A. Davydov, S. Jafarpour, M. Abate, F. Bullo, and S. 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-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.

S. Jafarpour*, A. Davydov*, M. Abate, F. Bullo and S. 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 ℒ_∞-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 l∞-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 ℒ_∞-norm input-output Lipschitz constant. Second, we introduce a related embedded network and show that the embedded network can be used to provide an ℒ_∞-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.

S. Jafarpour*, M. Abate*, A. Davydov*, F. Bullo and S. 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 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 ℒ_∞-norm box constraint on the input, the embedded network provides an ℒ_∞-norm box over-approximation for the output of the given network. Second, using ℒ_∞-matrix measures, we propose sufficient conditions for well-posedness of both the original and embedded system and design an iterative algorithm to compute the ℒ_∞-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.

Selected for Oral Presentation (Top 10% of submissions).

C. Llanes, M. Abate and S. Coogan

Abstract

We present a runtime assurance (RTA) mechanism for ensuring safety of a controlled dynamical system and an application to collision avoidance of two unmanned aerial vehicles (UAVs). We consider a dynamical system controlled by an unverified and potentially unsafe primary controller that might, e.g., lead to collision. The proposed RTA mechanism computes at each time the reachable set of the system under a backup control law. We then develop a novel optimization problem based on control barrier functions that filters the primary controller when necessary in order to keep the system’s reachable set within reach of a known, but conservative, safe region. The theory of mixed monotone systems is leveraged for efficient reachable set computation and to achieve a tractable optimization formulation. We demonstrate the proposed RTA mechanism on a dual multirotor UAV case study which requires a fast controller update rate as a result of the small time-scale rotational dynamics. In implementation, the algorithm computes the reachable set of an eight dimensional dynamical system in less than five milliseconds and solves the optimization problem in under one millisecond, yielding a controller update rate of 100Hz.

C. Llanes, M. Abate and S. Coogan

Abstract

We demonstrate a methodology for achieving safe autonomy that relies on computing reachable sets at runtime. Given a system subject to disturbances controlled by an unverified and potentially faulty controller, this methodology computes at each time the reachable set of the system under a backup control law to ensure the system is within reach of a known a priori safe region. Control barrier functions are then used in conjunction with the reachable set to adjust potentially unsafe control actions that would otherwise move the system beyond reach of this safe set. This approach faces several computational challenges: reachable sets for the dynamics must be computed at runtime; sensitivity of the reachable set to initial conditions is required for the control barrier optimization formulation; and the presence of disturbances introduces a large number of constraints in the resulting optimization. The proposed methodology leverages the theory of mixed monotone systems to address these challenges, and the main contribution of this paper is an application of this methodology to a ten dimensional dual planar multirotor system that is implemented on embedded hardware with a controller update rate up to 100Hz.

M. Abate, C. Klett, S. Coogan and E. 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 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 reduced conservatism, 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 or additional algebraic developments. Numerous examples are provided to illustrate the findings of this work.

M. Abate and S. 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 hyper-rectangles, 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, we 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.

G. Immanuel, M. Abate and Eric Feron

Abstract

This paper investigates stability analysis for implicit, switched linear systems using homogeneous Lyapunov functions (HLF). HLFs of increasing degree are constructed through an outer-product, lifting transformation of the state vector to higher dimensions. This paper presents linear matrix inequalities sufficient conditions for asymptotic stability of these systems based on HLFs. A method is provided to search for Lyapunov functions by incrementally increasing the degree of the homogeneous Lyapunov functions. To address the dimensional growth of the problem space incurred by the lifting transform, a method for dimensional reduction is derived.

C. Klett, M. Abate, S. Coogan and E. 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 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 contributions of the work.

M. Abate, M. Mote, E. Feron and S. Coogan

Abstract

In this work, we show how controlled robustly forward invariant sets for systems with disturbances are efficiently identified via the application of the mixed monotonicity property. A mixed monotone system can be embedded in a related deterministic embedding system with twice as many states but for which the dynamics are monotone; one can then apply the powerful theory of monotone dynamical systems to the embedding system to conclude useful properties of the initial mixed monotone system. Using this technique, we present a method for verifying state-feedback controllers against safety (set invariance) constraints, and our approach involves evaluating a control barrier function type condition that requires the vector field of the embedding system to point into a certain southeast cone. This approach also facilitates the construction of runtime assurance mechanisms for controlled systems with disturbances, and we study system safety in the presence of state uncertainty as well. The results and findings of this work are demonstrated through two numerical examples where we study (i) the verification of a controlled spacecraft system against a safety constraint, and (ii) the formation of a runtime assurance mechanism that functions in the presence of uncertain state measurements.

M. Abate and S. 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 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.

M. Abate and S. 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 characterized as being decomposable into increasing and decreasing components which allows the dynamics to be embedded in a higher dimensional embedding system. Even though the original system is nondeterministic due to the unknown disturbance input, the embedding system has no disturbance and its trajectories provide bounds for finite-time reachable sets of the original dynamics. We then present an efficient method for identifying robustly forward invariant and attractive sets for mixed-monotone systems by studying equilibria and their stability properties of the corresponding embedding system. Next, we show that this approach, when applied to the backward-time dynamics, also establishes different robustly forward invariant sets for the original dynamics. Lastly, we present an independent result for computing decomposition functions for mixed-monotone systems with polynomial dynamics. These tools are demonstrated in several examples and a case study.

Hybrid Sytems TC Outstanding Student Paper Finalist.

M. Abate, C. Klett, S. Coogan and E. 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 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 Lyapunov functions generated with a more traditional sum-of-squares based approach.

C. Klett, M. Abate, Y. Yoon, S. Coogan and E. Feron

Abstract

This paper studies the infinite-time behavior of switched linear systems in the presence of additive noise. In particular, we show that the propagation of the state covariance matrix can be described by a linear affine system and therefore classified by an invariant region of the covariance space. An algorithm is presented for bounding the state covariance matrix with a suitable hyper-ellipsoid in the dimension of the covariance space; we form this algorithm using a Kronecker algebra-based derivation.

M. Dutreix, C. Santoyo, M. Abate and S. Coogan

Abstract

This paper presents a stochastic barrier function-based abstraction technique for discrete-time stochastic systems. Recent works have shown the potential of Interval-valued Markov Chain abstractions for conducting efficient verification of continuous-state, discrete-time stochastic systems against complex objectives, as well as efficient synthesis for finite-mode switched stochastic systems. Such Markovian abstractions allow for a range of transition probabilities between its states. In this work, we address the problem of constructing Interval-valued Markov Chain abstractions for polynomial systems using stochastic barrier functions. Stochastic barrier functions serve as Lyapunov-like probabilistic certificates of forward set invariance. Specifically, given a finite partition of the system's domain, we show that bounds on the probability of transition between any two elements of the partition are found by generating stochastic barrier functions via optimization procedures in the form of Sum-of-Squares programs. We present an algorithm for solving these optimization problems whose implementation is demonstrated in a verification and a synthesis case study.

M. Abate, E. Feron and S. 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. The safety controller uses a monitor, constructed as a finite state machine, to analyze a desired control input policy online and form a sequence of control 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 cyber-physical system with a nondeterministic dynamical model.