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

TL;DR

The paper tackles how to maximize probabilistic opacity $PH( heta; M^{ ho}, \mathsf{Obs})$ while ensuring a task is satisfied with probability at least $\epsilon$ in stochastic systems with imperfect observations. It introduces an opaque-observations automaton by composing a finite-state transducer of the observation function with the secret DFA and intersecting with its dual to obtain the exact set of observations that enforce opacity. This leads to a product MDP $M\times\mathcal{A}\times\mathcal{A}^{opaque}$ whose opacity planning problem is solved via a constrained linear program over occupancy measures, yielding an optimal policy $\pi^{*}$. The approach is validated through case studies in robot motion planning and a power-plant gridworld, demonstrating how sensor configurations and task thresholds shape the trade-off between opacity and task satisfaction and illustrating a concrete path to extend opacity planning to partially observable settings and multi-agent scenarios.

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.

Figures (7)

• Figure 1: mdp for the illustrative example. The colored boxes represent the observation partition of the state space.
• Figure 2: A fragment of fst encoding the observation function.
• Figure 3: (a)dfa for the task specification $\psi = \Diamond \, s_4$. (b)dfa for the secret specification $\varphi = \Diamond \, s_6$.
• Figure 4: A fragment of product fst.
• Figure 5: A fragment of nfa for $L_O(\mathcal{A}_H)$.

Theorems & Definitions (24)

• Definition 1
• Definition 2: Transition-Observation function
• Definition 3: ltlf de2013linear
• Definition 4: dfa
• Definition 5: Symmetrical Opacity
• Definition 6: Symmetrical Transparency
• Lemma 1
• Definition 7: Probabilistic opacity and transparency
• Example 1: Part I
• Definition 8: Opaque observations