Showing 1–7 of 7 results for author: Jeannin, J

Falsification of a Vision-based Automatic Landing System

Authors: Sara Shoouri, Shayan Jalili, Jiahong Xu, Isabelle Gallagher, Yuhao Zhang, Joshua Wilhelm, Necmiye Ozay, Jean-Baptiste Jeannin

Abstract: At smaller airports without an instrument approach or advanced equipment, automatic landing of aircraft is a safety-critical task that requires the use of sensors present on the aircraft. In this paper, we study falsification of an automatic landing system for fixed-wing aircraft using a camera as its main sensor. We first present an architecture for vision-based automatic landing, including a vis… ▽ More At smaller airports without an instrument approach or advanced equipment, automatic landing of aircraft is a safety-critical task that requires the use of sensors present on the aircraft. In this paper, we study falsification of an automatic landing system for fixed-wing aircraft using a camera as its main sensor. We first present an architecture for vision-based automatic landing, including a vision-based runway distance and orientation estimator and an associated PID controller. We then outline landing specifications that we validate with actual flight data. Using these specifications, we propose the use of the falsification tool Breach to find counterexamples to the specifications in the automatic landing system. Our experiments are implemented using a Beechcraft Baron 58 in the X-Plane flight simulator communicating with MATLAB Simulink. △ Less

Submitted 4 July, 2023; originally announced July 2023.

Comments: AIAA Scitech 2021 Forum

Automating Geometric Proofs of Collision Avoidance with Active Corners

Authors: Nishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin

Abstract: Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional… ▽ More Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collision avoidance algorithms and proofs consider vehicles to be a point mass, though the actual vehicles are not points. In this paper, we consider a convex polygonal vehicle with nonzero area traveling along a 2-dimensional trajectory. We derive an easily-checkable, quantifier-free formula to check whether a given obstacle will collide with the vehicle moving on the planned trajectory. We apply our method to two case studies of aircraft collision avoidance and study its performance. △ Less

Submitted 14 July, 2022; originally announced July 2022.

Comments: 13 pages, 11 figures, conference paper

Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes

Authors: Liren Yang, Hang Zhang, Jean-Baptiste Jeannin, Necmiye Ozay

Abstract: Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that under-approximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics, and uses constrained zonotopes for set representation… ▽ More Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that under-approximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics, and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to under-approximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-sized representation for it in polynomial time. Our algorithm finds a polynomial-sized under-approximation in polynomial time. We further analyze the conservatism of this under-approximation technique, and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms. △ Less

Submitted 26 August, 2022; v1 submitted 9 July, 2022; originally announced July 2022.

Comments: This article will be presented at the International Conference on Embedded Software (EMSOFT) 2022 and will appear as part of the ESWEEK-TCAD special issue

A Concurrent Switching Model for Traffic Congestion Control

Authors: Hossein Rastgoftar, Xun Liu, Jean-Baptiste Jeannin

Abstract: We introduce a new conservation-based approach for traffic coordination modeling and control in a network of interconnected roads (NOIR) with switching movement phase rotations at every NOIR junction. For modeling of traffic evolution, we first assume that the movement phase rotation is cyclic at every NOIR junction, but the duration of each movement phase can be arbitrarily commanded by traffic s… ▽ More We introduce a new conservation-based approach for traffic coordination modeling and control in a network of interconnected roads (NOIR) with switching movement phase rotations at every NOIR junction. For modeling of traffic evolution, we first assume that the movement phase rotation is cyclic at every NOIR junction, but the duration of each movement phase can be arbitrarily commanded by traffic signals. Then, we propose a novel concurrent switching dynamics (CSD) with deterministic transitions among a finite number of states, representing the NOIR movement phases. We define the CSD control as a cyclic receding horizon optimization problem with periodic quadratic cost and constraints. More specifically, the cost is defined so that the traffic density is minimized and the boundary inflow is uniformly distributed over the boundary inlet roads, whereas the cost parameters are periodically changed with time. The constraints are linear and imposed by a trapezoidal fundamental diagram at every NOIR road so that traffic feasibility is assured and traffic over-saturation is avoided. The success of the proposed traffic boundary control is demonstrated by simulation of traffic congestion control in Downtown Phoenix. △ Less

Submitted 11 April, 2022; originally announced April 2022.

A Physics-Based Finite-State Abstraction for Traffic Congestion Control

Authors: Hossein Rastgoftar, Jean-Baptiste Jeannin

Abstract: This paper offers a finite-state abstraction of traffic coordination and congestion in a network of interconnected roads (NOIR). By applying mass conservation, we model traffic coordination as a Markov process. Model Predictive Control (MPC) is applied to control traffic congestion through the boundary of the traffic network. The optimal boundary inflow is assigned as the solution of a constrained… ▽ More This paper offers a finite-state abstraction of traffic coordination and congestion in a network of interconnected roads (NOIR). By applying mass conservation, we model traffic coordination as a Markov process. Model Predictive Control (MPC) is applied to control traffic congestion through the boundary of the traffic network. The optimal boundary inflow is assigned as the solution of a constrained quadratic programming problem. Additionally, the movement phases commanded by traffic signals are determined using receding horizon optimization. In simulation, we show how traffic congestion can be successfully controlled through optimizing boundary inflow and movement phases at traffic network junctions. △ Less

Submitted 19 January, 2021; originally announced January 2021.

Comments: 7 pages, 5 figures. arXiv admin note: text overlap with arXiv:1912.00565

Formal Specification of Continuum Deformation Coordination

Authors: Hossein Rastgoftar, Jean-Baptiste Jeannin, Ella Atkins

Abstract: Continuum deformation is a leader-follower multiagent cooperative control approach. Previous work showed a desired continuum deformation can be uniquely defined based on trajectories of d +1 leaders in a d-dimensional motion space and acquired by followers through local inter-agent communication. This paper formally specifies continuum deformation coordination in an obstacle-laden environment. Usi… ▽ More Continuum deformation is a leader-follower multiagent cooperative control approach. Previous work showed a desired continuum deformation can be uniquely defined based on trajectories of d +1 leaders in a d-dimensional motion space and acquired by followers through local inter-agent communication. This paper formally specifies continuum deformation coordination in an obstacle-laden environment. Using linear temporal logic (LTL), continuum deformation liveness and safety requirements are defined. Safety is prescribed by providing conditions on (i) agent deviation bound, (ii) inter-agent collision avoidance, (iii) agent containment, (iv) motion space containment, and (v) obstacle collision avoidance. Liveness specifies a reachability condition on the desired final formation. △ Less

Submitted 26 July, 2019; originally announced July 2019.

Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions

Authors: Kyle D. Julian, Shivam Sharma, Jean-Baptiste Jeannin, Mykel J. Kochenderfer

Abstract: The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic. The resulting system uses a large lookup table to determine advisories given to pilots, but these tables can grow very large. To enable the system to operate on limited hardware, prior work investigated compressing the table using a… ▽ More The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic. The resulting system uses a large lookup table to determine advisories given to pilots, but these tables can grow very large. To enable the system to operate on limited hardware, prior work investigated compressing the table using a deep neural network. However, ensuring that the neural network reliably issues safe advisories is important for certification. This work defines linearized regions where each advisory can be safely provided, allowing Reluplex, a neural network verification tool, to check if unsafe advisories are ever issued. A notional collision avoidance policy is generated and used to train a neural network representation. The neural networks are checked for unsafe advisories, resulting in the discovery of thousands of unsafe counterexamples. △ Less

Submitted 2 March, 2019; originally announced March 2019.