包络与波：水平非确定性转向的多车安全避碰

我们提出一种分析两辆车异步、独立、非确定性、转向至方位角的水平机动安全性的方法。未来的转向速率、最终方位角以及整个遭遇过程中连续变化的地速均未知，但被限制于已知范围内。我们开发了一个关于转向运动学的形式化证明库，并将该库应用于创建一个经形式化验证的时序计算。此外，我们创建了一种评估未来碰撞可能性的技术，该技术基于位置可能性的波并依赖于该时序计算。其结果要么判定该遭遇无碰撞，要么计算出碰撞可能发生的时间和位置的安全过近似。