Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification and Enforcement of Strong State-Based Opacity for Discrete-Event Systems

Xiaoguang Han, Kuize Zhang, Zhiwu Li

TL;DR

The algorithm for enforcing Inf-SSO has lower time complexity than the existing one in the literature, and does not depend on any assumption, and the algorithms for enforcing the above-mentioned four notions of strong SBO are designed using the proposed two concurrent-composition structures.

Abstract

In this paper, we investigate the verification and enforcement of strong state-based opacity (SBO) in discrete-event systems modeled as partially-observed (nondeterministic) finite-state automata, including strong K-step opacity (K-SSO), strong current-state opacity (SCSO), strong initial-state opacity (SISO), and strong infinite-step opacity (Inf-SSO). They are stronger versions of four widely-studied standard opacity notions, respectively. We firstly propose a new notion of K-SSO, and then we construct a concurrent-composition structure that is a variant of our previously-proposed one to verify it. Based on this structure, a verification algorithm for the proposed notion of K-SSO is designed. Also, an upper bound on K in the proposed K-SSO is derived. Secondly, we propose a distinctive opacity-enforcement mechanism that has better scalability than the existing ones (such as supervisory control). The basic philosophy of this new mechanism is choosing a subset of controllable transitions to disable before an original system starts to run in order to cut off all its runs that violate a notion of strong SBO of interest. Accordingly, the algorithms for enforcing the above-mentioned four notions of strong SBO are designed using the proposed two concurrent-composition structures. In particular, the designed algorithm for enforcing Inf-SSO has lower time complexity than the existing one in the literature, and does not depend on any assumption. Finally, we illustrate the applications of the designed algorithms using examples.

Verification and Enforcement of Strong State-Based Opacity for Discrete-Event Systems

TL;DR

The algorithm for enforcing Inf-SSO has lower time complexity than the existing one in the literature, and does not depend on any assumption, and the algorithms for enforcing the above-mentioned four notions of strong SBO are designed using the proposed two concurrent-composition structures.

Abstract

In this paper, we investigate the verification and enforcement of strong state-based opacity (SBO) in discrete-event systems modeled as partially-observed (nondeterministic) finite-state automata, including strong K-step opacity (K-SSO), strong current-state opacity (SCSO), strong initial-state opacity (SISO), and strong infinite-step opacity (Inf-SSO). They are stronger versions of four widely-studied standard opacity notions, respectively. We firstly propose a new notion of K-SSO, and then we construct a concurrent-composition structure that is a variant of our previously-proposed one to verify it. Based on this structure, a verification algorithm for the proposed notion of K-SSO is designed. Also, an upper bound on K in the proposed K-SSO is derived. Secondly, we propose a distinctive opacity-enforcement mechanism that has better scalability than the existing ones (such as supervisory control). The basic philosophy of this new mechanism is choosing a subset of controllable transitions to disable before an original system starts to run in order to cut off all its runs that violate a notion of strong SBO of interest. Accordingly, the algorithms for enforcing the above-mentioned four notions of strong SBO are designed using the proposed two concurrent-composition structures. In particular, the designed algorithm for enforcing Inf-SSO has lower time complexity than the existing one in the literature, and does not depend on any assumption. Finally, we illustrate the applications of the designed algorithms using examples.
Paper Structure (12 sections, 11 theorems, 6 equations, 20 figures, 3 algorithms)

This paper contains 12 sections, 11 theorems, 6 equations, 20 figures, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Verification of strong K-step opacity
  4. The notion of strongK-step opacity
  5. The structure of concurrent composition
  6. Verification for K-SSO in Definition \ref{['de:3.1']}
  7. An upper bound on K in K-SSO in Definition \ref{['de:3.1']}
  8. Enforcement of strong SBO
  9. Problem formulation
  10. Enforcement of K-SSO in Definition \ref{['de:3.1']}
  11. Enforcement of SCSO, SISO, and Inf-SSO
  12. Concluding remarks

Key Result

Theorem 3.1

Given a system $G=(X,\Sigma,\delta,X_0)$, a projection map $P$ w.r.t. a set $\Sigma_o$ of observable events, a set $X_{S}$ of secret states, and a non-negative integer $K$, let $Cc(\hat{G},\tilde{G}_{obs})$ be the corresponding concurrent composition. $G$ is $K$-SSO in Definition de:3.1 w.r.t. $\Sig

Figures (20)

  • Figure 1: The automaton $G$ considered in Example \ref{['ex:3.1']}.
  • Figure 2: The constructed automata $Obs(G)$, $\hat{G}$, $\tilde{G}$, $\tilde{G}_{obs}$, and $Cc(\hat{G},\tilde{G}_{obs})$ from the automaton $G$ shown in Fig. \ref{['Fig1']}.
  • Figure 3: A automaton $G$ in which $\Sigma_o=\{a,b\}$, $X_0=\{0\}$, and $X_S=\{1\}$.
  • Figure 4: The subautomaton $G^1$ and its corresponding concurrent composition $Cc(\hat{G}^1,\tilde{G}^1_{obs})$.
  • Figure 5: The concurrent composition $Cc(G^1,Obs(G^1))$ for the subautomaton $G^1$ shown in Fig \ref{['Fig:subfig4a']}.
  • ...and 15 more figures

Theorems & Definitions (40)

  • Remark 1
  • Definition 1: Falcone(2015)
  • Definition 2: Zhang(2023b)
  • Definition 3
  • Remark 2
  • Remark 3
  • Definition 4: Concurrent Composition
  • Remark 4
  • Theorem 3.1
  • proof
  • ...and 30 more