Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications

Bohan Cui, Ziyue Ma, Shaoyuan Li, Xiang Yin

TL;DR

This paper investigates the property verification problem for partially-observed DES from a new perspective and presents a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer.

Abstract

In this paper, we investigate the property verification problem for partially-observed DES from a new perspective. Specifically, we consider the problem setting where the system is observed by two agents independently, each with its own observation. The purpose of the first agent, referred to as the low-level observer, is to infer the actual behavior of the system, while the second, referred to as the high-level observer, aims to infer the knowledge of Agent 1 regarding the system. We present a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer. A typical instance of this definition is the notion of high-order opacity, which specifies that the intruder does not know that the system knows some critical information. This formalization is very general and supports any user-defined information-state-based knowledge between the two observers. We demonstrate how the general definition of epistemic properties can be applied in different problem settings such as information leakage diagnosis or tactical cooperation without explicit communications. Finally, we provide a systematic approach for the verification of epistemic properties. Particularly, we identify some fragments of epistemic properties that can be verified more efficiently.

On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications

TL;DR

This paper investigates the property verification problem for partially-observed DES from a new perspective and presents a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer.

Abstract

In this paper, we investigate the property verification problem for partially-observed DES from a new perspective. Specifically, we consider the problem setting where the system is observed by two agents independently, each with its own observation. The purpose of the first agent, referred to as the low-level observer, is to infer the actual behavior of the system, while the second, referred to as the high-level observer, aims to infer the knowledge of Agent 1 regarding the system. We present a general notion called the epistemic property capturing the inference from the high-level observer to the low-level observer. A typical instance of this definition is the notion of high-order opacity, which specifies that the intruder does not know that the system knows some critical information. This formalization is very general and supports any user-defined information-state-based knowledge between the two observers. We demonstrate how the general definition of epistemic properties can be applied in different problem settings such as information leakage diagnosis or tactical cooperation without explicit communications. Finally, we provide a systematic approach for the verification of epistemic properties. Particularly, we identify some fragments of epistemic properties that can be verified more efficiently.
Paper Structure (17 sections, 9 theorems, 40 equations, 5 figures)

This paper contains 17 sections, 9 theorems, 40 equations, 5 figures.

Table of Contents

  1. General Definition of Epistemic Properties
  2. Two-Agent Knowledge Model
  3. Knowledge of the Low-Level Observer
  4. Knowledge of the High-Level Observer
  5. Applications of Epistemic Properties
  6. Knowledge Security
  7. Invisible Attacker
  8. Release Awareness
  9. Tacit Cooperation
  10. Other Properties
  11. Verification of Epistemic Properties
  12. General Algorithm by Double-Estimators
  13. Twin-Estimators
  14. State-Pair-Estimators
  15. Epistemic Properties with Delayed Information
  16. ...and 2 more sections

Key Result

Proposition 1

System $G$ is high-order opaque (w.r.t. $T_\texttt{spec}$, $\mathcal{H}_a$ and $\mathcal{H}_o$) if and only if $G\models \langle \forall, \texttt{Dis}_o,\texttt{T},\texttt{U} \rangle$.

Figures (5)

  • Figure 2: A motivating example with $\Sigma_{o}=\{r,g\}$, $\Sigma_{a}=\{b,g\}$.
  • Figure 3: System $G$ with $\Sigma_o=\{b,d\}$ and $\Sigma_a=\{a,b\}$.
  • Figure 4: The construction of $Obs_D(G)$ for $G$.
  • Figure 5: twin-estimator of the system $G$.
  • Figure 6: State-pair-estimator $Obs_P(G)$ for $G$.

Theorems & Definitions (23)

  • Definition 1: IS-Based Knowledge
  • Definition 2: Epistemic Properties
  • Definition 3: High-Order Opacity
  • Proposition 1
  • Definition 4: Intrusion Undetectability
  • Proposition 2
  • Definition 5: Epistemic Diagnosability
  • Proposition 3
  • Definition 6: High-Order Detectability
  • Proposition 4
  • ...and 13 more