Optimal Synthesis of Opacity-Enforcing Supervisors for Qualitative and Quantitative Specifications

TL;DR

This paper develops algorithms for synthesizing optimal supervisors that enforce privacy in discrete-event systems, ensuring opacity and delaying secret revelation, with both qualitative and quantitative approaches.

Contribution

It provides the first complete solution to the infinite-step opacity control problem without assumptions on event controllability and observability, including a new quantitative measure.

Findings

Optimal qualitative synthesis as a safety-game.

Quantitative synthesis as an optimal total-cost control problem.

Introduction of secret-revelation-time as a new measure.

Abstract

In this paper, we investigate both qualitative and quantitative synthesis of optimal privacy-enforcing supervisors for partially-observed discrete-event systems. We consider a dynamic system whose information-flow is partially available to an intruder, which is modeled as a passive observer. We assume that the system has a "secret" that does not want to be revealed to the intruder. Our goal is to synthesize a supervisor that controls the system in a least-restrictive manner such that the closed-loop system meets the privacy requirement. For the qualitative case, we adopt the notion of infinite-step opacity as the privacy specification by requiring that the intruder can never determine for sure that the system is/was at a secret state for any specific instant. If the qualitative synthesis problem is not solvable or the synthesized solution is too restrictive, then we further investigate the quantitative synthesis problem so that the secret is revealed (if unavoidable) as late as possible. Effective algorithms are provided to solve both the qualitative and quantitative synthesis problems. Specifically, by building suitable information structures that involve information delays, we show that the optimal qualitative synthesis problem can be solved as a safety-game. The optimal quantitative synthesis problem can also be solved as an optimal total-cost control problem over an augmented information structure. Our work provides a complete solution to the standard infinite-step opacity control problem, which has not been solved without assumption on the relationship between controllable events and observable events. Furthermore, we generalize the opacity enforcement problem to the numerical setting by introducing the secret-revelation-time as a new quantitative measure.