Secure-by-Construction Optimal Path Planning for Linear Temporal Logic Tasks

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.

I. Introduction

Path planning is a fundamental problem in robotics which asks to generate a planned trajectory from an initial location such that some desired requirements are fulfilled. Classical planning problems usually focus on low-level tasks such as obstacle avoidance or point-to-point navigation [1]. In the past decades, temporal-logic-based high-level path planning for complex tasks has drawn considerable attention in the literature; see, e.g., [2], [3]. In this framework, the planning task is specified by linear temporal logic (LTL) or computation tree logic (CTL) formulae. By using automata-theoretic approach, algorithmic procedures are developed to automatically generate correct-by-construction plans to achieve the given temporal logic tasks.