-
$\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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Ride-Sharing Networks with Mixed Autonomy
Authors:
Qinshuang Wei,
Jorge Alberto Rodriguez,
Ramtin Pedarsani,
Samuel Coogan
Abstract:
We consider ride-sharing networks served byhuman-driven vehicles and autonomous vehicles. First, wepropose a novel model for ride-sharing in this mixed autonomysetting for a multi-location network in which the platformsets prices for riders, compensation for drivers, and operatesautonomous vehicles for a fixed price. Then we study thepossible benefits, in the form of increased profits, to the ride…
▽ More
We consider ride-sharing networks served byhuman-driven vehicles and autonomous vehicles. First, wepropose a novel model for ride-sharing in this mixed autonomysetting for a multi-location network in which the platformsets prices for riders, compensation for drivers, and operatesautonomous vehicles for a fixed price. Then we study thepossible benefits, in the form of increased profits, to the ride-sharing platform that are possible by introducing autonomousvehicles. We first establish a nonconvex optimization problemcharacterizing the optimal profits for a network operatingat a steady-state equilibrium and then propose a convexproblem with the same optimal profits that allows for efficientcomputation. Next, we study the relative mix of autonomous andhuman-driven vehicles that results at equilibrium for variouscosts of operation for autonomous vehicles. In particular, weshow that there is a regime for which the platform will chooseto mix autonomous and human-driven vehicles in order tooptimize profits. Our results provide insights into how suchride-sharing platforms might choose to integrate autonomousvehicles into their fleet.
△ Less
Submitted 18 March, 2019;
originally announced March 2019.
-
Koopman Operator Applications in Signalized Traffic Systems
Authors:
Esther Ling,
Liyuan Zheng,
Lillian J. Ratliff,
Samuel Coogan
Abstract:
This paper proposes Koopman operator theory and the related algorithm dynamical mode decomposition (DMD) for analysis and control of signalized traffic flow networks. DMD provides a model-free approach for representing complex oscillatory dynamics from measured data, and we study its application to several problems in signalized traffic. We first study a single signalized intersection, and we prop…
▽ More
This paper proposes Koopman operator theory and the related algorithm dynamical mode decomposition (DMD) for analysis and control of signalized traffic flow networks. DMD provides a model-free approach for representing complex oscillatory dynamics from measured data, and we study its application to several problems in signalized traffic. We first study a single signalized intersection, and we propose applying this method to infer traffic signal control parameters such as phase timing directly from traffic flow data. Next, we propose using the oscillatory modes of the Koopman operator, approximated with DMD, for early identification of unstable queue growth that has the potential to cause cascading congestion. Then we demonstrate how DMD can be coupled with knowledge of the traffic signal control status to determine traffic signal control parameters that are able to reduce queue lengths. Lastly, we demonstrate that DMD allows for determining the structure and the strength of interactions in a network of signalized intersections. All examples are demonstrated using a case study network instrumented with high resolution traffic flow sensors.
△ Less
Submitted 28 February, 2019;
originally announced February 2019.
-
Routing for Traffic Networks with Mixed Autonomy
Authors:
Daniel A. Lazar,
Sam Coogan,
Ramtin Pedarsani
Abstract:
In this work we propose a macroscopic model for studying routing on networks shared between human-driven and autonomous vehicles that captures the effects of autonomous vehicles forming platoons. We use this to study inefficiency due to selfish routing and bound the Price of Anarchy (PoA), the maximum ratio between total delay experienced by selfish users and the minimum possible total delay. To d…
▽ More
In this work we propose a macroscopic model for studying routing on networks shared between human-driven and autonomous vehicles that captures the effects of autonomous vehicles forming platoons. We use this to study inefficiency due to selfish routing and bound the Price of Anarchy (PoA), the maximum ratio between total delay experienced by selfish users and the minimum possible total delay. To do so, we establish two road capacity models, each corresponding to an assumption regarding the platooning capabilities of autonomous vehicles. Using these we develop a class of road delay functions, parameterized by the road capacity, that are polynomial with respect to vehicle flow. We then bound the PoA and the bicriteria, another measure of the inefficiency due to selfish routing. We find these bounds depend on: 1) the degree of the polynomial in the road cost function and 2) the degree of asymmetry, the difference in how human-driven and autonomous traffic affect congestion. We demonstrate that these bounds recover the classical bounds when no asymmetry exists. We show the bounds are tight in certain cases and that the PoA bound is order-optimal with respect to the degree of asymmetry.
△ Less
Submitted 4 September, 2018;
originally announced September 2018.
-
Control of Multi-Agent Systems with Finite Time Control Barrier Certificates and Temporal Logic
Authors:
Mohit Srinivasan,
Samuel Coogan,
Magnus Egerstedt
Abstract:
In this paper, a method to synthesize controllers using finite time convergence control barrier functions guided by linear temporal logic specifications for continuous time multi-agent dynamical systems is proposed. Finite time convergence to a desired set in the state space is guaranteed under the existence of a suitable finite time convergence control barrier function. In addition, these barrier…
▽ More
In this paper, a method to synthesize controllers using finite time convergence control barrier functions guided by linear temporal logic specifications for continuous time multi-agent dynamical systems is proposed. Finite time convergence to a desired set in the state space is guaranteed under the existence of a suitable finite time convergence control barrier function. In addition, these barrier functions also guarantee forward invariance once the system converges to the desired set. This allows us to formulate a theoretical framework which synthesizes controllers for the multi-agent system. These properties also enable us to solve the reachability problem in continuous time by formulating a theorem on the composition of multiple finite time convergence control barrier functions. This approach is more flexible than existing methods and also allows for a greater set of feasible control laws. Linear temporal logic is used to specify complex task specifications that need to be satisfied by the multi-agent system. With this solution methodology, a control law is synthesized that satisfies the given temporal logic task specification. Robotic experiments are provided which were performed on the Robotarium multi-robot testbed at Georgia Tech.
△ Less
Submitted 7 August, 2018;
originally announced August 2018.
-
Generalizing infinitesimal contraction analysis to hybrid systems
Authors:
Samuel A Burden,
Samuel D Coogan
Abstract:
Infinitesimal contraction analysis, wherein global asymptotic convergence results are obtained from local dynamical properties, has proven to be a powerful tool for applications in biological, mechanical, and transportation systems. Thus far, the technique has been restricted to systems governed by a single smooth differential or difference equation. We generalize infinitesimal contraction analysi…
▽ More
Infinitesimal contraction analysis, wherein global asymptotic convergence results are obtained from local dynamical properties, has proven to be a powerful tool for applications in biological, mechanical, and transportation systems. Thus far, the technique has been restricted to systems governed by a single smooth differential or difference equation. We generalize infinitesimal contraction analysis to hybrid systems governed by interacting differential and difference equations. Our theoretical results are illustrated on a series of examples.
△ Less
Submitted 11 April, 2018;
originally announced April 2018.
-
The Price of Anarchy for Transportation Networks with Mixed Autonomy
Authors:
Daniel A. Lazar,
Samuel Coogan,
Ramtin Pedarsani
Abstract:
We study routing behavior in transportation networks with mixed autonomy, that is, networks in which a fraction of the vehicles on each road are equipped with autonomous capabilities such as adaptive cruise control that enable reduced headways and increased road capacity. Motivated by capacity models developed for such roads with mixed autonomy, we consider transportation networks in which the del…
▽ More
We study routing behavior in transportation networks with mixed autonomy, that is, networks in which a fraction of the vehicles on each road are equipped with autonomous capabilities such as adaptive cruise control that enable reduced headways and increased road capacity. Motivated by capacity models developed for such roads with mixed autonomy, we consider transportation networks in which the delay on each road or link is an affine function of two quantities: the number of vehicles with autonomous capabilities on the link and the number of regular vehicles on the link. We particularly study the price of anarchy for such networks, that is, the ratio of the total delay experienced by selfish routing to the socially optimal routing policy. Unlike the case when all vehicles are of the same type, for which the price of anarchy is known to be bounded, we first show that the price of anarchy can be arbitrarily large for such mixed autonomous networks. Next, we define a notion of asymmetry equal to the maximum possible travel time improvement due to the presence of autonomous vehicles. We show that when the degree of asymmetry of all links in the network is bounded by a factor less than 4, the price of anarchy is bounded. We also bound the bicriteria, which is a bound on the cost of selfishly routing traffic compared to the cost of optimally routing additional traffic. These bounds depend on the degree of asymmetry and recover classical bounds on the price of anarchy and bicriteria in the case when no asymmetry exists. Further, we show with examples that these bound are tight in particular cases.
△ Less
Submitted 21 October, 2017;
originally announced October 2017.
-
Traffic Network Control from Temporal Logic Specifications
Authors:
Samuel Coogan,
Ebru Aydin Gol,
Murat Arcak,
Calin Belta
Abstract:
We propose a framework for generating a signal control policy for a traffic network of signalized intersections to accomplish control objectives expressible using linear temporal logic. By applying techniques from model checking and formal methods, we obtain a correct-by-construction controller that is guaranteed to satisfy complex specifications. To apply these tools, we identify and exploit stru…
▽ More
We propose a framework for generating a signal control policy for a traffic network of signalized intersections to accomplish control objectives expressible using linear temporal logic. By applying techniques from model checking and formal methods, we obtain a correct-by-construction controller that is guaranteed to satisfy complex specifications. To apply these tools, we identify and exploit structural properties particular to traffic networks that allow for efficient computation of a finite state abstraction. In particular, traffic networks exhibit a componentwise monotonicity property which allows reach set computations that scale linearly with the dimension of the continuous state space.
△ Less
Submitted 21 June, 2016; v1 submitted 6 August, 2014;
originally announced August 2014.
-
A note on norm-based Lyapunov functions via contraction analysis
Authors:
Samuel Coogan,
Murat Arcak
Abstract:
It is well know that for globally contractive autonomous systems, there exists a unique equilibrium and the distance to the equilibrium evaluated along any trajectory decreases exponentially with time. We show that, additionally, the magnitude of the velocity evaluated along any trajectory decreases exponentially, thus giving an alternative choice of Lyapunov function.
It is well know that for globally contractive autonomous systems, there exists a unique equilibrium and the distance to the equilibrium evaluated along any trajectory decreases exponentially with time. We show that, additionally, the magnitude of the velocity evaluated along any trajectory decreases exponentially, thus giving an alternative choice of Lyapunov function.
△ Less
Submitted 30 July, 2013;
originally announced August 2013.