Automating Geometric Proofs of Collision Avoidance with Active Corners

TL;DR

This paper presents a method to automatically verify collision avoidance for convex polygonal vehicles along planned trajectories, simplifying the process with a new formula and demonstrating its effectiveness in aircraft scenarios.

Contribution

It introduces a quantifier-free formula for collision checking of polygonal vehicles, advancing beyond point-mass models in automated collision avoidance proofs.

Findings

Effective in aircraft collision avoidance case studies

Provides an easily-checkable collision verification formula

Improves accuracy over point-mass models

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 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.