面向可转向针安全优化控制的在线策略综合

自主系统常应用于不确定环境中，需要进行前瞻性行动规划与回顾性数据评估以用于未来规划，从而确保安全运行。形式化方法可为这些系统提供安全性保障，但通常计算代价高昂，且随着系统复杂性增长而难以扩展。本文基于经典策略综合引入在线策略综合，以在响应并适应环境变化的同时获得形式化安全性保障。为保障在线安全，我们将环境划分为若干区域类型，这些类型决定了行动计划的接受并触发局部纠正动作。通过对频繁更新的模型进行模型检测，我们可由此推导局部安全的行动计划（前瞻性），并通过可达性检查将当前模型与新观测进行匹配（回顾性）。作为用例，我们成功将在线策略综合应用于医疗针导航，即引导一根（柔性且带斜面的）针穿过组织抵达目标而不损伤其周围组织。