面向具有长期访问比例目标的LTL规范的控制综合

中文摘要 AI 辅助

本文研究了系统在满足线性时序逻辑（LTL）规范的同时实现期望的长期访问比例所需的路径规划问题。对于以前缀-后缀结构表示的路径，长期访问比例量化了后缀轨迹中感兴趣的原子命题序列的渐近出现比例。这种定量要求通常无法用标准的LTL规范表达。此外，我们开发了一种规划方法，该方法综合出一条满足LTL的路径，其长期访问比例保持在期望值的指定容差范围内，同时满足总体成本约束。通过调整期望比例，综合出的路径可以为感兴趣的原子命题序列分配更多或更少的长期关注，从而提高任务执行的灵活性和效率。最后，在四足机器人上的实验证明了所提出的长期访问比例的实际意义以及所提出的规划方法的有效性。

英文摘要

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 (AP) 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.

发表机构

• The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））

机构由 AI 辅助整理，请以论文原文为准。