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

TL;DR

This paper presents a method for planning optimal robot paths that satisfy LTL tasks while ensuring security against passive eavesdroppers by preventing them from inferring secret start locations.

Contribution

We introduce a novel twin-WTS based approach that guarantees security and optimality in LTL path planning, with a polynomial-time algorithm for the problem.

Findings

Algorithm is sound and complete.

Security constraints are effectively integrated.

Polynomial complexity in system size.

Abstract

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.