Planning with Probabilistic Opacity and Transparency: A Computational Model of Opaque/Transparent Observations

TL;DR

This paper introduces a novel automaton-based approach for synthesizing control policies that maximize the probability of maintaining opacity or transparency of secrets in dynamical systems, improving security in robotic planning.

Contribution

It develops an opaque-observations automaton to precisely characterize observation sets enforcing opacity, enabling optimal planning in MDPs for security and task performance.

Findings

Effective in robot motion planning with opacity constraints

Automaton-based method outperforms belief-based approaches

Demonstrated success in maximizing secrecy in dynamic systems

Abstract

Qualitative opacity of a secret is a security property, which means that a system trajectory satisfying the secret is observation-equivalent to a trajectory violating the secret. In this paper, we study how to synthesize a control policy that maximizes the probability of a secret being made opaque against an eavesdropping attacker/observer, while subject to other task performance constraints. In contrast to existing belief-based approach for opacity-enforcement, we develop an approach that uses the observation function, the secret, and the model of the dynamical systems to construct a so-called opaque-observations automaton which accepts the exact set of observations that enforce opacity. Leveraging this opaque-observations automaton, we can reduce the optimal planning in Markov decision processes(MDPs) for maximizing probabilistic opacity or its dual notion, transparency, subject to task constraints into a constrained planning problem over an augmented-state MDP. Finally, we illustrate the effectiveness of the developed methods in robot motion planning problems with opacity or transparency requirements.