用于导航的混合动力学类型论

我们提出一种混合动力学类型论，其配备了用于组织并证明导航控制算法安全性的有用原语。该类型论将 Fu--Kishida--Selinger 从状态-参数纤维化构造线性依赖类型论的框架与先前关于顺序复合下混合系统范畴的工作相结合。我们还定义了线性时序逻辑的一个片段在我们类型论中的推测性嵌入，旨在实现与现有从形式化任务规约自动综合控制器的前沿工具的互操作。作为一个案例研究，我们使用该类型论来组织并证明由 Vasilopoulos 实现的 Arslan--Koditschek 避障导航算法的安全性质。最后，我们推测了该类型论的扩展，以处理模型空间与物理空间之间的共轭关系，以及分层模板-锚点关系。