Secure-by-Construction Optimal Path Planning for Linear Temporal Logic Tasks
2020
Online
report
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\"{u}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.
Comment: This work has been accepted by 59th IEEE Conference on Decision and Control for publication
Titel: |
Secure-by-Construction Optimal Path Planning for Linear Temporal Logic Tasks
|
---|---|
Autor/in / Beteiligte Person: | Yang, Shuo ; Yin, Xiang ; Li, Shaoyuan ; Zamani, Majid |
Link: | |
Veröffentlichung: | 2020 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|