ACAS X 中形式化验证的下一代机载避撞博弈
计算机科学中的逻辑
2022-11-23 v2 计算机科学与博弈论
系统与控制
系统与控制
摘要
飞机避撞算法的设计是一项微妙而重要的挑战，亟需可证明的安全性保证。鉴于入侵机决策、本机飞行员反应以及飞机连续运动动力学微妙性的不可预测交织，获得此类保证并非易事。现有避撞系统，如 TCAS 和下一代机载避撞系统 ACAS X，已在假设对入侵机飞行动作有严格限制的前提下进行分析，这限制了其在入侵机可能改变航向的真实场景中的安全保证。本工作在概念上意义重大且具实际相关性，它偏离现有 ACAS X 模型，将其推广为混合博弈，以一流方式表示来自两个独立玩家的本机与入侵机决策，从而实现显著先进的预测能力。通过在微分博弈逻辑中证明所得对抗式 ACAS X 存在获胜策略，针对本机与入侵机沿具有演化垂直/水平速度的微分方程飞行路径且各自独立决策的丰富相遇情形，确立了无碰撞性。我们提出三类复杂度递增的模型：单建议无限时间模型、有界时间模型以及无限时间多建议模型。在每类模型中，我们辨识出符号条件并证明总存在可能的本机机动可防止两机相撞。
引用
@article{arxiv.2106.02030,
title = {Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X},
author = {Rachel Cleaveland and Stefan Mitsch and André Platzer},
journal= {arXiv preprint arXiv:2106.02030},
year = {2022}
}