Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Approximate Opacity of Stochastic Control Systems

Siyuan Liu, Xiang Yin, Dimos V. Dimarogonas, Majid Zamani

TL;DR

This work defines a quantitative, horizon-bounded notion of opacity for stochastic control systems modeled as general Markov decision processes, introducing $(\varepsilon,\lambda)$-approximate initial-state and current-state opacity. It provides finite-gMDP verification methods via specialized estimators and value iteration, enabling efficient checking of opacity on finite abstractions. To scale to infinite-state systems, the authors introduce opacity-preserving stochastic simulation relations (InitSOP and CurSOP) based on $\delta$-lifting, which guarantee that opacity properties transfer between a concrete gMDP and its finite abstraction with explicit error terms. They show how to construct opacity-preserving finite abstractions under $\delta$-ISS stability, and demonstrate the approach on a road-traffic case study where opacity guarantees transition from abstraction to the concrete system. The results offer a scalable, abstraction-based pathway for verifying and potentially designing controllers that enforce opacity in stochastic CPS.

Abstract

This paper investigates an important class of information-flow security property called opacity for stochastic control systems. Opacity captures whether a system's secret behavior (a subset of the system's behavior that is considered to be critical) can be kept from outside observers. Existing works on opacity for control systems only provide a binary characterization of the system's security level by determining whether the system is opaque or not. In this work, we introduce a quantifiable measure of opacity that considers the likelihood of satisfying opacity for stochastic control systems modeled as general Markov decision processes (gMDPs). We also propose verification methods tailored to the new notions of opacity for finite gMDPs by using value iteration techniques. Then, a new notion called approximate opacity-preserving stochastic simulation relation is proposed, which captures the distance between two systems' behaviors in terms of preserving opacity. Based on this new system relation, we show that one can verify opacity for stochastic control systems using their abstractions (modeled as finite gMDPs). We also discuss how to construct such abstractions for a class of gMDPs under certain stability conditions.

On Approximate Opacity of Stochastic Control Systems

TL;DR

This work defines a quantitative, horizon-bounded notion of opacity for stochastic control systems modeled as general Markov decision processes, introducing -approximate initial-state and current-state opacity. It provides finite-gMDP verification methods via specialized estimators and value iteration, enabling efficient checking of opacity on finite abstractions. To scale to infinite-state systems, the authors introduce opacity-preserving stochastic simulation relations (InitSOP and CurSOP) based on -lifting, which guarantee that opacity properties transfer between a concrete gMDP and its finite abstraction with explicit error terms. They show how to construct opacity-preserving finite abstractions under -ISS stability, and demonstrate the approach on a road-traffic case study where opacity guarantees transition from abstraction to the concrete system. The results offer a scalable, abstraction-based pathway for verifying and potentially designing controllers that enforce opacity in stochastic CPS.

Abstract

This paper investigates an important class of information-flow security property called opacity for stochastic control systems. Opacity captures whether a system's secret behavior (a subset of the system's behavior that is considered to be critical) can be kept from outside observers. Existing works on opacity for control systems only provide a binary characterization of the system's security level by determining whether the system is opaque or not. In this work, we introduce a quantifiable measure of opacity that considers the likelihood of satisfying opacity for stochastic control systems modeled as general Markov decision processes (gMDPs). We also propose verification methods tailored to the new notions of opacity for finite gMDPs by using value iteration techniques. Then, a new notion called approximate opacity-preserving stochastic simulation relation is proposed, which captures the distance between two systems' behaviors in terms of preserving opacity. Based on this new system relation, we show that one can verify opacity for stochastic control systems using their abstractions (modeled as finite gMDPs). We also discuss how to construct such abstractions for a class of gMDPs under certain stability conditions.
Paper Structure (15 sections, 12 theorems, 57 equations, 6 figures)

This paper contains 15 sections, 12 theorems, 57 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. General Markov Decision Processes
  4. Approximate Opacity for gMDPs
  5. Verification of Approximate Opacity for Finite GMDPs
  6. Verification of Approximate Initial-State Opacity
  7. Verification of Approximate Current-State Opacity
  8. Approximate Opacity-preserving Stochastic Simulation Relations
  9. Initial-State Opacity-Preserving Stochastic Simulation Relation
  10. Current-State Opacity-Preserving Stochastic Simulation Relation
  11. Finite Abstractions for GMDPs
  12. Finite General Markov Decision Processes
  13. Establishing Opacity-Preserving Stochastic Simulation Relations
  14. Case Study
  15. Conclusion and Discussions

Key Result

Lemma 4.2

Consider a finite gMDP $\Sigma\!=\!(X,X_0,X_S,U,T,$$Y,h)$ and its approximate initial-state estimator $\Sigma_{I,obs}$ as in Definition def:iniesti. For any initial state $x_0$ and any input sequence $\nu= (\nu(0), \dots, \nu(n-1))$, we have where $L_{\mathcal{I}_\varepsilon}^n$ is the set of initial-state secure state trajectories as in secureinitialset within time horizon $n \in \mathbb{N}$, an

Figures (6)

  • Figure 1: States marked by red denote secret states, states marked by sourceless arrows denote initial states, and the output map is specified by the value associated to each state. For each transition, the input and state transition probability are also specified on the arrows.
  • Figure 2: Example of approximate initial-state estimators.
  • Figure 3: Example of $(\epsilon, \delta)$-InitSOP from $\hat{\Sigma}$ to $\Sigma$, i.e., $\hat{\Sigma} \preceq_{{\mathcal{I}}^{\epsilon}_\delta} {\Sigma}$.
  • Figure 4: A road traffic model observed by an outside intruder.
  • Figure 5: A state trajectory (Traj.1) initiated from a secret initial condition and its ($\varepsilon$-close) output equivalent trajectory (Traj.2) started from a non-secret initial condition. The shaded area in light blue represents the $\varepsilon$-band around Traj.1.
  • ...and 1 more figures

Theorems & Definitions (30)

  • Definition 2.1
  • Definition 3.1
  • Example 3.2
  • Remark 3.3
  • Remark 3.4
  • Remark 3.5
  • Definition 4.1
  • Lemma 4.2
  • Lemma 4.3
  • Lemma 4.4
  • ...and 20 more