论文标题
线性时间逻辑任务的安全性最佳路径计划
Secure-by-Construction Optimal Path Planning for Linear Temporal Logic Tasks
论文作者
论文摘要
在本文中，我们研究了计划单个机器人实现线性时间逻辑（LTL）任务的最佳无限途径的问题，并具有安全保证。我们假设可以通过被动入侵者（Eavesdropper）访问由输出功能指定的机器人的外部行为。安全约束要求入侵者不要推断机器人是从秘密位置开始的。我们提供了一个声音而完整的算法程序来解决此问题。我们的方法是基于双重加权过渡系统（Twin-wts）的构建，该系统跟踪一对具有相同观察的路径。我们表明，可以根据Twin-WTS和代表LTL公式的BüchiAutomaton的图形搜索技术有效解决安全感路径计划问题。所提出的计划算法的复杂性在系统模型的大小上是多项式。最后，我们通过一个简单的机器人计划示例来说明我们的算法。
In this paper, we investigate the problem of planning an optimal infinite path for a single robot to achieve a linear temporal logic (LTL) task with security guarantee. We assume that the external behavior of the robot, specified by an output function, can be accessed by a passive intruder (eavesdropper). The security constraint requires that the intruder should never infer that the robot was started from a secret location. We provide a sound and complete algorithmic procedure to solve this problem. Our approach is based on the construction of the twin weighted transition systems (twin-WTS) that tracks a pair of paths having the same observation. We show that the security-aware path planning problem can be effectively solved based on graph search techniques in the product of the twin-WTS and the Büchi automaton representing the LTL formula. The complexity of the proposed planning algorithm is polynomial in the size of the system model. Finally, we illustrate our algorithm by a simple robot planning example.
