通过混合图规划和时序自动机验证实现的安全保障型自主水面航行（ASV）导航决策支持

自主水面航行器（ASV）在复杂海洋环境中需确保安全可靠的导航。本文提出集成混合图路径规划与形式验证的决策支持框架，通过HVV-E规划器生成Voronoi图与可见性图结合的复合路线，并利用线性定价时自动机（LPTA）抽象导航过程进行形式验证，确保路径满足碰撞避免、无死锁、时间与能耗约束等要求，同时通过UPPAAL提供安全/不安全配置的明确解释，支持可审计的自主决策。

桂慧琳|李萌|文光辉|卢宇

江苏科技大学海洋学院，中国镇江

摘要

自主水面航行器（ASVs）需要在复杂多变的海洋环境中可靠地运行以确保安全。本文开发了一个集成的决策支持框架，该框架将基于混合图的路径规划与形式化验证相结合，以保证航行安全且可达。所提出的HVV-E规划器生成了综合路线图，它结合了基于Voronoi的全局规划和可视性图优化，以生成无碰撞且考虑能源消耗的轨迹。为了确保候选路线的可信度，航行过程被抽象为线性定价时序自动机（LPTA）模型，并使用UPPAAL进行形式化验证。验证内容包括定性属性（如避障和无死锁）和定量任务约束（如行驶时间限制和能耗）。验证结果明确说明了为什么某条路线是安全的或不安全的，从而能够及早识别出不可行或风险较高的任务配置。在新加坡海峡的现实场景中进行的实验表明，所提出的框架为实际ASV任务提供了透明、安全且有能源意识的导航支持。这些结果凸显了将形式化推理与智能规划相结合对于推进可解释和可信的自主海洋系统的重要性。

引言

自主水面航行器（ASVs）越来越多地应用于环境监测、监视、基础设施检查以及搜救等海洋任务（Luo, Zhuang, Jin, Xu, & Su (2024); Yin & Xiang (2025)）。随着人类监督的减少，导航系统必须在水流不稳定、有漂浮物、通道受限以及船舶交通不规律的水域中做出安全且负责任的决策。因此，确保ASV既能避开危险又能可靠地到达任务目标对于实现可信的海洋自主性至关重要。在港口安全或时间敏感的救援任务等安全关键场景中，即使是微小的导航错误也可能导致任务失败或碰撞风险（Perez-Cerrolaza et al. (2024)）。除了简单计算可行路线外，此类任务的决策支持工具还必须提供可被操作员检查、认证和信任的保证。实际上，海洋管理部门越来越要求在部署前有证据表明自主导航决策满足安全裕度、任务截止时间和能源限制。因此，一个能够从数学上证明导航选择合理性的框架可以提高任务可靠性，支持认证流程，并降低实际部署中的操作风险。

路径规划是ASV导航的核心，它决定了车辆如何在环境和任务约束下穿越复杂水域。传统的基于路线图的规划方法（如Voronoi和可视性图方法（Lozano-Pérez & Wesley (1979a); Mahkovic & Slivnik (2000)）能够高效捕捉自由空间的连通性，但在处理动态障碍物或潮汐和移动船舶造成的时间约束时存在困难（Liu, Wang, Hu, & He (2018); Liu, Zhang, Yu, & Yuan (2016)），并且严重缺乏形式上的正确性保证（Qu et al. (2025)）。较新的启发式、基于优化的和学习驱动的方法在非结构化海洋环境中提高了适应性（Krell, King, & Carrillo (2022); Peralta, Reina, & Toral (2023)），但这些方法仍然更注重经验性能而非明确的正确性保证。因此，许多ASV规划器无法正式确保安全性、时间范围内的可达性或避免死锁，限制了它们在高保障任务中的适用性。因此，越来越多的人关注可解释和可信的自主系统（Arrieta et al. (2020)）。最近的研究从互补的角度进一步强调了这些挑战。Wang等人（Wang et al. (2025)）研究了ASV实时物体检测模型的鲁棒性。同时，Barik和Parhi（Barik & Parhi (2025）提出了一种用于自主水下车辆的增强型路径规划和避障框架。尽管这些努力提高了感知鲁棒性和算法规划效率，但它们仍然无法同时提供形式上的保证，确保导航决策同时满足时间、能源和安全约束。

形式化验证为自主系统提供了严谨的数学推理工具。基于自动机的模型检查已广泛应用于机器人技术和信息物理系统（Peng, Lu, & Miller (2016); Quottrup, Bak, & Zamanabadi (2004); Saberi, Groote, & Keshishzadeh (2013)），能够验证逻辑约束、时间行为和同步性。时序自动机为这些模型增加了明确的时钟，用于截止时间推理，而线性定价时序自动机（LPTA）进一步纳入了累积成本（如行驶距离或能源消耗）。最近的研究探索了将形式化验证与数据驱动或混合控制架构相结合的方法（Huang et al. (2024); Lu, Zheng, & Leung (2025); Wang, Yang, & Wu (2024)）。然而，大多数现有的基于验证的导航框架将规划和验证视为松散耦合的阶段：规划器独立生成路线，验证仅报告规范是否成立，而不解释失败的原因或提供更安全的替代方案。此外，导航通常被抽象为纯粹的离散转换，限制了对实际ASV任务所需的空间、时间和成本的联合处理。

本文通过开发一个具有验证意识的决策支持框架来解决这些限制，该框架将混合图规划与基于LPTA的形式化推理紧密集成。所提出的规划组件称为HVV-E（Hybrid Voronoi–Visibility with Energy Optimization），它结合了基于Voronoi的全局覆盖和可视性图优化，以支持考虑能源消耗和安全性的ASV导航。该框架不仅仅将验证作为最后的筛选步骤，而是构建了可以系统地抽象为时序自动机模型的路线图结构，并针对定性的安全性和定量的任务要求进行验证。由此产生的流程能够在执行前提供透明的路线建议，并明确解释不安全的配置。通过在单一决策支持流程中整合规划和验证，该框架不仅能够计算无碰撞的轨迹，还能够提供明确的、可审计的证据，证明计划的任务满足操作约束——这对于可认证和准备部署的ASV系统至关重要。

具体来说，HVV-E规划器通过结合Voronoi图的全局覆盖和可视性优化来生成综合路线图，以实现精确的避障和 clearance。生成的轨迹被转换为LPTA抽象，其中同时编码了空间约束、时间限制和路径成本指标。然后使用UPPAAL进行验证，以评估避障能力、无死锁性、时间范围内的可达性和成本限制下的性能，并在违反属性时生成诊断性反例。这种设计超越了事后验证，提供了可解释的安全保障导航支持。

本文的主要贡献总结如下：

•

具有验证意识的混合规划。构建了一种混合路线图，提高了覆盖率和障碍物清除能力，同时可以忠实转换为时序自动机模型，以便后续进行形式化推理。

•

统一的LPTA导航抽象。一个统一的建模框架在单个LPTA模型中编码了空间关系、截止时间和累积成本，实现了时间和能源范围内的可达性分析。

•

可解释的安全保障。

基于UPPAAL的验证流程不仅提供了布尔验证结果，还提供了解释不安全或不可达配置的反例轨迹，支持可解释的决策支持。

本文的其余部分组织如下。第2节回顾了自主导航中的路径规划和形式化验证。第3节介绍了所提出的HVV-E混合规划框架及其基于LPTA的导航抽象。第4节报告了在代表性海洋场景中的实验评估。第5节讨论了见解、局限性和未来研究方向。第6节总结了本文。

章节片段

基于路线图的路径规划方法

由于波浪、水流和移动船舶等动态和不可预测的因素，海洋环境中的导航具有挑战性（Liu et al. (2018); Sidoti et al. (2017)）。因此，已经探索了许多启发式搜索和基于图的算法来提高鲁棒性（Cui, Li, & Yan (2016); Liu & Bucknall (2015); Niu, Lu, Savvaris, & Tsourdos (2016); Pamosoaji & Hong (2013)）。基于路线图的方法特别吸引人，因为它们将连续导航转换为可处理的

HVV-E规划算法概述

所提出的框架遵循一个三阶段流程，将原始环境数据转换为ASV的能源意识导航路径。所得到的规划器被称为HVV-E（Hybrid Voronoi–Visibility with Energy Optimization）。其核心思想是利用Voronoi图（全局覆盖和清除）和可视性图（几何效率）的互补优势，同时为所有候选路径段分配物理上的能源成本。

首先，异构

实验

本节介绍了一组全面的实验，旨在从三个互补的角度评估所提出的框架。首先，我们评估所提出的HVV-E规划器是否能够在真实的海洋环境中生成既几何上可行又能源效率高的路径。其次，我们量化每个规划阶段的计算成本，以确定该方法是否适合实际部署。第三，我们评估基于LPTA的验证层

讨论

在实际海洋环境中部署的ASVs必须在动态和部分不可预测的条件下运行，包括海洋水流、风扰动和移动障碍物。传统的几何规划器（如Voronoi图和可视性图方法）由于其可解释性和在静态地图中的效率而仍然具有吸引力。然而，这些方法本身不能保证规划轨迹满足任务级别的约束，如时间预算和能源

结论

本文通过将混合路径规划与形式化验证相结合，提出了一种安全有保障且能源意识强的自主水面航行器（ASV）导航决策支持框架。所提出的HVV-E规划器结合了基于Voronoi的全局覆盖和可视性图优化，以在复杂的海洋环境中生成几何上可行且能源效率高的路线。除了规划之外，候选轨迹还被系统地抽象为线性定价时序自动机（LPTA）

未引用的引用

缺少图1和算法1的引用。

CRediT作者贡献声明

桂慧琳：资金获取、调查、写作——审阅与编辑。李萌：可视化、写作——审阅与编辑。文光辉：验证、写作——审阅与编辑。卢宇：概念化、资金获取、方法论、调查、写作——初稿、写作——审阅与编辑。

利益冲突声明

作者声明他们没有已知的竞争性财务利益或个人关系可能影响本文报告的工作。