Reference. Automating Geometric Proofs of Collision Avoidance with Active Corners
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.
Cite
Cited by (2)
Provably Safe Optimization of Arrival Flows Into Terminal Airspace dane-2026-provably
Automatic Certification of the Active Corner Method for Collision Avoidance kheterpal-2026-automatic
Cites 36 works (2 here)
With notes (2)
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system jeannin-2016-a
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System jeannin-2015-a
External (34)
- A Decision Method for Elementary Algebra and Geometry (2023)
- Set Propagation Techniques for Reachability Analysis (2021)
- Formal Verification of Collision Avoidance for Turning Maneuvers in UAVs (2019)
- Safe, Aggressive Quadrotor Flight via Reachability-based Trajectory Design (2019)
- Control Barrier Functions: Theory and Applications (2019)
- Hamilton-Jacobi reachability: A brief overview and recent advances (2017)
- Compositional transient stability analysis of power systems via the computation of reachable sets (2017)
- SymPy: symbolic computing in Python (2017)
- A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets (2017)
- A Complete Uniform Substitution Calculus for Differential Dynamic Logic (2016)
- A Method for Invariant Generation for Polynomial Continuous Systems (2016)
- Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations (2014)
- Online Verification of Automated Road Vehicles Using Reachability Analysis (2014)
- Characterizing Algebraic Invariants by Differential Radical Invariants (2014)
- On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles (2013)
- Solving set-valued constraint satisfaction problems (2011)
- Relational Abstractions for Continuous and Hybrid Systems (2011)
- Computing semi-algebraic invariants for polynomial dynamical systems (2011)
- Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods (2010)
- Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization (2008)
- The complexity of quantifier elimination and cylindrical algebraic decomposition (2007)
- Reachability of Uncertain Linear Systems Using Zonotopes (2005)
- Safety Verification of Hybrid Systems Using Barrier Certificates (2004)
- Constructing invariants for hybrid systems (2004)
- QEPCAD B: a program for computing with semi-algebraic sets using CADs (2003)
- Exact Collision Checking of Robot Paths (2002)
- A Safe Swept Volume Method for Collision Detection (2000)
- I-COLLIDE: an interactive and exact collision detection system for large-scale environments (1995)
- Efficient collision detection for animation and robotics (1993)
- Efficient collision detection for animation (1992)
- Collision detection by four-dimensional intersection testing (1990)
- Real Quantifier Elimination is Doubly Exponential (1988)
- Cylindrical Algebraic Decomposition I: The Basic Algorithm (1984)
- Quantifier elimination for real closed fields by cylindrical algebraic decomposition (1975)