安全性可形式化验证
融合Voronoi全局规划与可视图细化，生成的路径能通过时间自动机模型在UPPAAL中形式化验证安全性，给出路线安全与否的明确解释。
葛慧林 · 李梦 · 温广辉 · Lu, Yu
Expert Systems with Applications 2026
导航过程被抽象为线性定价时间自动机模型，在UPPAAL中可验证避障、无死锁等定性与定量属性。
验证结果直接解释路线为何安全或不安全，使不可行或高风险的使命配置在规划阶段即可被排除。
混合Voronoi全局规划与可视图细化生成无碰撞路径，并在验证中考虑能耗等定量约束。