Home About Publications Software Teaching

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

Y. Kouskoulas, T. J. Machado, D. Genin, A. Schmidt, I. Papusha, and J. Brulé

• Manuscript
• DOI: 10.1007/s10009-022-00654-2
• Coq code

Abstract

We present an approach to analyze 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.

Citation

Y. Kouskoulas, T. J. Machado, D. Genin, A. Schmidt, I. Papusha, and J. Brulé. “Envelopes and Waves: Safe Multivehicle Collision Avoidance for Horizontal Non-deterministic Turns,” Journal on Software Tools for Technology Transfer, 2022.