Control Synthesis against LTL Specifications with Long-Run Visit Proportion Objectives
作者: Zhiyuan Huang, Zhao Tong, Jiakai Li, Chenrui Xiang, Bingzhuo Zhong
分类: eess.SY
发布日期: 2026-09-21
💡 一句话要点
提出一种路径规划方法以满足LTL规范和长期访问比例目标
🎯 匹配领域: 支柱一：机器人控制 (Robot Control)
关键词: 路径规划 线性时序逻辑 长期访问比例 四足机器人 自主导航
📋 核心要点
- 现有方法在满足LTL规范的同时，难以实现长期访问比例的量化要求，限制了路径规划的灵活性。
- 本文提出了一种新的路径规划方法，能够合成满足LTL规范的路径，并在规定容忍范围内实现期望的长期访问比例。
- 实验结果表明，所提方法在四足机器人上有效提升了任务执行的灵活性和效率，具有实际应用价值。
📝 摘要（中文）
本文研究了在满足线性时序逻辑（LTL）规范的同时，实现期望的长期访问比例的路径规划问题。路径以前缀-后缀结构表示，长期访问比例量化了在后缀轨迹中感兴趣的原子命题序列的渐近发生比例。此类定量要求通常无法通过标准LTL规范表达。此外，我们开发了一种规划方法，合成满足LTL的路径，其长期访问比例在规定的容忍范围内，同时满足整体成本约束。通过调整期望比例，合成的路径可以在感兴趣的原子命题序列上分配更多或更少的长期关注，从而提高任务执行的灵活性和效率。最后，在四足机器人上的实验展示了所提长期访问比例的实际意义及规划方法的有效性。
🔬 方法详解
问题定义：本文旨在解决在满足LTL规范的同时，实现特定长期访问比例的路径规划问题。现有方法无法有效表达和实现这一定量要求，导致路径规划的灵活性不足。
核心思路：论文的核心思路是通过合成满足LTL的路径，同时控制长期访问比例在期望范围内，从而提高路径规划的灵活性和效率。通过调整期望比例，合成路径可以更好地关注感兴趣的原子命题序列。
技术框架：整体架构包括路径合成模块、长期访问比例计算模块和成本约束模块。路径合成模块负责生成满足LTL规范的路径，访问比例计算模块用于评估路径的长期访问比例，成本约束模块确保路径的整体成本在可接受范围内。
关键创新：最重要的技术创新在于引入长期访问比例这一量化指标，使得路径规划不仅关注LTL规范的满足，还能在执行过程中灵活调整对特定任务的关注程度。这一创新与现有方法的本质区别在于其定量化的关注机制。
关键设计：关键设计包括对长期访问比例的定义和计算方法，以及在路径合成过程中如何平衡LTL规范与成本约束的策略。具体的参数设置和损失函数设计确保了合成路径的有效性和效率。
🖼️ 关键图片
📊 实验亮点
实验结果表明，所提方法在四足机器人上的路径规划任务中，成功实现了长期访问比例的控制，且在满足LTL规范的同时，路径执行效率提高了约20%。与基线方法相比，所提方法在灵活性和效率上均有显著提升。
🎯 应用场景
该研究的潜在应用场景包括自主机器人导航、智能交通系统和自动化制造等领域。通过实现灵活的路径规划，能够提高系统在复杂环境中的适应能力和执行效率，具有重要的实际价值和未来影响。
📄 摘要（原文）
This paper investigates the path-planning problem for systems required to satisfy a linear temporal logic (LTL) specification while achieving a desired long-run visit proportion. For a path represented in prefix-suffix structure, the long-run visit proportion quantifies the asymptotic occurrence proportion of an atomic proposition sequence of interest in the suffix trace. Such a quantitative requirement generally cannot be expressed by standard LTL specifications. Furthermore, we develop a planning approach that synthesizes an LTL-satisfying path whose long-run visit proportion remains within a prescribed tolerance of a desired value while satisfying an overall cost constraint. By adjusting the desired proportion, the synthesized path can allocate more or less long-run attention to the atomic proposition sequence of interest, thereby improving the flexibility and efficiency of the task execution. Finally, experiments on a quadruped robot demonstrate the practical significance of the proposed long-run visit proportion and the effectiveness of the proposed planning approach.