Security Quantification for Discrete Event Systems Based on the Worth of States

Abstract

This work addresses the problem of quantifying opacity for discrete event systems. We consider a passive intruder who knows the overall structure of a system but has limited observational capabilities and tries to infer the secret of this system based on the captured information flow. Researchers have developed various approaches to quantify opacity to compensate for the lack of precision of qualitative opacity in describing the degree of security of a system. Most existing works on quantifying opacity study specified probabilistic problems in the framework of probabilistic systems, where the behaviors or states of a system are classified as secret or non-secret. In this work, we quantify opacity by a state-worth function, which associates each state of a system with the worth it carries. To this end, we present a novel category of opacity, called worthy opacity, characterizing whether the worth of information exposed to the outside world during the system’s evolution is below a threshold. We first provide an online approach for verifying worthy opacity using the notion of a run matrix proposed in this research. Then, we investigate a class of systems satisfying the so-called 1-cycle returned property and present a worthy opacity verification algorithm for this class. Finally, an example in the context of smart buildings is provided.

1. Introduction

With global urbanization, cities are growing in size and population, and the proportion of people living in urban areas is expected to grow to 68% by 2050 [1], creating inevitable challenges to urban residents due to limited resources and services. The concept of smart cities has been proposed to efficiently deploy public resources, improve social governance, and promote sustainable urban development. Currently, smart cities are being intensively established around the world; for example, there are already more than 500 in China [2].

Buildings provide the physical space required for people to carry out various social, economic, and cultural activities, and are one of the areas where the Internet of Things (IoT) would make significant impacts [3]. Smart buildings improve the energy efficiency, operational efficiency, security, and comfort of the living or working environment by integrating advanced technologies and systems [4,5]. For example, people use the model predictive control approach for temperature control in smart buildings, reducing operating costs and improving thermal comfort [6,7]. However, IoT devices in smart buildings generate a large amount of data, which can pose many potential threats. Deciding how to analyze the security of smart buildings is becoming an increasingly important issue and has attracted a lot of attention over the past few years [8,9,10].

In this article, we study an information flow security property of great interest: opacity, within the discrete event system (DES) framework, where DES can describe the state transition relationships between events in an IoT, thereby assisting us in understanding and analyzing IoT behavior. Opacity was originally introduced in 2004 for the analysis of cryptographic protocols [11]. Later, it is taken as a general information flow security framework for a DES interacting with a passive intruder. Many kinds of information flow security properties can be formulated as opacity, such as non-interference [12], anonymity [13], etc. Roughly speaking, opacity is a type of confidentiality property that characterizes whether certain secret information from a system can be deduced by outside observers that may be malicious.

In the context of DESs, opacity is classified into language-based and state-based opacity, depending on the defined secret [14]. Language-based opacity has been studied with models such as automata [13] and Petri nets [15], where the secret is defined as a language. In general, this type of opacity can be further classified as strong and weak opacity, as opposed to state-based opacity, which has a wide range of classifications depending on the state of interest. For example, current-state opacity [16,17] has been proposed to take the system’s current state as a secret and determine whether the system reveals this secret during its evolution. Similarly, initial-state opacity [18] and initial-and-final-state opacity [19] are suggested when the secret is defined as a set of initial states or a set of secret state pairs. The notions of K-step opacity [20] and infinite-step opacity [21] are developed when the delayed information of a system is concerned, and pre-opacity [22] is formulated when the intention of a system needs to be kept secret.

All of the aforementioned notions of opacity describe a system in a binary way, where the system is either opaque or non-opaque. It has been noted that qualitative opacity is not accurate enough in assessing the information obtained by passive attackers [23]. For instance, a system that violates qualitative opacity with a very low probability and one that violates qualitative opacity with a very high probability are considered insecure. However, their degree of security is different [24]. The authors of [25] introduce game theory’s ideas into probabilistic automata and propose a model of probabilistic resource automata based on which the current-state opacity is quantified.

The above-mentioned studies on quantification of opacity are basically based on probabilistic systems. However, a probabilistic model is much more difficult to be abstracted than a non-probabilistic version. The study in [26] is the first work that introduces the quantification of opacity into non-probabilistic DES. Considering that the essence of opacity is to explore the observational equivalent strings, the authors developed a method to calculate the opacity degree of a system by computing the dispersion among non-secret runs and secret equivalents.

In this work, we investigate the quantification of opacity from a new perspective by describing the worth of information that each system state carries in terms of a state-worth function. Then, we introduce a new type of opacity, called worthy opacity, to describe whether the worth of information exposed to the outside world in the system’s evolution meets the security requirements. We consider an intruder who knows the whole structure of a system but has limited observation capabilities. Unlike the general notions of state-based opacity, we do not explicitly treat a secret as a specific sub-set of states since the state-worth function describes the importance of each system state. We show that current-state opacity is strictly weaker than worthy opacity. The proposed notion of worthy opacity is closely related to the notion of opacity degree in [26]. The contributions of this article can be summarized as follows:   

• A novel notion of worthy opacity is proposed to quantitatively characterize the worth of a system available to an intruder;
• An online algorithm is provided to verify worthy opacity;
• A system property called 1-cycle returned is defined, and an offline verification algorithm for the system’s worthy opacity satisfying this property is presented;
• It is shown that worthy opacity provides a more granular partitioning of the system than current-state opacity.

The rest of this article is organized as follows. Section 2 recalls the necessary preliminaries. The notion of worthy opacity is proposed in Section 3. In Section 4, two effective algorithms for the verification of worthy opacity are reported. Finally, Section 5 concludes this research.

2. Preliminaries

Symbols $\mathbb{R}$, ${\mathbb{R}}_{\ge 0}$, $\mathbb{N}$, and ${\mathbb{Z}}^{+}$ are specified to denote the sets of real numbers, non-negative real numbers, non-negative integers, and positive integers, respectively. The ceiling function of a real number $x\in \mathbb{R}$, denoted as $\lceil x\rceil$, is defined as the smallest integer that is not smaller than x. For a vector $\mathit{v}$, ${\left[\mathit{v}\right]}_i$ is used to denote the i-th entry of $\mathit{v}$. Given a matrix $\mathit{M}$, its $(i,j)$-th entry is denoted as ${\left[\mathit{M}\right]}_{i,j}$. The transpose of a vector $\mathit{v}$ is denoted by ${\mathit{v}}^T$. Given a k-dimensional vector $\mathit{v}$, its 1-norm is defined as the sum of the absolute values of each entry, i.e., $∥\mathit{v}∥={\sum }_{i=1}^k\left|{\left[\mathit{v}\right]}_i\right|$. The L1-normalization of a vector $\mathit{v}$, denoted by $\mathtt{norm}\left(\mathit{v}\right)$ in this article, is defined as $\mathtt{norm}\left(\mathit{v}\right)=\mathit{v}/∥\mathit{v}∥$. Given an ordered pair $c=(a,b)$, we use $c\left(1\right)$ and $c\left(2\right)$ to denote its first and second components, namely, $c\left(1\right)=a$ and $c\left(2\right)=b$.

2.1. System Model

We define an alphabet as any non-empty finite set of events, denoted by E. A string over the alphabet E is a sequence of events taken out of E [27]. The length of a string s, written as $\left|s\right|$ (if X is a set, the notation $\left|X\right|$ denotes the cardinality of X. The distinction is usually clear from context), is the number of events contained in it, counting multiple occurrences of the same event. The string without any events is called the empty string and is denoted by $\epsilon$ with $\left|\epsilon \right|=0$. Given two strings $s_1$ and $s_2$, the concatenation of $s_1$ and $s_2$ is the sequence of events in $s_1$ followed by the sequence of events in $s_2$, denoted as $s_1·s_2$ or $s_1{s}_2$. We use the superscript notation $s^k$ to indicate that the string s is concatenated with itself k times.

Given an alphabet E, we denote by $E^k$ the set of all strings of length k, particularly, $E^0=\left\{\epsilon \right\}$. The set consisting of all finite-length strings defined over E is denoted by $E^{*}$, i.e., $E^{*}=E^0\cup E\cup E^2\cup \cdots$. Given an alphabet E, a language is a sub-set of $E^{*}$. Given two languages $L_1$ and $L_2$, the concatenation of $L_1$ and $L_2$ is $L_1{L}_2=\{s_1{s}_2\mid s_1\in L_1,s_2\in L_2\}$. In this article, we model a DES as a non-deterministic finite automaton, formally defined as follows.

Definition 1

(Non-deterministic Finite Automaton). A non-deterministic finite automaton (NFA) is a four-tuple $G=(Q,E,f,Q_0)$, where   

• $Q=\{q_1,q_2,\cdots ,q_N\}$ is the finite set of states;
• $E=\{e_1,e_2,\cdots ,e_M\}$ is the finite set of events associated with G;
• $f:Q\times E\to 2^Q$ (where $2^Q$ is the power set of Q) is the transition function, and $q^{\prime }\in f(q,e)$ means that there is a transition labeled by e from state q to state $q^{\prime }$;
• $Q_0\subseteq Q$ is the set of initial states.

If $Q_0$ in G is a singleton and the transition function of G is a partially defined function $Q\times E\to Q$, then G is called a deterministic finite automaton (DFA). The transition function f can be extended recursively from the domain $Q\times E$ to the domain $Q\times E^{*}$: $f(q,\epsilon )=\left\{q\right\}$ and $f(q,se)={\bigcup }_{q^{\prime }\in f(q,s)}f(q^{\prime },e)$ for all states $q\in Q$, where $s\in E^{*}$ and $e\in E$. The language generated by G from state $q\in Q$ is $\mathcal{L}(G,q)=\{s\in E^{*}\mid f(q,s)!\}$, where $f(q,s)!$ indicates that $f(q,s)$ is defined, i.e., $f(q,s)\ne \varnothing$. The language generated by G from a set of states $Q^{\prime }\subseteq Q$ is $\mathcal{L}(G,Q^{\prime })={\bigcup }_{q\in Q^{\prime }}\mathcal{L}(G,q)$. Naturally, the language generated by G is $\mathcal{L}\left(G\right)=\mathcal{L}(G,Q_0)$.

Formally an NFA G can be equivalently represented by a directed graph, with a set of nodes Q denoting states and a set of edges $\{q\stackrel{e}{⟶}{q}^{\prime }\mid q^{\prime }\in f(q,e)\}$ denoting transitions. A run in G starting from $q_{\left(0\right)}\in Q$ is a finite sequence of transitions $r:q_{\left(0\right)}\stackrel{e_{\left(1\right)}}{⟶}{q}_{\left(1\right)}\stackrel{e_{\left(2\right)}}{⟶}\cdots q_{(k-1)}\stackrel{e_{\left(k\right)}}{⟶}{q}_{\left(k\right)}$ (here, we use the numbers in parentheses to indicate the order in which states or events appear in the run, that is to say, $q_{\left(i\right)}$ is not necessarily equal to $q_i$ and $e_{\left(i\right)}$ is not necessarily equal to $e_i$), and the events extracted from it in order form the string associated with it, denoted by $\varphi \left(r\right)=e_{\left(1\right)}{e}_{\left(2\right)}\cdots e_{\left(k\right)}$ (we also say that r is a run on $\varphi \left(r\right)$ and use $last\left(r\right)=q_{\left(k\right)}$ to denote the ending state). We define the length of a run r as the length of the string $\varphi \left(r\right)$ associated with it, i.e., $\left|r\right|=\left|\varphi \right(r\left)\right|$. Given a run from state q to $q^{\prime }$ on a string s, we denote it as $q\stackrel{s}{⟶}{q}^{\prime }$; if a specific string associated with the run is not of interest, we denote it as $q\to q^{\prime }$. The set of all runs starting from state $q\in Q$ in G is denoted by $\mathrm{\Gamma }(G,q)$; the set of all runs generated by G is $\mathrm{\Gamma }\left(G\right)={\cup }_{q\in Q_0}\mathrm{\Gamma }(G,q)$. A run of length greater than zero that begins and ends at the same state is called a cycle.

2.2. Intruder Model and Opacity

In the general setting of studying opacity in DESs, it is assumed that the intruder is fully aware of the system’s structure but only partially observes the system’s behavior [14]. We follow this setting in our work and formalize it as the partial observability of events, where the set of events E is divided into an observable event set $E_o$ and an unobservable event set $E_{uo}$, i.e., $E=E_o\dot{\cup }{E}_{uo}$. Given a string $s\in E^{*}$ generated by G, the intruder’s observation is the output of the natural projection function $P:E^{*}\to E_o^{*}$, which is defined recursively as:

$$P\left(\epsilon \right)=\epsilon ;P\left(e\right)=\left\{\begin{array}{cc}e,\hfill & \mathrm{if}e\in E_o,\hfill \\ \epsilon ,\hfill & \mathrm{otherwise};\hfill \end{array}\right.$$

$$P\left(se\right)=P\left(s\right)·P\left(e\right)\mathrm{for}s\in E^{*},e\in E.$$

The unobservable reach of a state $q\in Q$ in G, denoted by $UR\left(q\right)$, is $UR\left(q\right)=\{q^{\prime }\in Q\mid \exists t\in E_{uo}^{*}:f(q,t)!,q^{\prime }\in f(q,t)\}$. This definition can be extended to a set of states $Q^{\prime }\subseteq Q$ by $UR\left(Q^{\prime }\right)={\bigcup }_{q\in Q^{\prime }}UR\left(q\right)$.

This work is an extension of state-based opacity, where the secret of a system is a sub-set of states $S\subseteq Q$. When a system generates a string $s\in E^{*}$, the intruder observes $P\left(s\right)$ and infers whether the system is in a secret state based on this observation and the system’s structure.

Definition 2

(Current-State Opacity [14]). Given a system $G=(Q,E,f,Q_0)$, a secret $S\subseteq Q$, and a set of observable events $E_o\subseteq E$, G is current-state opaque with respect to S and $E_o$, written as $(S,E_o)$-CSO, if

$$\forall q\in Q_0,\forall s\in \mathcal{L}(G,q)[f(q,s)\subseteq S]\Rightarrow \exists q^{\prime }\in Q_0,\exists s^{\prime }\in \mathcal{L}(G,q^{\prime })[P\left(s\right)=P\left(s^{\prime }\right),f(q^{\prime },s^{\prime })⊈S].$$

In plain words, a system being current-state opaque means that an intruder cannot infer whether the current state belongs to the secret, regardless of the sequence of events occurring in the system. Given an observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$, the current-state estimate associated with $\omega$ is $\mathcal{C}\left(\omega \right)=\{q\in Q\mid \exists q_0\in Q_0:s\in \mathcal{L}(G,q_0),q\in f(q_0,s),P\left(s\right)=\omega \}$, and the set of consistent strings is $\mathcal{S}\left(\omega \right)=\{s\in \mathcal{L}(G)\mid P(s)=\omega \}$.

Lemma 1

([28]). Given a system $G=(Q,E,f,Q_0)$, a secret $S\subseteq Q$, and a set of observable events $E_o\subseteq E$, G is $(S,E_o)$-CSO if and only if for any observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$, $\mathcal{C}\left(\omega \right)⊈S$.

By Lemma 1, to verify current-state opacity, we can construct the observer $G_{obs}$ of system G and check whether there exists a state in observer $G_{obs}$ that is a sub-set of S [16].

Definition 3.

Given a system $G=(Q,E,f,Q_0)$ and a set of observable events $E_o\subseteq E$, its observer is a DFA $G_{obs}=(X,E_{obs},f_{obs},x_0)$, where   

• $X\subseteq 2^Q$, with each state $x\subseteq Q$ being a state estimate generated by an intruder based on the evolution of G;
• $E_{obs}=E_o$ is the set of events that can be observed by an intruder;
• $f_{obs}(x,e)={\bigcup }_{q\in x}UR\left(f(q,e)\right)$;
• $x_0=UR\left(Q_0\right)$ is the initial state estimate.

Example 1.

Consider the system $G_1$ in Figure 1a, where $S=\{q_2,q_3\}$ and $E_o=\left\{e_1\right\}$. Clearly, by constructing the observer of $G_1$ as shown in Figure 1b, we can find that G is current-state opaque, since no state of $G_{1,obs}$ is a sub-set of S.

2.3. Some Counting Principles

As an essential part of combinatorics, counting objects with specific properties is indispensable for the study of DESs. Many different types of problems require us to count items. For instance, some notions of diagnosability are defined in terms of fault counting problems [29]. Counting is also required to determine the complexity of algorithms [30]. In addition, counting techniques are widely used in calculating the finite probability [31]. Our work is also inseparable from counting. This subsection recalls some critical counting principles [32].

Lemma 2

(Addition Principle). Suppose that a set S can be partitioned into pairwise disjoint parts $S_1,S_2,\cdots ,S_m$. The number of elements in S is the sum of the number of elements in each of its part, i.e., $\left|S\right|={\sum }_{i=1}^m\left|S_i\right|$.

We divide the problem into mutually exclusive cases for applying the addition principle. An alternative formulation of Lemma 2 is as follows: if there are m ways to complete a task, where the i-th way has $k_i$ ($i\in \{1,2,\cdots ,m\}$) choices, then there are ${\sum }_{i=1}^m{k}_i$ choices for completing that task.

Example 2.

Consider the system $G_1$ in Example 1. Suppose we want to find the number of cycles of length two in $G_1$. We divide these cycles by listing their start and end states. The number of 2-length cycles starting and ending in states $q_1$, $q_2$, $q_3$, and $q_4$ are 2, 2, 1, and 1, respectively. Therefore, the number of cycles of length two in $G_1$ is $2+2+1+1=6$.

Lemma 3

(Multiplication Principle). Let S be a set of m-tuples $(S_1,S_2,\cdots ,S_m)$, where the i-th component $S_i$ comes from a set of size $a_i$. The size of S is ${\prod }_{i=1}^m{a}_i$.

The multiplication principle is a corollary of Lemma 2. A useful formulation of Lemma 3 is as follows: suppose that a task can be decomposed into m consecutive steps. If step i can be performed in $a_i$ ways, and for each of these, step $i+1$ can be performed in $a_{i+1}$ ($i\in \{1,2,\cdots ,m-1\}$) ways, then the task itself can be accomplished in ${\prod }_{i=1}^m{a}_i$ ways.

Example 3.

Consider the system $G_1$ in Example 1. The number of 2-length runs starting from state $q_1$, passing through state $q_2$, and ending at state $q_3$ is 1, as the number of 1-length runs from state $q_1$ to $q_2$ and state $q_2$ to $q_3$ is 1, respectively.

Lemma 4

(Generalized Pigeonhole Principle [33]). If p objects are placed into q boxes, then at least one box contains a minimum of $\lceil p/q\rceil$ objects.

3. Notions of Worthy Opacity

In this section, we first provide the definition of worthy opacity for DESs, and then compare it with the widely studied current-state opacity. Existing notions of state-based opacity, both qualitative and quantitative, divide the set of states into secret or non-secret. However, various degrees of confidentiality exist for different states that are part of the same secret. For example, a spy trying to hide his/her tracks would wish neither his/her hiding place be exposed nor the convenience store he/she regularly visits be discovered. Nevertheless, it is clear that the secrecy of the hiding place is more valuable. To describe the degree of confidentiality of individual states, we introduce the notion of state-worth function.

Definition 4

(State-worth Function). Given a system $G=(Q,E,f,Q_0)$, a state-worth function is a mapping that assigns a non-negative number to a state, defined as $\mathsf{\Delta }:Q\to {\mathbb{R}}_{\ge 0}$.

Note that instead of describing the degree of confidentiality of each state in the secret (a sub-set of the state set), we define the state-worth function as assigning a worth to each state of the system. This is a more general approach than splitting the states into two categories. When linked to the conventional notion of secret, we can use this function to divide secrets: each state possesses a worth, and states carrying worth above a certain threshold are considered constituent elements of a secret.

Example 4.

Suppose that we have a bank account with a deposit limit of $300 and a balance of $100. The amount we deposit into our account or spend at a point of sale (POS) is $100 each time. In addition, a private detective is lying in wait at the bank door and wants to know our financial situation, and he can only find out that we deposit but not that we use POS spending.

Then, the above scenario can be modeled with the system of Example 1; event $e_1$ represents the deposit of $100 while event $e_2$ represents the POS spending of $100. Each state represents the balance of the bank account, and naturally, we can take the balance represented by each state as the value of the state-worth function, i.e., $\mathsf{\Delta }\left(q_1\right)=100$, $\mathsf{\Delta }\left(q_2\right)=200$, $\mathsf{\Delta }\left(q_3\right)=300$, and $\mathsf{\Delta }\left(q_4\right)=0$. If we treat a bank balance over $100 as a secret, then it is $S=\{q\mid \mathsf{\Delta }\left(q\right)>100\}=\{q_2,q_3\}$, as shown in Example 1.

In addition, the existing notions of opacity are not sufficiently refined for depicting the evolution of a system. In fact, the most fundamental element of a system corresponding to an observation is the set of runs rather than the set of strings, as shown in Figure 2. Specifically, given a run $r\in \mathrm{\Gamma }\left(G\right)$ of a system G, we can obtain the string $\varphi \left(r\right)\in \mathcal{L}\left(G\right)$ by extracting the sequence of events occurring in it, also commonly considered as the logical behavior of a system, and then an intruder obtains the corresponding observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$ based on the observability of the events.

Definition 5.

Given a system $G=(Q,E,f,Q_0)$ with a set of observable events $E_o\subseteq E$ and an observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$, the set of consistent runs and the set of consistent runs ending in state $q\in Q$ are defined as $\Phi \left(\omega \right)=\{r\in \mathrm{\Gamma }(G)\mid \exists s\in \mathcal{S}(\omega ):\varphi (r)=s\}$ and ${\Phi }_q\left(\omega \right)=\{r\in \Phi \left(\omega \right)\mid last\left(r\right)=q\}$, respectively.

Intuitively, given an observation $\omega$, the set of consistent runs $\Phi \left(\omega \right)$ is the set of all runs for which the system can generate that observation, and accordingly, the set ${\Phi }_q\left(\omega \right)$ is the set of all runs that cause the system to produce that observation and reach state q.

Definition 6

(Worthy Opacity). Given a system $G=(Q,E,f,Q_0)$ with state-worth function Δ, a set of observable events $E_o\subseteq E$, and a non-negative value $K\in {\mathbb{R}}_{\ge 0}$, an observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$ is worthy opaque with respect to $E_o$, Δ, and K (denoted by $(E_o,\mathsf{\Delta },K)$-WO) if

$$\sum _{q\in Q}{\alpha }_{\omega }\left(q\right)·\mathsf{\Delta }\left(q\right)\le K,$$

(1)

where ${\alpha }_{\omega }\left(q\right)=\left|{\Phi }_q\left(\omega \right)\right|/|\Phi \left(\omega \right)|$. System G is said to be worthy opaque with respect to $E_o$, Δ, and K ($(E_o,\mathsf{\Delta },K)$-WO) if all observations $\mathsf{\omega }\in P\left(\mathcal{L}\right(G\left)\right)$ are $(E_o,\mathsf{\Delta },K)$-WO.

Note that ${\alpha }_{\omega }\left(q\right)$ in Definition 6 can be viewed as the intruder’s probability estimate of the current state of the system as q after observing $\omega$, i.e., the probability of system G in state $q\in \mathcal{C}\left(\omega \right)$ when observation $\omega$ is generated is implicitly defined as the number of runs in which the system generates observation $\omega$ and ends up in state q divided by the number of all runs that can generate observation $\omega$. Then, the left-hand side of (1) shows the worth the system is expected to expose for generating the observation $\omega$. That is to say, a system is worthy opaque if the worth it exposes to the outside world during its evolution does not exceed a certain threshold.

Example 5.

Consider the situation in Example 4, which is modeled as the system $G_1$ of Example 1. Suppose that the private detective sees that we deposit $100 in the bank, i.e., the system $G_1$ produces the observation $e_1$. We have $\Phi \left(e_1\right)=\{q_1\stackrel{e_1}{⟶}{q}_2\stackrel{e_2}{⟶}{q}_1,q_1\stackrel{e_2}{⟶}{q}_4\stackrel{e_1}{⟶}{q}_1,q_1\stackrel{e_1}{⟶}{q}_2,q_1\stackrel{e_2}{⟶}{q}_4\stackrel{e_1}{⟶}{q}_1\stackrel{e_2}{⟶}{q}_4,q_1\stackrel{e_1}{⟶}{q}_2\stackrel{e_2}{⟶}{q}_1\stackrel{e_2}{⟶}{q}_4\}$. Thus, we have $\left|{\Phi }_{q_1}\left(e_1\right)\right|=2$, $\left|{\Phi }_{q_2}\left(e_1\right)\right|=1$, $\left|{\Phi }_{q_4}\left(e_1\right)\right|=2$, and $|\Phi \left(e_1\right)|=5$, leading to ${\alpha }_{e_1}\left(q_1\right)=2/5$, ${\alpha }_{e_1}\left(q_2\right)=1/5$, and ${\alpha }_{e_1}\left(q_4\right)=2/5$. By (1), we have ${\sum }_{q\in Q}{\alpha }_{\omega }\left(q\right)·\mathsf{\Delta }\left(q\right)=2/5·100+1/5·200+2/5·0=80$, implying that observation $e_1$ is $(E_o,\mathsf{\Delta },80)$-WO. In plain words, the worth of information revealed to the outside world by observation $e_1$ is 80, which is a reasonable inference that the private detective can make.

Notice that the probabilities implied in Definition 6 are based on a uniform distribution over the set of consistent runs, which implies that the set $\Phi \left(\omega \right)$ must be finite, since there is no uniform distribution over infinite countable sets; otherwise the additivity of the probability axioms [31] is violated. Therefore, we have the following assumption on system G.

Assumption 1.

There are no unobservable cycles in the system G, where an unobservable cycle $c_u$ is a cycle such that $P\left(\varphi \left(c_u\right)\right)=\epsilon$.

The above assumption ensures that, for each observation, the set of consistent runs is finite (as shown in Proposition 1), and this assumption is also a general one when the system is modeled as a Petri net and the problem is analyzed using the notion of a basis reachability graph [28].

Proposition 1.

  Given a system $G=(Q,E,f,Q_0)$ with a set of observable events $E_o\subseteq E$, the set $\Phi \left(\omega \right)$ is finite for any observation $\omega \in P\left(\mathcal{L}\right(G\left)\right)$ if there are no unobservable cycles in G.

Proof. 

We first show that system G can generate no more than $N^{k+1}{M}^k$ runs of length k, where N is the number of states and M is the number of events in G. Note that we can consider a k-length run as a cross-arrangement of $k+1$ states and k events, provided that the transition function f is satisfied and $q_{\left(0\right)}\in Q_0$. The number of k-length runs is maximized by setting $Q_0=Q$ and $f(q,e)=Q$ (for any $q\in Q$ and $e\in E$). In this way, each state and each event in a run can be arbitrarily selected from N states and M events, respectively. In other words, the number of k-length runs cannot exceed $N^{k+1}{M}^k$.

Then, we prove the proposition by contrapositive. Suppose that there exists an observation $\omega =o_{\left(1\right)}{o}_{\left(2\right)}\cdots o_{\left(l\right)}$ such that the set $\Phi \left(\omega \right)$ is infinite. The length of runs in set $\Phi \left(\omega \right)$ can be greater than any given positive integer L. Otherwise, the number of runs in $\Phi \left(\omega \right)$ cannot exceed ${\sum }_{i=1}^L{N}^{i+1}{M}^i$, which implies that $\Phi \left(\omega \right)$ is finite.

Now, let $L=N·(l+2)-1$, we can find a run

$$r_L=q_{\left(0\right)}\stackrel{e_{\left(1\right)}}{⟶}{q}_{\left(1\right)}\stackrel{e_{\left(2\right)}}{⟶}\cdots q_{(N·(l+2)-1)}\stackrel{e_{(N·(l+2\left)\right)}}{⟶}{q}_{(N·(l+2\left)\right)},$$

whose length is greater than L. By Lemma 4, we can obtain that there is a state $q_d$ of G that is duplicated at least $l+2$ times in $r_L$. This implies that there are at least $l+1$ cycles in $r_L$ that begin and end with state $q_d$. Since the length of $\omega$ is $l<l+1$, we conclude that at least one of these $l+1$ cycles is unobservable, which completes the proof. □

Recall that in the research of state-based opacity, the secret is defined as a sub-set of system states. In general, secret states are more valuable than non-secret states. With this consideration, we can relate current-state opacity to the proposed worthy opacity.

Proposition 2.

Given a system $G=(Q,E,f,Q_0)$ with state-worth function Δ, a secret $S=\{q\mid \mathsf{\Delta }(q)>K\}$ ($K\in {\mathbb{R}}_{\ge 0}$), and a set of observable events $E_o\subseteq E$, G is $(S,E_o)$-CSO, if G is $(E_o,\mathsf{\Delta },K)$-WO.

Proof. 

By contrapositive, suppose that G is not $(S,E_o)$-CSO. By Lemma 1, there exists an observation $\omega$ such that $\mathcal{C}\left(\omega \right)\subseteq S$. That is, for any $q\in \mathcal{C}\left(\omega \right)$, $\mathsf{\Delta }\left(q\right)>K$ holds, which leads to the fact that G is not $(E_o,\mathsf{\Delta },K)$-WO. □

Note that the converse of the above proposition does not hold, as illustrated by the following example.

Example 6.

Consider the system $G_2$ in Figure 3a, where $E_o=E=\left\{e_1\right\}$. Let $\mathsf{\Delta }\left(q_1\right)=50$, $\mathsf{\Delta }\left(q_2\right)=200$, and $S=\{q\mid \mathsf{\Delta }\left(q\right)>100\}=\left\{q_2\right\}$. It is not difficult to verify that system $G_2$ is $(S_2,E_o)$-CSO. By analysis, we see that the evolution of $G_2$ satisfies

Table 1. Number of runs in $G_2$.

Observation $\mathit{\omega }$ ($\mathit{i}\in {\mathbb{Z}}^{+}$)	$\left|{\mathsf{\Phi }}_{{\mathit{q}}_{\mathbf{1}}}\left(\mathit{\omega }\right)\right|$	$\left|{\mathsf{\Phi }}_{{\mathit{q}}_{\mathbf{2}}}\left(\mathit{\omega }\right)\right|$
$\epsilon$	1	0
${e_1}^i$	$2^{i-1}$	$2^{i-1}$

. From Definition 6, we find that the system is $(E_o,\mathsf{\Delta },125)$-WO, not $(E_o,\mathsf{\Delta },100)$-WO.

4. Verifying Worthy Opacity

Intuitively, to verify the worthy opacity of a given system G, we need to check whether (1) holds for all $\omega \in P\left(\mathcal{L}\right(G\left)\right)$, which means that the value of ${\alpha }_{\omega }\left(q\right)$ needs to be computed for all $q\in Q$. In general, this requires an exhaustive enumeration of all possible strings that can be generated by G, which may require infinite memory and thus render the problem unsolvable. In this section, we first provide an online verification procedure, and then propose an algorithm to identify a particular class of systems and verify their worthy opacity.

4.1. Online Verification of an Observation

Given an observation $\omega$, we develop a notion of run matrix to compute the cardinality of a set ${\Phi }_q\left(\omega \right)$ (for any $q\in Q$) based on the transition matrix of automata.

Definition 7

(Transition Matrix [34]). Given an event $e\in E$ of a system $G=(Q,E,f,Q_0)$, the transition matrix ${\mathit{T}}_e$ is an $N\times N$ matrix, where the typical entry ${\left[{\mathit{T}}_e\right]}_{i,j}$ is equal to one if $q_i\in f(q_j,e)$ and to zero otherwise.

Example 7.

Consider the system in Example 1. The transition matrices associated with events $e_1$ and $e_2$ are, respectively:

$${\mathit{T}}_{e_1}=\left[\begin{array}{cccc}0& 0& 0& 1\\ 1& 0& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 0& 0\end{array}\right],{\mathit{T}}_{e_2}=\left[\begin{array}{cccc}0& 1& 0& 0\\ 0& 0& 1& 0\\ 0& 0& 0& 0\\ 1& 0& 0& 0\end{array}\right].$$

As runs are composed of transitions, we can utilize the transition matrix to calculate the number of runs between two states on a given string $s\in E^{*}$. Based on the idea of a transition matrix, we propose the notion of a run matrix.

Definition 8

(Run Matrix). Given a system $G=(Q,E,f,Q_0)$ and a string $s\in E^{*}$, the run matrix ${\mathit{R}}_s$ is an $N\times N$ matrix whose typical entry ${\left[{\mathit{R}}_s\right]}_{i,j}$ is equal to the number of runs from $q_j$ to $q_i$ on string s.

Recall that the values of transition function f of system G are sub-sets of states rather than multi-sets [35], which means that given a state q and an event e, the number of runs from state q to $q^{\prime }$ on the one-length string e is one if $q^{\prime }\in f(q,e)$ and zero otherwise. This coincides with the definition of the transition matrix; hence, ${\mathit{R}}_e={\mathit{T}}_e$ for all $e\in E$. For the empty string $\epsilon$, to fit the extended definition of transition function, we have ${\mathit{R}}_{\epsilon }=\mathit{I}$, where $\mathit{I}$ is an identity matrix of size N.

Remark 1.

For a string $s\notin \mathcal{L}(G,Q)$, its corresponding run matrix is a null matrix, indicating no run on s in G from whatever state it starts in.

Even though we specify the run matrices associated with strings of length zero and one for a given system G, it is still a problem to compute the run matrix associated with a string s of length greater than one, which is a more general case. Before we introduce the computation, we prove the following two properties of run matrices.

Proposition 3.

Given two strings $s_1$ and $s_2$ that have corresponding run matrices ${\mathit{R}}_{s_1}$ and ${\mathit{R}}_{s_2}$, respectively,   

(1) 

In the case that $s_1$ and $s_2$ are not identical, the number of runs on string $s_1$ or $s_2$ can be described by matrix ${\mathit{R}}_{s_1+s_2}={\mathit{R}}_{s_1}+{\mathit{R}}_{s_2}$, i.e., the number of runs from state $q_j$ to $q_i$ on string $s_1$ or $s_2$ is ${\left[{\mathit{R}}_{s_1+s_2}\right]}_{i,j}$;

(2) 

The number of runs on string $s_1{s}_2$ can be described by matrix ${\mathit{R}}_{s_1{s}_2}={\mathit{R}}_{s_2}·{\mathit{R}}_{s_1}$, i.e., the number of runs from state $q_j$ to $q_i$ on string $s_1{s}_2$ is ${\left[{\mathit{R}}_{s_1{s}_2}\right]}_{i,j}$.

Proof. 

(1) As $s_1\ne s_2$, a system cannot generate strings $s_1$ and $s_2$ simultaneously, whereas the way the system generates a string is the number of runs it can generate on that string. By Lemma 2, we have that the number of runs on string $s_1$ or $s_2$ is equal to the sum of the number of runs on $s_1$ and the number of runs on $s_2$, which is ${\left[{\mathit{R}}_{s_1}\right]}_{i,j}+{\left[{\mathit{R}}_{s_2}\right]}_{i,j}={\left[{\mathit{R}}_{s_1+s_2}\right]}_{i,j}$.

(2) Clearly, a system generates a string $s_1{s}_2$ in the order that first yields $s_1$ and then generates $s_2$. By Lemma 3, we have that the number of runs from state $q_j$ to $q_i$ on $s_1{s}_2$ is equal to the product of the number of runs from state $q_j$ to any state $q_k\in Q$ and the number of runs from that state $q_k$ to state $q_i$, which is ${\sum }_{1\le k\le N}{\left[{\mathit{R}}_{s_1}\right]}_{k,j}·{\left[{\mathit{R}}_{s_2}\right]}_{i,k}={\left[{\mathit{R}}_{s_1{s}_2}\right]}_{i,j}$. □

Remark 2.

Given any string $s\in E^{*}$, we have ${\mathit{R}}_s={\mathit{R}}_s·{\mathit{R}}_{\epsilon }={\mathit{R}}_{\epsilon }·{\mathit{R}}_s$, which also meets the definition of the concatenation of strings.

Based on the second part of the above proposition, we have the following corollary, which can be used to calculate the run matrix associated with a string $s\in E^{*}$ of length greater than zero.

Corollary 1.

The run matrix associated with a string $s=e_{\left(1\right)}{e}_{\left(2\right)}\cdots e_{\left(k\right)}$ ($k>0$) is

$${\mathit{R}}_s={\mathit{T}}_{e_{\left(k\right)}}{\mathit{T}}_{e_{(k-1)}}\cdots {\mathit{T}}_{e_{\left(2\right)}}{\mathit{T}}_{e_{\left(1\right)}}.$$

(2)

We can also extend the notion of run matrices to languages, i.e., given a language L, the run matrix ${\mathit{R}}_L$ associated with it is an $N\times N$ matrix whose typical entry ${\left[{\mathit{R}}_L\right]}_{i,j}$ is equal to the total number of runs on all strings in L from $q_j$ to $q_i$. It is not difficult to conclude that ${\mathit{R}}_L={\sum }_{s\in L}{\mathit{R}}_s$. Moreover, the extended run matrix has the following properties.

Proposition 4.

Given two finite languages $L_1$ and $L_2$ that have corresponding run matrices ${\mathit{R}}_{L_1}$ and ${\mathit{R}}_{L_2}$, respectively,

(1) 

In the case that $L_1$ and $L_2$ are disjoint, ${\mathit{R}}_{L_1\cup L_2}={\mathit{R}}_{L_1}+{\mathit{R}}_{L_2}$.

(2) 

${\mathit{R}}_{L_1·L_2}={\mathit{R}}_{L_2}·{\mathit{R}}_{L_1}$.

Proof. 

(1) As $L_1$ and $L_2$ are disjoint, the string in $L_1\cup L_2$ either belongs to $L_1$ or to $L_2$. Therefore, we have ${\mathit{R}}_{L_1\cup L_2}={\sum }_{s\in L_1}{\mathit{R}}_s+{\sum }_{s\in L_2}{\mathit{R}}_s={\mathit{R}}_{L_1}+{\mathit{R}}_{L_2}$.

(2) By $L_1{L}_2=\{s_1{s}_2\mid s_1\in L_1,s_2\in L_2\}$, and the definition of extended run matrices, we have ${\mathit{R}}_{L_1·L_2}={\sum }_{s_1\in L_1,s_2\in L_2}{\mathit{R}}_{s_2}·{\mathit{R}}_{s_1}=\left({\sum }_{s_2\in L_2}{\mathit{R}}_{s_2}\right)·\left({\sum }_{s_1\in L_1}{\mathit{R}}_{s_1}\right)={\mathit{R}}_{L_2}·{\mathit{R}}_{L_1}$, where the first equal sign is due to the second part of Proposition 3. □

Remark 3.

For any finite language $L\subseteq E^{*}$, we have ${\mathit{R}}_L={\mathit{R}}_{L\cap \mathcal{L}(G,Q)}$, as for any $s\in L\backslash \mathcal{L}(G,Q)$, we have ${\mathit{R}}_s=\mathit{O}$ by Remark 1, where $\mathit{O}$ is a null matrix.

Proposition 5.

Given a system $G=(Q,E,f,Q_0)$, define an N-dimensional column vector π such that ${\left[\mathit{\pi }\right]}_i=1$ if $q_i\in Q_0$ and ${\left[\mathit{\pi }\right]}_i=0$ otherwise. Then, ${[{\mathit{R}}_L·\mathit{\pi }]}_i$ is the total number of runs generated by system G on strings in language L, where the ending state of these runs is $q_i$.

Proof. 

It can be directly obtained from the definition of the multiplication of matrices and the meaning of run matrices. □

Based on the above discussions, we can use matrix operations to calculate the number of runs between different states on observations. It is not difficult to find that given an observation $\omega =o_{\left(1\right)}{o}_{\left(2\right)}\cdots o_{\left(l\right)}$, we have $\mathcal{S}\left(\omega \right)=E_{uo}^{*}\left\{o_{\left(1\right)}\right\}{E}_{uo}^{*}\left\{o_{\left(2\right)}\right\}{E}_{uo}^{*}\cdots E_{uo}^{*}\left\{o_{\left(l\right)}\right\}{E}_{uo}^{*}\cap \mathcal{L}\left(G\right)$. Based on Definition 5, we know that the cardinality of set ${\Phi }_q\left(\omega \right)$ is the total number of runs generated by the system on all strings in language $\mathcal{S}\left(\omega \right)$ that can reach state q, i.e., $\left|{\Phi }_{q_i}\left(\omega \right)\right|={[{\mathit{R}}_{\mathcal{S}\left(\omega \right)}·\mathit{\pi }]}_i$ ($1\le i\le N$). With Remark 3, once the run matrix corresponding to the language $E_{uo}^{*}\left\{o_{\left(1\right)}\right\}{E}_{uo}^{*}\left\{o_{\left(2\right)}\right\}{E}_{uo}^{*}$⋯$E_{uo}^{*}\left\{o_{\left(l\right)}\right\}{E}_{uo}^{*}$ is obtained, the cardinality of set ${\Phi }_q\left(\omega \right)$ for any $q\in Q$ is calculated.

Clearly, for any $e\in E_o$, we have ${\mathit{R}}_{\left\{e\right\}}={\mathit{R}}_e={\mathit{T}}_e$. The remaining problem is how to determine the run matrix associated with $E_{uo}^{*}$. Considering the set of unobservable events $E_{uo}$ as a language, we have ${\mathit{R}}_{E_{uo}}={\sum }_{e\in E_{uo}}{\mathit{R}}_e={\sum }_{e\in E_{uo}}{\mathit{T}}_e$. By the second part of Proposition 4, we have ${\mathit{R}}_{E_{uo}^i}={\mathit{R}}_{E_{uo}}^i$ for $i>0$. Note that by $E_{uo}^0=\left\{\epsilon \right\}$, there is ${\mathit{R}}_{E_{uo}^0}={\mathit{R}}_{\epsilon }=\mathit{I}$.

Theorem 1.

Given a system $G=(Q,E,f,Q_0)$ with no unobservable cycles, the run matrix ${\mathit{R}}_{E_{uo}^{*}}$ associated with $E_{uo}^{*}$ is ${(\mathit{I}-{\mathit{R}}_{E_{uo}})}^{-1}$.

Proof. 

Since $E_{uo}^{*}=\left\{\epsilon \right\}\cup E_{uo}\cup E_{uo}^2\cup \cdots$ and any two sets in $\{E_{uo}^i\mid i\in \mathbb{N}\}$ are disjoint, by Proposition 4, we have ${\mathit{R}}_{E_{uo}^{*}}={\sum }_{i\in \mathbb{N}}{\mathit{R}}_{E_{uo}^i}$. Suppose that there exists a run r of length N generated by G with $N+1$ states, where N is the number of states in G. By Lemma 4, we can find a duplicate state $q_d$ in r. This indicates the existence of an unobservable cycle in r, which violates the premise that there are no unobservable cycles in G. Therefore, the length of unobservable runs generated by G cannot be greater than N. Naturally, we have ${\mathit{R}}_{E_{uo}^i}=\mathit{O}$ for all $i>N$. From this, we obtain ${\mathit{R}}_{E_{uo}^{*}}={\sum }_{i=0}^N{\mathit{R}}_{E_{uo}^i}$.

$${\mathit{R}}_{E_{uo}^{*}}·(\mathit{I}-{\mathit{R}}_{E_{uo}})=(\mathit{I}+{\mathit{R}}_{E_{uo}}+{\mathit{R}}_{E_{uo}}^2+\cdots +{\mathit{R}}_{E_{uo}}^N)·(\mathit{I}-{\mathit{R}}_{E_{uo}})=\mathit{I}-{\mathit{R}}_{E_{uo}^{N+1}}=\mathit{I}$$

(3)

Furthermore, by (3), we conclude that the matrix $(\mathit{I}-{\mathit{R}}_{E_{uo}})$ is invertible and ${\mathit{R}}_{E_{uo}^{*}}={(\mathit{I}-{\mathit{R}}_{E_{uo}})}^{-1}$. □

Remark 4.

In the following, we will notate the run matrix associated with $E_{uo}^{*}$ as ${\mathit{R}}_{uo}$ for brevity of notation. If there are no unobservable events in the system G, then ${\mathit{R}}_{E_{uo}}=\mathit{O}$, leading to ${\mathit{R}}_{uo}=\mathit{I}$ without affecting the results below.

In light of the above discussion, it is natural to present Algorithm 1 for the online verification of worthy opacity. Lines 3 to 8 are the initialization of the marker variable $flag$ and the count vector $\mathit{\pi }$, where $flag$ is set to be $True$ to indicate that the system is worthy opaque, and the i-th entry of $\mathit{\pi }$ indicates the number of system-generated runs ending in state $q_i$, inferred by an intruder from the observation. Lines 9 to 23 are the intruder’s online judgment of worthy opacity, whereas lines 10 to 14 are calculations of the expected worth of the currently revealed information. Once the expected worth exceeds K, which means that the system is not worthy opaque, set the $flag$ to be $False$ and stop observing as shown in lines 15 to 18; otherwise, continue the observation as shown in lines 19 to 22. As regards the complexity of Algorithm 1, we note that the complexity of the recursive step k (observe the kth event) is $\mathcal{O}(k·N)$.

Example 8.

Consider the system $G_1$ in Example 1, where its state-worth function is shown in Example 4. Given an observation $\omega =e_1^2$, we verify online the $(E_o,\mathsf{\Delta },100)$-worthy opacity of ω using Algorithm 1. Initially, ω is set to be the empty string, i.e., $\omega =\epsilon$. By Algorithm 1, we have that the expected worth for this system is 50, which is less than 100, implying that the null observation ε is $(E_o,\mathsf{\Delta },100)$-WO. Similarly, after observing $e_1$, the value of $worth$ becomes $80<100$, so $e_1$ is also $(E_o,\mathsf{\Delta },100)$-WO. Continuing to run the algorithm, after observing $e_1$ again, we have $worth=100$, implying that $e_1^2$ is $(E_o,\mathsf{\Delta },100)$-WO.

Algorithm 1 Online verification of worthy opacity

Input:  A system $G=(Q,E,f,Q_0)$ with $E=E_o\dot{\cup }{E}_{uo}$, a state-worth function $\mathsf{\Delta }$, and a non-negative value K Output:  $(E_o,\mathsf{\Delta },K)$-WO of $\omega$ upon observing an event e 1: $flag\leftarrow True$, $\mathit{\pi }\leftarrow \mathbf{0}$ 2: for $i\leftarrow 1$ to N do 3:    if $q_i\in Q_0$ then 4:      ${\left[\mathit{\pi }\right]}_i\leftarrow 1$ 5:    end if 6: end for 7: while $flag$ do 8:    $\mathit{\pi }\leftarrow {\mathit{R}}_{uo}·\mathit{\pi }$, $worth\leftarrow 0$ 9:    ${\mathit{\pi }}_n\leftarrow \mathtt{norm}\left(\mathit{\pi }\right)$ 10:    for $i\leftarrow 1$ to N do 11:      $worth\leftarrow worth+\mathsf{\Delta }\left(q_i\right)·{\left[{\mathit{\pi }}_n\right]}_i$ 12:    end for 13:    if $worth>K$ then 14:      $flag\leftarrow False$ 15:    end if 16:    Output $flag$ 17:    if $flag$ then 18:      Wait until a new event e is observed 19:      $\mathit{\pi }\leftarrow {\mathit{T}}_e·\mathit{\pi }$ 20:    end if 21: end while

4.2. Run Status Recorder and 1-Cycle Returned

It is not difficult to find that for any observation $\omega$, there is ${\Phi }_q\left(\omega \right)=\varnothing$ if $q\notin \mathcal{C}\left(\omega \right)$, which leads to ${\alpha }_{\omega }\left(q\right)=0$ if $q\notin \mathcal{C}\left(\omega \right)$, and implies that we can narrow the computation from $\{{\alpha }_{\omega }\left(q\right)\mid q\in Q\}$ to $\{{\alpha }_{\omega }\left(q\right)\mid q\in \mathcal{C}\left(\omega \right)\}$. We call the set $\{{\alpha }_{\omega }\left(q\right)\mid q\in \mathcal{C}\left(\omega \right)\}$ the current-state probability distribution estimate associated with $\omega$, denoted by $\mathcal{A}\left(\omega \right)$. Note that the observer mentioned in Definition 3 represents, in a compact structure, all possible current state estimates during the evolution of a system. Inspired by this idea, it seems that we can also represent all current-state probability distribution estimates in a finite structure. Unfortunately, as the system evolves, there may be an infinite number of sets $\mathcal{A}\left(\omega \right)$, as the sets $\mathcal{A}\left(\omega \right)$ and $\mathcal{C}\left(\omega \right)$ do not correspond one-to-one.

By analyzing the evolution of a system, we find that if there is no cycle in its observer. Then, the observations generated by that system are finite, which means that the number of set $\mathcal{A}\left(\omega \right)$ is also finite. Thus, the verification of worthy opacity can be achieved by traversing all observations to determine whether (1) holds. In contrast, if there is a cycle in the observer of a system, then this system can generate an infinite number of observations.

Given a cycle $c_o$ of an observer, the system associated with that observer can generate an infinite number of observations of the form $\omega c_o^i$ ($i\in \mathbb{N}$), assuming that the observation when the observer first enters the cycle is $\omega$. If $\mathcal{A}\left(\omega \right)=\mathcal{A}\left(\omega c_o\right)$, we say that the cycle is 1-cycle returned (1-CR), and if all cycles in an observer of a system are 1-CR, then we say that this system is 1-CR. Fortunately, if a system G is 1-CR, then the current-state probability distribution estimate that can be generated by G is finite, i.e., the worthy opacity of system G is verifiable, as shown in Example 6.

Given a system G, we check whether G is 1-CR by Algorithm 2 and, if so, construct a run status recorder, which is an automaton that enumerates all possible current-state probability distribution estimates generated by system G (see Figure 4). The core idea of Algorithm 2 comes from Proposition 6.

Proposition 6.

Given two N-dimensional column vectors ${\mathit{\pi }}_1$ and ${\mathit{\pi }}_1$ that satisfy $\mathtt{norm}\left({\mathit{\pi }}_1\right)=\mathtt{norm}\left({\mathit{\pi }}_2\right)$, for any $N\times N$ matrix $\mathit{R}$, it holds that $\mathtt{norm}(\mathit{R}·{\mathit{\pi }}_1)=\mathtt{norm}(\mathit{R}·{\mathit{\pi }}_2)$.

Proof. 

Let $\mathtt{norm}\left({\mathit{\pi }}_1\right)=\mathtt{norm}\left({\mathit{\pi }}_2\right)=\mathit{\pi }$. We have ${\mathit{\pi }}_1=k_1\mathit{\pi }$ and ${\mathit{\pi }}_2=k_2\mathit{\pi }$, where $k_1$ and $k_2$ are 1-norms of ${\mathit{\pi }}_1$ and ${\mathit{\pi }}_2$, respectively. Hence, one obtains

$$\mathtt{norm}(\mathit{R}·{\mathit{\pi }}_1)=\frac{\mathit{R}·k_1\mathit{\pi }}{∥\mathit{R}·k_1\mathit{\pi }∥}=\frac{k_1\mathit{R}·\mathit{\pi }}{k_1∥\mathit{R}·\mathit{\pi }∥}=\frac{k_2\mathit{R}·\mathit{\pi }}{k_2∥\mathit{R}·\mathit{\pi }∥}=\frac{\mathit{R}·k_2\mathit{\pi }}{∥\mathit{R}·k_2\mathit{\pi }∥}=\mathtt{norm}(\mathit{R}·{\mathit{\pi }}_2).$$

This completes the proof. □

Algorithm 2 Construction of the run status recorder and and verification of the 1-CR of system G

Input:  A system $G=(Q,E,f,Q_0)$ with $E=E_o\dot{\cup }{E}_{uo}$ Output:  Run status recorder $G_r=(Y,E_o,f_r,y_0)$ 1: for $i\leftarrow 1$ to N do 2:    if $q_i\in Q_0$ then 3:      ${\left[\mathit{\pi }\right]}_i\leftarrow 1$ 4:    end if 5: end for 6: $\mathit{\pi }\leftarrow {\mathit{R}}_{uo}·\mathit{\pi }$ 7: $y_0\leftarrow (\mathit{\pi },\mathtt{norm}\left(\mathit{\pi }\right))$ 8: $Y\leftarrow \left\{y_0\right\},ns\leftarrow \left\{\mathtt{norm}\left(\mathit{\pi }\right)\right\}$ 9: $un\leftarrow \left\{y_0\right\}$ 10: while $un\ne \varnothing$ do 11:    Select a state $y\in un$ 12:    for all $e\in E_o$ do 13:      $\mathit{\pi }\leftarrow {\mathit{R}}_{uo}·{\mathit{T}}_e·y\left(1\right)$ 14:      if $\mathit{\pi }\ne \mathbf{0}$ and $\mathtt{norm}\left(\mathit{\pi }\right)\notin ns$ then 15:         if $\exists y^{\prime }\to y$ such that $\mathtt{eig}\left(y^{\prime }\left(1\right)\right)=\mathtt{eig}\left(\mathit{\pi }\right)$ then 16:           return NOT 1-CR 17:         end if 18:         $ns\leftarrow ns\cup \left\{\mathtt{norm}\right(\mathit{\pi }\left)\right\}$ 19:         $y_n\leftarrow (\mathit{\pi },\mathtt{norm}\left(\mathit{\pi }\right)),Y\leftarrow Y\cup \left\{y_n\right\}$ 20:         $un\leftarrow un\cup \left\{y_n\right\}$ 21:    else 22:      Select $y_n\in Y$ with $y_n\left(2\right)=\mathtt{norm}\left(\mathit{\pi }\right)$ 23:    end if 24:      $f_r(y,e)\leftarrow y_n$ 25:    end for 26:     $un\leftarrow un\backslash \left\{y\right\}$ 27: end while

Each state in the run status recorder $G_r$ is an ordered pair of two vectors, whose first component is the count vector mentioned in Algorithm 1, denoting the number of runs that reach each state after the system generates a certain observation. Its second component is the L1-normalization of the first vector. Proposition 6 shows that we can merge count vectors that have the same L1-normalization because we are only interested in the current-state probability distribution estimates, which is why we use the second component of the state to identify the different states.

Algorithm 2 works as follows: Lines 3 to 11 are the initialization of the key parameters of the algorithm, where set $ns$ includes all possible current-state probability distribution estimates generated by the input system and set $un$ contains the states generated by the algorithm for which subsequent states are not computed. Function $\mathtt{eig}:{\mathbb{N}}^N\to {\mathbb{N}}^N$ in line 16 of Algorithm 2 is defined as ${\left[\mathtt{eig}\left(\mathit{\pi }\right)\right]}_i=1$ if ${\left[\mathit{\pi }\right]}_i\ne 0$ otherwise ${\left[\mathtt{eig}\left(\mathit{\pi }\right)\right]}_i=0$, representing a current-state estimate of system G. Once the judgment condition in line 16 is satisfied, it means that the newly generated current-state probability distribution estimate, which different from some previously calculated current-state probability distribution estimate, corresponds to the same current-state estimate, i.e., this system is not 1-CR.

The construction of a run status recorder shows that the number of its states is related to the number of cycles in the observer of the input system G. The number of cycles in an observer of system G containing i different states is $\left(\genfrac{}{}{0pt}{}{2^N}{i}\right)(i-1)!$, where the observer is considered as the worst case. Then, these $\left(\genfrac{}{}{0pt}{}{2^N}{i}\right)(i-1)!$ cycles can produce $i·\left(\genfrac{}{}{0pt}{}{2^N}{i}\right)(i-1)!=\left(2^N\right)!/(2^N-i)!$ different states in $G_r$ in the worst case. Therefore, the complexity of Algorithm 2 is $\mathcal{O}(2^N!)$. Although the complexity of Algorithm 2 looks formidable, there are few systems that can reach the worst case that we analyze. If there is no cycle in the observer of a system, then the complexity of Algorithm 2 is reduced to $\mathcal{O}\left(2^N\right)$.

Theorem 2.

Given a system $G=(Q,E,f,Q_0)$ with state-worth function Δ, a set of observable events $E_o\subseteq E$, and a non-negative value $K\in {\mathbb{R}}_{\ge 0}$, if system G is 1-CR, then construct the run status recorder $G_r=(Y,E_o,f_r,y_0)$ as in Algorithm 2. System G is worthy opaque with respect to $E_o$, Δ and K if and only if for any states $y\in Y$, $\mathsf{\Delta }·y\left(2\right)\le K$ holds, where Δ is an N-dimensional row vector with ${\left[\mathsf{\Delta }\right]}_i=\mathsf{\Delta }\left(q_i\right)$.

Proof. 

(Sufficiency) By contrapositive, assume that there exists a state y in $G_r$ such that $\mathsf{\Delta }·y\left(2\right)>K$. Let $\omega$ be the observation that leads to y from $y_0$. By the construction of $G_r$, we have that, for the observation $\omega$, ${\sum }_{q\in Q}{\alpha }_{\omega }\left(q\right)·\mathsf{\Delta }\left(q\right)>K$ holds. By Definition 6, G is not worthy opaque with respect to $E_o$, $\mathsf{\Delta }$ and K.

(Necessity) Also by contrapositive, assume that G is not worthy opaque with respect to $E_o$, $\mathsf{\Delta }$ and K. By Definition 6, there exists an observation ${\omega }^{\prime }$ such that ${\sum }_{q\in Q}{\alpha }_{{\omega }^{\prime }}\left(q^{\prime }\right)·\mathsf{\Delta }\left(q\right)>K$. By the construction of $G_r$, we conclude that there is a state $y^{\prime }\in Y$ with $\mathsf{\Delta }·y\left(2\right)>K$. □

Example 9.

Consider a single-story smart building with five rooms marked with $R_1$, $R_2$, $R_3$, $R_4$, and $R_5$, as shown in Figure 5a. A bi-directional door exists between $R_1$ and $R_2$, $R_3$ and $R_4$, $R_3$ and $R_5$, $R_1$ and $R_5$, while $R_2$ to $R_4$ have a uni-directional door. And these five rooms are provided to three different departments according to $R_1$ and $R_2$, $R_3$ and $R_4$, and $R_5$. A smart vehicle provides different services to staff depending on the department, with sensors inside the vehicle that identify the current department. Five levels of confidential documents need to be stored in these five rooms, ranging in value from 1 to 5. Now, suppose that an intruder can read the sensor data of a smart vehicle; how does one allot the five rooms to store confidential documents such as to minimize the worth of information exposed by the vehicle?

The vehicle’s trajectory can be represented by the model shown in Figure 5b. The five states $q_1$ to $q_5$ correspond to the five rooms $R_1$ to $R_5$, respectively. Events $e_1$ to $e_3$ represent the sensor readings of the vehicle reaching each room, respectively. Since the intruder does not know the exact location of the vehicle but can obtain the sensor readings, the initial state of this model is $Q_0=Q=\{q_1,q_2,q_3,q_4,q_5\}$ and the observable event set is $E_o=E=\{e_1,e_2,e_3\}$. Now, running Algorithm 2 with system $G_3$ as input, we can obtain the corresponding run status recorder $G_{r,3}$ as shown in Figure 6.

By assumption, the state-worth function Δ of system $G_3$ is a one-to-one mapping from Q to $\{1,2,3,4,5\}$. Let Δ be an N-dimensional row vector with ${\left[\mathsf{\Delta }\right]}_i=\mathsf{\Delta }\left(q_i\right)$. Then, the problem of allotting the rooms where the confidential documents are to be stored is transformed into how to define the function Δ such that the maximum value in $\{\mathsf{\Delta }·y_i\left(2\right)\mid i=0,1,2,3,4,5,6\}$ is minimized. Based on states $y_4$, $y_5$, and $y_6$, we know that the two documents with the highest level of confidentiality can only be placed in rooms $R_1$ and $R_2$, respectively. Once this is done, it is not difficult to verify that $max\{\mathsf{\Delta }·y_i\left(2\right)\mid i=0,1,2,3,4,5,6\}=\mathsf{\Delta }·y_0\left(2\right)=3$, which means the system $G_3$ is $(E_0,\mathsf{\Delta },3)$-WO.

In plain words, we only need to place the documents with the highest and second-highest level of confidentiality in rooms $R_1$ and $R_2$, respectively; then, no matter how the sensor data of the vehicle is exposed, the worth of the information it reveals to the outside world will not exceed 3.

5. Conclusions

In this article, we introduce a notion of worthy opacity to quantify the worth of information released by a partially observed DES modeled with an automaton. We propose an online verification algorithm that considers an intruder who waits and observes the occurrence of observable events and determines whether the observation is worthy opaque. We also present a 1-CR system to verify the worthy opacity offline.

We believe that there are multiple interesting directions for future work related to the notion of worthy opacity. An attractive direction is to synthesize a supervisor that enforces worthy opacity when the verification result is negative. Also, we would like to apply the notion of worthy opacity to more complex, realistic environments.