You Don't Know When I Will Arrive: Unpredictable Controller Synthesis for Temporal Logic Tasks

TL;DR

This paper presents a novel method for synthesizing controllers that ensure task completion while maintaining unpredictability against passive intruders in systems with temporal logic specifications.

Contribution

It introduces a new information structure and a complete algorithm for secure controller synthesis under temporal logic constraints with security considerations.

Findings

The approach guarantees task achievement and security simultaneously.

The algorithm is sound and complete for the proposed problem.

Case study demonstrates practical effectiveness in robot planning.

Abstract

In this paper, we investigate the problem of synthesizing controllers for temporal logic specifications under security constraint. We assume that there exists a passive intruder (eavesdropper) that can partially observe the behavior of the system. For the purpose of security, we require that the system's behaviors are unpredictable in the sense that the intruder cannot determine for sure that the system will exactly accomplish the task in $K$ steps ahead. This problem is particularly challenging since future information is involved in the synthesis process. We propose a novel information structure that predicts the effect of control in the future. A sound and complete algorithm is developed to synthesize a controller which ensures both task completion and security guarantee. The proposed approach is illustrated by a case study of robot task planning.