Envelopes and Waves: Safe Multivehicle Collision Avoidance for Horizontal Non-deterministic Turns

TL;DR

This paper introduces a formal verification approach for collision avoidance in multi-vehicle horizontal maneuvers with uncertain turn rates and speeds, ensuring safety through wave-based collision possibility evaluation.

Contribution

It develops a library of formal proofs for turning kinematics and a verified timing computation to assess collision risks under non-deterministic conditions.

Findings

Successfully verifies safety of maneuvers with unknown future turn rates.

Provides a collision possibility evaluation technique based on waves of position.

Computes safe overapproximations for collision timing and location.

Abstract

We present an approach to analyzing the safety of asynchronous, independent, non-deterministic, turn-to-bearing horizontal maneuvers for two vehicles. Future turn rates, final bearings, and continuously varying ground speeds throughout the encounter are unknown but restricted to known ranges. We develop a library of formal proofs about turning kinematics, and apply the library to create a formally verified timing computation. Additionally, we create a technique that evaluates future collision possibilities that is based on waves of position possibilities and relies on the timing computation. The result either determines that the encounter will be collision-free, or computes a safe overapproximation for when and where collisions may occur.