-
Early Versus Late Traffic Management For Autonomous Agents
Authors:
Salman Ghori,
Ania Adil,
Eric Feron
Abstract:
Intersections pose critical challenges in traffic management, where maintaining operational constraints and ensuring safety are essential for efficient flow. This paper investigates the effect of intervention timing in management strategies on maintaining operational constraints at intersections while ensuring safe separation distance, avoiding collisions, and minimizing delay. We introduce contro…
▽ More
Intersections pose critical challenges in traffic management, where maintaining operational constraints and ensuring safety are essential for efficient flow. This paper investigates the effect of intervention timing in management strategies on maintaining operational constraints at intersections while ensuring safe separation distance, avoiding collisions, and minimizing delay. We introduce control regions, represented as circles around the intersection, which refers to the timing of interventions by a centralized control system when agents approach the intersection. We use a mixed-integer linear programming (MILP) approach to optimize the system's performance. To analyze the effectiveness of early and late control measures, a simulation study is conducted, focusing on the safe, efficient, and robust management of agent movement within the control regions.
△ Less
Submitted 9 December, 2024; v1 submitted 29 November, 2024;
originally announced November 2024.
-
Mixed-Integer Linear Programming Model for Collision Avoidance Planning in Commercial Aircraft Formations
Authors:
Songqiying Yang,
Ania Adil,
Eric Feron
Abstract:
With advancements in technology, commercial aircraft formation flying is becoming increasingly feasible as an efficient and environmentally friendly flight method. However, gaps remain in practical implementation, particularly in collision avoidance for aircraft formations. Existing avoidance algorithms mainly focus on single aircraft or UAV swarms, lacking comprehensive studies on the complex int…
▽ More
With advancements in technology, commercial aircraft formation flying is becoming increasingly feasible as an efficient and environmentally friendly flight method. However, gaps remain in practical implementation, particularly in collision avoidance for aircraft formations. Existing avoidance algorithms mainly focus on single aircraft or UAV swarms, lacking comprehensive studies on the complex interactions within commercial aircraft formations. To address this, this paper proposes an optimization model designed to generate safe and effective collision avoidance solutions for commercial aircraft formations. This model demonstrates avoidance paths for formations facing intruders and offers insights for developing formation flight strategies. This study explores response strategies for commercial aircraft formations encountering intruders, considering the difficulty of pilot maneuvers. The findings provide theoretical support for the practical implementation of commercial formation flying and may advance the adoption of this technology.
△ Less
Submitted 29 November, 2024;
originally announced November 2024.
-
Polynomial Lyapunov Functions and Invariant Sets from a New Hierarchy of Quadratic Lyapunov Functions for LTV Systems
Authors:
Hassan Abdelraouf,
Eric Feron,
Jeff S. Shamma
Abstract:
We introduce a new class of quadratic functions based on a hierarchy of linear time-varying (LTV) dynamical systems. These quadratic functions in the higher order space can be also seen as a non-homogeneous polynomial Lyapunov functions for the original system, i.e the first system in the hierarchy. These non-homogeneous polynomials are used to obtain accurate outer approximation for the reachable…
▽ More
We introduce a new class of quadratic functions based on a hierarchy of linear time-varying (LTV) dynamical systems. These quadratic functions in the higher order space can be also seen as a non-homogeneous polynomial Lyapunov functions for the original system, i.e the first system in the hierarchy. These non-homogeneous polynomials are used to obtain accurate outer approximation for the reachable set given the initial condition and less conservative bounds for the impulse response peak of linear, possibly time-varying systems. In addition, we pose an extension to the presented approach to construct invariant sets that are not necessarily Lyapunov functions. The introduced methods are based on elementary linear systems theory and offer very much flexibility in defining arbitrary polynomial Lyapunov functions and invariant sets for LTV systems.
△ Less
Submitted 23 January, 2024;
originally announced January 2024.
-
Algebraic Lyapunov Functions for Homogeneous Dynamic Systems
Authors:
Hassan Abdelraouf,
Eric Feron,
Jeff Shamma
Abstract:
A method for constructing homogeneous Lyapunov functions of degree 1 from polynomial invariant sets is presented for linear time varying systems, homogeneous dynamic systems and the class of nonlinear systems that can be represented as such. The method allows the development of Lyapunov functions that are not necessarily symmetric about the origin, unlike the polynomial, homogeneous Lyapunov funct…
▽ More
A method for constructing homogeneous Lyapunov functions of degree 1 from polynomial invariant sets is presented for linear time varying systems, homogeneous dynamic systems and the class of nonlinear systems that can be represented as such. The method allows the development of Lyapunov functions that are not necessarily symmetric about the origin, unlike the polynomial, homogeneous Lyapunov functions discussed in the prior literature. The work is illustrated by very simple examples.
△ Less
Submitted 3 March, 2023;
originally announced March 2023.
-
From Observability to Observer Realization: A path via elementary block-diagram manipulations
Authors:
Eder Baron-Prada,
Renzo Caballero,
Eric Feron
Abstract:
Introductory state-space linear control courses focus on linear, time-invariant systems and spend intense efforts by introducing system realizations that allow the student to grasp fundamental concepts, among which controllability, observability, and controller and observer design. This note describes a graphical mechanism to transform a system expressed in observability form into its observer for…
▽ More
Introductory state-space linear control courses focus on linear, time-invariant systems and spend intense efforts by introducing system realizations that allow the student to grasp fundamental concepts, among which controllability, observability, and controller and observer design. This note describes a graphical mechanism to transform a system expressed in observability form into its observer form based on elementary block diagram manipulations, a technique whose pedagogical usefulness tends to be overlooked. Given the well-known duality principle in linear systems with respect to controllability and observability, the proposed graphical mechanism is applicable to transform from controllability to controller realization.
△ Less
Submitted 26 August, 2022;
originally announced August 2022.
-
Computing Bounds on $L_{\infty}$-induced Norm for Linear Time-Invariant Systems Using Homogeneous Lyapunov Functions
Authors:
Hassan Abdelraouf,
Gidado-Yisa Immanuel,
Eric Feron
Abstract:
Quadratic Lyapunov function has been widely used in the analysis of linear time invariant (LTI) systems ever since it has shown that the existence of such quadratic Lyapunov function certifies the stability of the LTI system. In this work, the problem of finding upper and lower bounds for the $L_{\infty}$-induced norm of the LTI system is considered. Quadratic Lyapunov functions are used to find t…
▽ More
Quadratic Lyapunov function has been widely used in the analysis of linear time invariant (LTI) systems ever since it has shown that the existence of such quadratic Lyapunov function certifies the stability of the LTI system. In this work, the problem of finding upper and lower bounds for the $L_{\infty}$-induced norm of the LTI system is considered. Quadratic Lyapunov functions are used to find the star norm, the best upper on the $L_{\infty}$-induced norm, by bounding the unit peak input reachable sets by inescapable ellipsoids. Instead, a more general class of homogeneous Lyapunov functions is used to get less conservative upper bounds on the $L_{\infty}$-induced norm and better conservative approximations for the reachable sets than those obtained using standard quadratic Lyapunov functions. The homogeneous Lyapunov function for the LTI system is considered to be a quadratic Lyapunov function for a higher-order system obtained by Lifting the LTI system via Kronecker product. Different examples are provided to show the significant improvements on the bounds obtained by using Homogeneous Lyapunov functions.
△ Less
Submitted 1 March, 2022;
originally announced March 2022.
-
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 developing RTA systems.
△ Less
Submitted 6 June, 2022; v1 submitted 7 October, 2021;
originally announced October 2021.
-
On Linear Time-Invariant Systems Analysis via A Single Trajectory: A Linear Programming Approach
Authors:
Hassan Abdelraouf,
Fahad Albalawi,
Eric Feron
Abstract:
In this note, a novel methodology that can extract a number of analysis results for linear time-invariant systems (LTI) given only a single trajectory of the considered system is proposed. The superiority of the proposed technique relies on the fact that it provides an automatic and formal way to obtain valuable information about the controlled system by only having access to a single trajectory o…
▽ More
In this note, a novel methodology that can extract a number of analysis results for linear time-invariant systems (LTI) given only a single trajectory of the considered system is proposed. The superiority of the proposed technique relies on the fact that it provides an automatic and formal way to obtain valuable information about the controlled system by only having access to a single trajectory over a finite period of time (i.e., the system dynamics is assumed to be unknown). At first, we characterize the stability region of LTI systems given only a single trajectory dataset by constructing the associated Lyapunov function of the system. The Lyapunov function is found by formulating and solving a linear programming (LP) problem. Then, we extend the same methodology to a variety of essential analysis results for LTI systems such as deriving bounds on the output energy, deriving bounds on output peak, deriving $\mathbf{L}_2$ and RMS gains. To illustrate the efficacy of the proposed data-driven paradigm, a comparison analysis between the learned LTI system metrics and the true ones is provided.
△ Less
Submitted 21 September, 2021;
originally announced September 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.
-
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.
-
Modeling and Experimental Validation of a Fractal Tetrahedron UAS Assembly
Authors:
Kévin Garanger,
Jeremy Epps,
Eric Feron
Abstract:
This paper presents the foundation of a modular robotic system comprised of several novel modules in the shape of a tetrahedron. Four single-propeller submodules are assembled to create the Tetracopter, a tetrahedron-shaped quad-rotorcraft used as the elementary module of a modular flying system. This modular flying system is built by assembling the different elementary modules in a fractal shape.…
▽ More
This paper presents the foundation of a modular robotic system comprised of several novel modules in the shape of a tetrahedron. Four single-propeller submodules are assembled to create the Tetracopter, a tetrahedron-shaped quad-rotorcraft used as the elementary module of a modular flying system. This modular flying system is built by assembling the different elementary modules in a fractal shape. The fractal tetrahedron structure of the modular flying assembly grants the vehicle more rigidity than a conventional two-dimensional modular robotic flight system while maintaining the relative efficiency of a two-dimensional modular robotic flight system. A prototype of the Tetracopter has been modeled, fabricated, and successfully flight-tested by the Decision and Control Laboratory at the Georgia Institute of Technology. The results of this research set the foundation for the development of Tetrahedron rotorcraft that can maintain controllable flight and assemble in flight to create a Fractal Tetrahedron Assembly.
△ Less
Submitted 15 March, 2020;
originally announced March 2020.
-
Decentralized On-line Task Reallocation on Parallel Computing Architectures with Safety-Critical Applications
Authors:
Thanakorn Khamvilai,
Louis Sutter,
Eric Feron,
Philippe Baufreton,
Francois Neumann
Abstract:
This work presents a decentralized allocation algorithm of safety-critical application on parallel computing architectures, where individual Computational Units can be affected by faults.
The described method consists in representing the architecture by an abstract graph where each node represents a Computational Unit. Applications are also represented by the graph of Computational Units they re…
▽ More
This work presents a decentralized allocation algorithm of safety-critical application on parallel computing architectures, where individual Computational Units can be affected by faults.
The described method consists in representing the architecture by an abstract graph where each node represents a Computational Unit. Applications are also represented by the graph of Computational Units they require for execution. The problem is then to decide how to allocate Computational Units to applications to guarantee execution of the safety-critical application. The problem is formulated as an optimization problem, with the form of an Integer Linear Program. A state-of-the-art solver is then used to solve the problem.
Decentralizing the allocation process is achieved through redundancy of the allocator executed on the architecture. No centralized element decides on the allocation of the entire architecture, thus improving the reliability of the system.
Experimental reproduction of a multi-core architecture is also presented. It is used to demonstrate the capabilities of the proposed allocation process to maintain the operation of a physical system in a decentralized way while individual component fails.
△ Less
Submitted 19 November, 2019; v1 submitted 3 October, 2019;
originally announced October 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.
-
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.
-
Additive manufacturing for high precision structural properties via feedback control
Authors:
Kévin Garanger,
Thanakorn Khamvilai,
Eric Feron
Abstract:
This paper discusses the possibility of making an object that precisely meets global structural requirements using additive manufacturing and feedback control. An experimental validation is presented by printing a cantilever beam with a prescribed stiffness requirement. The printing process is formalized as a model-based finite-horizon discrete control problem, where the control variables are the…
▽ More
This paper discusses the possibility of making an object that precisely meets global structural requirements using additive manufacturing and feedback control. An experimental validation is presented by printing a cantilever beam with a prescribed stiffness requirement. The printing process is formalized as a model-based finite-horizon discrete control problem, where the control variables are the widths of the successive layers. Sensing is performed by making {\em in situ} intermediate stiffness measurements on the partially built part. The hypothesis that feedback control is effective in enabling the 3D-printed beam to meet precise stiffness requirements is validated experimentally.
△ Less
Submitted 25 May, 2020; v1 submitted 24 May, 2019;
originally announced May 2019.
-
Bounding the State Covariance Matrix for a Randomly Switching Linear System with Noise
Authors:
Yongeun Yoon,
Corbin Klett,
Eric Feron
Abstract:
The propagation of a state vector is governed by a set of time-invariant state transition matrices that switch arbitrarily between two values. The evolution of the state is also perturbed by white Gaussian noise with a variance that switches randomly with the state transition relation. The behavior of this system can be characterized by the covariance matrix of the state vector, which is time vary…
▽ More
The propagation of a state vector is governed by a set of time-invariant state transition matrices that switch arbitrarily between two values. The evolution of the state is also perturbed by white Gaussian noise with a variance that switches randomly with the state transition relation. The behavior of this system can be characterized by the covariance matrix of the state vector, which is time varying. However, we can bound the set of covariances by comparing the switching system to an augmented system derived with Kronecker algebra. We formulate a matrix optimization problem to compute an ellipsoid that bounds the covariance dynamics, which in turn bounds the state covariance of the set of switching systems subject to white noise. In developing this approach, an invariant ellipsoid for a linear switching affine system is computed along the way.
△ Less
Submitted 21 May, 2019;
originally announced May 2019.
-
3D printing of a leaf spring: A demonstration of closed-loop control in additive manufacturing
Authors:
Kevin Garanger,
Thanakorn Khamvilai,
Eric Feron
Abstract:
This paper presents the integration of a feedback control loop during the printing of a plastic object using additive manufacturing. The printed object is a leaf spring made of several parts of different infill density values, which are the control variables in this problem. In order to achieve a desired objective stiffness, measurements are taken after each part is completed and the infill densit…
▽ More
This paper presents the integration of a feedback control loop during the printing of a plastic object using additive manufacturing. The printed object is a leaf spring made of several parts of different infill density values, which are the control variables in this problem. In order to achieve a desired objective stiffness, measurements are taken after each part is completed and the infill density is adjusted accordingly in a closed-loop framework. The absolute error in the stiffness at the end of printing is reduced from 11.63% to 1.34% by using a closed-loop instead of an open-loop control. This experiments serves as a proof of concept to show the relevance of using feedback control in additive manufacturing. By considering the printing process and the measurements as stochastic processes, we show how stochastic optimal control and Kalman filtering can be used to improve the quality of objects manufactured with rudimentary printers.
△ Less
Submitted 7 May, 2018;
originally announced May 2018.
-
Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
Authors:
Guillaume Davy,
Eric Féron,
Pierre-Loïc Garoche,
Didier Henrion
Abstract:
Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more complex controls such as aggressive maneuvering or performing fuel-efficient controls. Another approach called optimal control is capable of computing such difficult trajectories but lacks the ability to adapt to dynamic ch…
▽ More
Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more complex controls such as aggressive maneuvering or performing fuel-efficient controls. Another approach called optimal control is capable of computing such difficult trajectories but lacks the ability to adapt to dynamic changes in the environment. In both cases, the control was designed offline, relying on more or less complex algorithms to find the appropriate parameters. More recent kinds of approaches such as Linear Model-Predictive Control (MPC) rely on the online use of convex optimization to compute the best control at each sample time. In these settings, optimization algorithms are specialized for the specific control problem and embed on the device. This paper proposes to revisit the code generation of an interior point method (IPM)algorithm, an efficient family of convex optimization, focusing on the proof of its implementation at code level. Our approach relies on the code specialization phase to produce additional annotations formalizing the intented specification of the algorithm. Deductive methods are then used to prove automatically the validity of these assertions. Since the algorithm is complex, additional lemmas are also produced, allowing the complete proofto be checked by SMT solvers only. This work is the first to address the effective formal proof of an IPM algorithm. Theapproach could also be generalized more systematically to code generation frameworks, producing proof certificate along the code, for numerical intensive software.
△ Less
Submitted 28 September, 2018; v1 submitted 11 January, 2018;
originally announced January 2018.
-
Maneuver Regulation for Accelerating Bodies in Atmospheric Environments
Authors:
Juan-Pablo Afman,
Eric Feron,
John Hauser
Abstract:
In order to address the need for an affordable reduced gravity test platform, this work focuses on the analysis and implementation of atmospheric acceleration tracking with an autonomous aerial vehicle. As proof of concept, the vehicle is designed with the objective of flying accurate reduced-gravity parabolas. Suggestions from both academia and industry were taken into account, as well as require…
▽ More
In order to address the need for an affordable reduced gravity test platform, this work focuses on the analysis and implementation of atmospheric acceleration tracking with an autonomous aerial vehicle. As proof of concept, the vehicle is designed with the objective of flying accurate reduced-gravity parabolas. Suggestions from both academia and industry were taken into account, as well as requirements imposed by a regulatory agency. The novelty of this work is the Proportional Integral Ramp Quadratic PIRQ controller, which is employed to counteract the aerodynamic forces impeding the vehicles constant acceleration during the maneuver. The stability of the free-fall maneuver under this controller is studied in detail via the formation of the transverse dynamics and the application of the circle criterion. The implementation of such a controller is then outlined, and the PIRQ controller is validated through a flight test, where the vehicle successfully tracks Martian gravity 0.378 G's with a standard deviation of 0.0426.
△ Less
Submitted 5 August, 2017;
originally announced August 2017.
-
Anatomy of a Crash
Authors:
Aude Marzuoli,
Emmanuel Boidot,
Eric Feron,
Paul B. C. van Erp,
Alexis Ucko,
Alexandre Bayen,
Mark Hansen
Abstract:
Transportation networks constitute a critical infrastructure enabling the transfers of passengers and goods, with a significant impact on the economy at different scales. Transportation modes, whether air, road or rail, are coupled and interdependent. The frequent occurrence of perturbations on one or several modes disrupts passengers' entire journeys, directly and through ripple effects. The pres…
▽ More
Transportation networks constitute a critical infrastructure enabling the transfers of passengers and goods, with a significant impact on the economy at different scales. Transportation modes, whether air, road or rail, are coupled and interdependent. The frequent occurrence of perturbations on one or several modes disrupts passengers' entire journeys, directly and through ripple effects. The present paper provides a case report of the Asiana Crash in San Francisco International Airport on July 6th 2013 and its repercussions on the multimodal transportation network. It studies the resulting propagation of disturbances on the transportation infrastructure in the United States. The perturbation takes different forms and varies in scale and time frame : cancellations and delays snowball in the airspace, highway traffic near the airport is impacted by congestion in previously never congested locations, and transit passenger demand exhibit unusual traffic peaks in between airports in the Bay Area. This paper, through a case study, aims at stressing the importance of further data-driven research on interdependent infrastructure networks for increased resilience. The end goal is to form the basis for optimization models behind providing more reliable passenger door-to-door journeys.
△ Less
Submitted 15 October, 2014;
originally announced October 2014.
-
Credible Autocoding of Convex Optimization Algorithms
Authors:
Timothy Wang,
Romain Jobredeaux,
Marc Pantel,
Pierre-Loic Garoche,
Eric Feron,
Didier Henrion
Abstract:
The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. In this paper, we demonstrat…
▽ More
The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. In this paper, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the level of the code, thereby making it accessible for the formal methods community. The running example used in this paper is a generic semi-definite programming (SDP) solver. Semi-definite programs can encode a wide variety of optimization problems and can be solved in polynomial time at a given accuracy. We describe a top-to-down approach that transforms a high-level analysis of the algorithm into useful code annotations. We formulate some general remarks about how such a task can be incorporated into a convex programming autocoder. We then take a first step towards the automatic verification of the optimization program by identifying key issues to be adressed in future work.
△ Less
Submitted 2 September, 2014; v1 submitted 7 March, 2014;
originally announced March 2014.
-
Credible Autocoding of Fault Detection Observers
Authors:
Timothy Wang,
Alireza Esna Ashari,
Romain Jobredeaux,
Eric M. Feron
Abstract:
In this paper, we present a domain specific process to assist the verification of observer-based fault detection software. Observer-based fault detection systems, like control systems, yield invariant properties of quadratic types. These quadratic invariants express both safety properties of the software such as the boundedness of the states and correctness properties such as the absence of false…
▽ More
In this paper, we present a domain specific process to assist the verification of observer-based fault detection software. Observer-based fault detection systems, like control systems, yield invariant properties of quadratic types. These quadratic invariants express both safety properties of the software such as the boundedness of the states and correctness properties such as the absence of false alarms from the fault detector. We seek to leverage these quadratic invariants, in an automated fashion, for the formal verification of the fault detection software. The approach, referred to as the credible autocoding framework [1], can be characterized as autocoding with proofs. The process starts with the fault detector model, along with its safety and correctness properties, all expressed formally in a synchronous modeling environment such as Simulink. The model is then transformed by a prototype credible autocoder into both code and analyzable annotations for the code. We demonstrate the credible autocoding process on a running example of an output observer fault detector for a 3-degrees-of-freedom (3DOF) helicopter control system.
△ Less
Submitted 8 November, 2013;
originally announced November 2013.
-
Verifiable Control System Development for Gas Turbine Engines
Authors:
Mehrdad Pakmehr,
Timothy Wang,
Romain Jobredeaux,
Martin Vivies,
Eric Feron
Abstract:
A control software verification framework for gas turbine engines is developed. A stability proof is presented for gain scheduled closed-loop engine system based on global linearization and linear matrix inequality (LMI) techniques. Using convex optimization tools, a single quadratic Lyapunov function is computed for multiple linearizations near equilibrium points of the closed-loop system. With t…
▽ More
A control software verification framework for gas turbine engines is developed. A stability proof is presented for gain scheduled closed-loop engine system based on global linearization and linear matrix inequality (LMI) techniques. Using convex optimization tools, a single quadratic Lyapunov function is computed for multiple linearizations near equilibrium points of the closed-loop system. With the computed stability matrices, ellipsoid invariant sets are constructed, which are used efficiently for DGEN turbofan engine control code stability analysis. Then a verifiable linear gain scheduled controller for DGEN engine is developed based on formal methods, and tested on the engine virtual test bench. Simulation results show that the developed verifiable gain scheduled controller is capable of regulating the engine in a stable fashion with proper tracking performance.
△ Less
Submitted 8 November, 2013;
originally announced November 2013.
-
A Message Passing Strategy for Decentralized Connectivity Maintenance in Agent Removal
Authors:
Derya Aksaray,
A. Yasin Yazicioglu,
Eric Feron,
Dimitri N. Mavris
Abstract:
In a multi-agent system, agents coordinate to achieve global tasks through local communications. Coordination usually requires sufficient information flow, which is usually depicted by the connectivity of the communication network. In a networked system, removal of some agents may cause a disconnection. In order to maintain connectivity in agent removal, one can design a robust network topology th…
▽ More
In a multi-agent system, agents coordinate to achieve global tasks through local communications. Coordination usually requires sufficient information flow, which is usually depicted by the connectivity of the communication network. In a networked system, removal of some agents may cause a disconnection. In order to maintain connectivity in agent removal, one can design a robust network topology that tolerates a finite number of agent losses, and/or develop a control strategy that recovers connectivity. This paper proposes a decentralized control scheme based on a sequence of replacements, each of which occurs between an agent and one of its immediate neighbors. The replacements always end with an agent, whose relocation does not cause a disconnection. We show that such an agent can be reached by a local rule utilizing only some local information available in agents' immediate neighborhoods. As such, the proposed message passing strategy guarantees the connectivity maintenance in arbitrary agent removal. Furthermore, we significantly improve the optimality of the proposed scheme by incorporating $δ$-criticality (i.e. the criticality of an agent in its $δ$-neighborhood).
△ Less
Submitted 1 November, 2013;
originally announced November 2013.
-
Online Performance Optimization of a DC Motor Driving a Variable Pitch Propeller
Authors:
Raphael Cohen,
David Miculescu,
Kevin Reilley,
Mehrdad Pakmehr,
Eric Feron
Abstract:
A practical online optimization scheme is developed for performance optimization of an electrical aircraft propulsion system. The goal is to minimize the power extraction of the propulsion system for any given thrust value. The online optimizer computes the optimum pitch angle of a variable pitch propeller by minimizing the power of the system for a command thrust value. This algorithm is tested o…
▽ More
A practical online optimization scheme is developed for performance optimization of an electrical aircraft propulsion system. The goal is to minimize the power extraction of the propulsion system for any given thrust value. The online optimizer computes the optimum pitch angle of a variable pitch propeller by minimizing the power of the system for a command thrust value. This algorithm is tested on a DC motor driving a variable pitch propeller; the experimental hardware setup of the DC motor along with its variable pitch propeller is also described. Experimental results show the efficiency and practicality of the proposed online optimization scheme. Outstanding issues are sketched.
△ Less
Submitted 30 September, 2013;
originally announced October 2013.
-
Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller
Authors:
Timothy Wang,
Eric Feron
Abstract:
This article describes the application of a credible autocoding framework for control systems towards a nonlinear car controller example. The framework generates code, along with guarantees of high level functional properties about the code that can be independently verified. These high-level functional properties not only serves as a certificate of good system behvaior but also can be used to gua…
▽ More
This article describes the application of a credible autocoding framework for control systems towards a nonlinear car controller example. The framework generates code, along with guarantees of high level functional properties about the code that can be independently verified. These high-level functional properties not only serves as a certificate of good system behvaior but also can be used to guarantee the absence of runtime errors. In one of our previous works, we have constructed a prototype autocoder with proofs that demonstrates this framework in a fully automatic fashion for linear and quasi-nonlinear controllers. With the nonlinear car example, we propose to further extend the prototype's dataflow annotation language environment with with several new annotation symbols to enable the expression of general predicates and dynamical systems. We demonstrate manually how the new extensions to the prototype autocoder work on the car controller using the output language Matlab. Finally, we discuss the requirements and scalability issues of the automatic analysis and verification of the documented output code.
△ Less
Submitted 27 August, 2013;
originally announced August 2013.
-
From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems
Authors:
Timothy Wang,
Romain Jobredeaux,
Heber Herencia,
Pierre-Loic Garoche,
Arnaud Dieumegard,
Eric Feron,
Marc Pantel
Abstract:
This article describes a fully automated, credible autocoding chain for control systems. The framework generates code, along with guarantees of high level functional properties which can be independently verified. It relies on domain specific knowledge and fomal methods of analysis to address a context of heightened safety requirements for critical embedded systems and ever-increasing costs of ver…
▽ More
This article describes a fully automated, credible autocoding chain for control systems. The framework generates code, along with guarantees of high level functional properties which can be independently verified. It relies on domain specific knowledge and fomal methods of analysis to address a context of heightened safety requirements for critical embedded systems and ever-increasing costs of verification and validation. The platform strives to bridge the semantic gap between domain expert and code verification expert. First, a graphical dataflow language is extended with annotation symbols enabling the control engineer to express high level properties of its control law within the framework of a familiar language. An existing autocoder is enhanced to both generate the code implementing the initial design, but also to carry high level properties down to annotations at the level of the code. Finally, using customized code analysis tools, certificates are generated which guarantee the correctness of the annotations with respect to the code, and can be verified using existing static analysis tools. Only a subset of properties and controllers are handled at this point.
△ Less
Submitted 25 August, 2013; v1 submitted 9 July, 2013;
originally announced July 2013.
-
Airport Gate Scheduling for Passengers, Aircraft, and Operation
Authors:
Sang Hyun Kim,
Eric Feron,
John-Paul Clarke,
Aude Marzuoli,
Daniel Delahaye
Abstract:
Passengers' experience is becoming a key metric to evaluate the air transportation system's performance. Efficient and robust tools to handle airport operations are needed along with a better understanding of passengers' interests and concerns. Among various airport operations, this paper studies airport gate scheduling for improved passengers' experience. Three objectives accounting for passenger…
▽ More
Passengers' experience is becoming a key metric to evaluate the air transportation system's performance. Efficient and robust tools to handle airport operations are needed along with a better understanding of passengers' interests and concerns. Among various airport operations, this paper studies airport gate scheduling for improved passengers' experience. Three objectives accounting for passengers, aircraft, and operation are presented. Trade-offs between these objectives are analyzed, and a balancing objective function is proposed. The results show that the balanced objective can improve the efficiency of traffic flow in passenger terminals and on ramps, as well as the robustness of gate operations.
△ Less
Submitted 15 January, 2013;
originally announced January 2013.
-
Optimization of Lyapunov Invariants in Verification of Software Systems (Extended Version)
Authors:
Mardavij Roozbehani,
Alexandre Megretski,
Eric Feron
Abstract:
The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance speci…
▽ More
The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, presence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-resembling those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification.
△ Less
Submitted 29 August, 2011;
originally announced August 2011.
-
A graphical environment to express the semantics of control systems
Authors:
Timothy Wang,
Romain Jobredeaux,
E. Feron
Abstract:
We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the verification and validation of the control software. We propose extensions to a Simulink-like environment's annotation capabilities to include formal control system…
▽ More
We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the verification and validation of the control software. We propose extensions to a Simulink-like environment's annotation capabilities to include formal control system stability, performance properties and their proofs. We provide a conceptual description of a tool, that takes in a Simulink-like diagram of the control system as the input, and generates a graphically annotated control system diagram as the output. The annotations can either be inserted by the user or generated automatically by a third party control analysis software such as IQC$β$ or $μ$-tool. We finally describe how the graphical representation of the system and its properties can be translated to annotated programs in a programming language used in verification and validation such as Lustre or C.
△ Less
Submitted 19 August, 2011;
originally announced August 2011.
-
Optimization of Lyapunov Invariants in Verification of Software Systems
Authors:
Mardavij Roozbehani,
Alexandre Megretski,
Eric Feron
Abstract:
The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance speci…
▽ More
The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, presence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-resembling those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
-
Environmental benefits of enhanced surveillance technology on airport departure operations
Authors:
Pierrick Burgain,
Eric Feron
Abstract:
Airport departure operations constitute an important source of airline delays and passenger frustration. Excessive surface traffic is the cause of increased controller and pilot workload; It is also the source of increased emissions; It worsens traffic safety and often does not yield improved runway throughput. Acknowledging this fact, this paper explores some of the feedback mechanisms by which a…
▽ More
Airport departure operations constitute an important source of airline delays and passenger frustration. Excessive surface traffic is the cause of increased controller and pilot workload; It is also the source of increased emissions; It worsens traffic safety and often does not yield improved runway throughput. Acknowledging this fact, this paper explores some of the feedback mechanisms by which airport traffic can be optimized in real time according to its current degree of congestion. In particular, it examines the environmnetal benefits that improved surveillance technologies can bring in the context of gate- or spot-release aircraft strategies. It is shown that improvements can lead yield 4% to 6% emission reductions for busy airports like New-York La Guardia or Seattle Tacoma. These benefits come on top of the benefits already obtained by adopting threshold strategies currently under evaluation.
△ Less
Submitted 13 February, 2011;
originally announced February 2011.
-
ATC Taskload Inherent to the Geometry of Stochastic 4-D Trajectory Flows with Flight Technical Errors
Authors:
Vlad Popescu,
John-Paul B. Clarke,
Karen M. Feigh,
Eric Feron
Abstract:
A method to quantify the probabilistic controller taskload inherent to maintaining aircraft adherence to 4-D trajectories within flow corridors is presented. An Ornstein-Uhlenbeck model of the aircraft motion and a Poisson model of the flow scheduling are introduced along with reasonable numerical values of the model parameters. Analytic expressions are derived for the taskload probability densit…
▽ More
A method to quantify the probabilistic controller taskload inherent to maintaining aircraft adherence to 4-D trajectories within flow corridors is presented. An Ornstein-Uhlenbeck model of the aircraft motion and a Poisson model of the flow scheduling are introduced along with reasonable numerical values of the model parameters. Analytic expressions are derived for the taskload probability density functions for basic functional elements of the flow structure. Monte Carlo simulations are performed for these basic functional elements and the controller taskload probabilities are exhibited.
△ Less
Submitted 7 February, 2011;
originally announced February 2011.
-
Aircraft Proximity Maps Based on Data-Driven Flow Modeling
Authors:
Erwan Salaün,
Maxime Gariel,
Adan Vela,
Eric Feron
Abstract:
With the forecast increase in air traffic demand over the next decades, it is imperative to develop tools to provide traffic flow managers with the information required to support decision making. In particular, decision-support tools for traffic flow management should aid in limiting controller workload and complexity, while supporting increases in air traffic throughput. While many decision-supp…
▽ More
With the forecast increase in air traffic demand over the next decades, it is imperative to develop tools to provide traffic flow managers with the information required to support decision making. In particular, decision-support tools for traffic flow management should aid in limiting controller workload and complexity, while supporting increases in air traffic throughput. While many decision-support tools exist for short-term traffic planning, few have addressed the strategic needs for medium- and long-term planning for time horizons greater than 30 minutes. This paper seeks to address this gap through the introduction of 3D aircraft proximity maps that evaluate the future probability of presence of at least one or two aircraft at any given point of the airspace. Three types of proximity maps are presented: presence maps that indicate the local density of traffic; conflict maps that determine locations and probabilities of potential conflicts; and outliers maps that evaluate the probability of conflict due to aircraft not belonging to dominant traffic patterns. These maps provide traffic flow managers with information relating to the complexity and difficulty of managing an airspace. The intended purpose of the maps is to anticipate how aircraft flows will interact, and how outliers impact the dominant traffic flow for a given time period. This formulation is able to predict which "critical" regions may be subject to conflicts between aircraft, thereby requiring careful monitoring. These probabilities are computed using a generative aircraft flow model. Time-varying flow characteristics, such as geometrical configuration, speed, and probability density function of aircraft spatial distribution within the flow, are determined from archived Enhanced Traffic Management System data, using a tailored clustering algorithm. Aircraft not belonging to flows are identified as outliers.
△ Less
Submitted 6 February, 2011; v1 submitted 25 January, 2011;
originally announced January 2011.
