Language-Based Opacity Verification in Partially Observed Petri Nets through Linear Constraints

Abstract

Information security is an important area of concern in modern computer-integrated systems. It involves implementing preventative measures to protect confidential data from potential vulnerabilities, such as unauthorized access, secret disclosure, modification, or destruction. Considering such threats, we investigate a particular confidentiality property called opacity, which specifies a system’s ability to cover its ‘secret’ data from being interfered with by outside observers, termed as intruders. This paper discusses language-based opacity formulation and verification in the context of discrete event systems represented by partially observed Petri nets. In this context, we identify two opacity properties, called consistency and non-secrecy; then, we exploit the mathematical characterization of a net system, to separately check each property, by specifying two feasibility problems. The proposed method is carried out for two distinct settings of a system. The first setting is centralized, where an intruder is granted complete information about the system structure but a partial observation of its behavior. The second setting is decentralized, where a group of intruders cooperates to reveal the secret language, by using a coordinator. Finally, experimental findings are given, to demonstrate the proficiency of the proposed approach.

1. Introduction

The growing number of modern cyber-physical systems involving critical information, such as defense, health care, banking, and communication systems, emphasizes the need to establish measures to ensure their security against hostile actions. These systems are particularly subject to unauthorized access, because the risk of information leakage to unauthorized users may reveal sensitive details about their behavior.

Both the industry and the research communities have recently stressed the importance of security properties. These properties are primarily categorized into three groups: confidentiality, availability, and integrity, which guide policies for information security within systems and organizations. Motivated by security concerns about discrete event systems (DESs), our study concentrates on a specific confidentiality property, called opacity. This property describes the capability of preventing a hostile observer, referred to as an intruder, from inferring whether or not a system’s secret behavior has occurred. Numerous aspects of opacity have recently been investigated in the computer security community.

Due to their competency for system modeling, Petri nets under partial observations have been widely used in cyber-physical systems. In the area of DESs, there has been a deluge of studies on fault diagnosis, deadlock control [1], and supervisory control [2] based on Petri nets. One significant feature of a Petri net (PN) is its mathematical formalism that allows the use of integer linear programming (ILP), which can alleviate the state explosion problem, to some extent. For this reason, we use a Petri net as a modeling framework in this study.

Opacity is considered as a general information flow property that covers a wide range of applications in DESs. Bryans et al. [3] proved that certain information flow properties, such as anonymity and non-interference [4] problems, can be converted into opacity, by using appropriate observation mappings. In addition, Lin et al. [5] showed that observability, detectability, and diagnosability [6] can be conceived as opacity problems.

Opacity in DESs is categorized into two main groups, based on the secret’s representation: state-based opacity [7], where a secret is specified as a subset of the state space, and language-based opacity (LBO) [8], where a secret is specified as a subset of firable transition sequences.

This study considers the language-based opacity verification problem in DESs represented by partially observed Petri nets (POPNs), where a secret is defined as a finite sub-language of a PN system, and an intruder is allowed to possess complete knowledge of the system’s structure, but can only identify the firing of visible transitions and (or) the tokens variation in visible places. Language-based opacity was initially introduced to DESs modeled with FSA in [5,9], and it was extended recently to bounded labeled Petri net systems (LPNs) in [10]. In [5], Lin et al. specified two classes of opacity, called strong and weak opacity. A strongly (resp. weakly) opaque language is a language where strings from a different language camouflage all (resp. some) of its strings. Specifically, given a regular system language and a state-based projection information mapping, the authors in [5] proposed algorithms with exponential complexity, to verify both weak and strong opacity. In the current study, language-based opacity is attributed to strong opacity. In [10], Tong et al. studied a special case of LBO, called strict language opacity, in a bounded PN system. This work was based on the assumption that a secret is defined as a subset of firable sequences of transitions and an intruder who is interested in observable transitions only. To check the strict language opacity property, Tong et al. built a finite automaton, called a verifier, which synchronized the PN system and the secret language, based on observable transitions. This approach was time-consuming, because it required off-line construction of the verifier, which suffered an exponential space complexity. In [11], Cong et al. also established a necessary and sufficient condition for current state opacity (CSO) verification in LPN through integer linear programming. However, their method cannot be directly used for LBO verification, unless we convert the CSO problem into an LBO problem, using the transformation method given in [12]. Furthermore, the research in [11] only considered secret markings defined by a set of generalized mutual exclusion constraints (GMECs), which restricts the scope of secret selection.

Another interesting work is found in [13], which investigated the verification problem of LBO in LPNs, where the unobservable subnet was considered to be acyclic, and the secret was specified across sequences of events rather than transitions. The study in [13] was closely related to this particular research, in which the authors solved an integer linear programming problem (ILPP), to establish a condition that was both sufficient and necessary for LBO verification. The technique proposed in this study is more general, as it applies to a greater range of PN systems under partial observations (i.e., PNs equipped with place and transition sensors).

Nowadays, intruders tend to be highly skilled and intelligent. They are often part of an organized group providing illegal specialized services, such as credit card fraud, theft of intellectual property, or counterfeiting documents. This paper investigates the LBO verification problem in a decentralized setting, where local intruders collaborate by using a coordinator. Each local intruder has complete information about the net structure but only partial information about its evolution.

Decentralized opacity can be reduced to many security properties, such as decentralized anonymity, secrecy, and non-interference. Specifically, consider a multi-user system that allows many users to share the resources of a single computer. In our framework, these users can be viewed as intruders who should not determine whether or not the decentralized security property is met. Furthermore, many properties employed in discrete event systems for supervisory control can be restated as a particular instance of decentralized opacity. Paoli et al. [14] showed that co-opacity is an extension of co-observability [15] used for supervisory control [16], and that it can be used to check the existence of a group of decentralized local supervisors (intruders in our framework, with or without a coordinator) that control a system. Tripakis and Rudie [17] developed a decidable condition called “at least one can tell”, which ensures that decentralized agents can make correct decisions about the behavior of a system. This condition is relevant to the decentralized opacity problem, because it provides a way to verify whether or not a decentralized system is opaque.

This research aims to compose the LBO verification problem in the context of a DES represented by a POPN, taking into account observations from place and transition sensors. Then, based on the proposed formulation, new approaches to verifying LBO are set up. In light of the preceding, the findings of this study contribute the following to the existing literature:

• We define the concept of secret observation sequences, by considering a case where a secret involves numerous transition sequences yielding the same observation. This concept decreases the effort required to check language opacity in a POPN, by avoiding redundant explorations.
• We identify two language-based opacity properties, called consistency and non-secrecy properties; we separately check each property; then, we provide necessary and sufficient conditions to check language-based opacity, by defining and solving an ILPP.
• Finally, we extend the above results from a centralized framework to a decentralized framework with a coordinator, where more than one intruder observes the system.

The following is a breakdown of the paper’s structure. Section 2 provides an overview of Petri nets and partially observed Petri nets. The theory underlying the partition of unobservable transitions, as well as the concept of discernible transitions, is presented in Section 3. The LBO verification problem is formulated in a POPN system in Section 4. An ILP problem is established in Section 5, to solve the LBO verification problem. In Section 7, we discuss opacity in a decentralized case, where a group of local intruders unites to reveal a secret language via a coordinator. To demonstrate the proposed method, an example is given in Section 6. Finally, Section 8 brings the study to a close and points the way forward for further research.

2. Preliminaries

2.1. Petri Nets

A Petri net structure is a weighted bipartite graph $N=(P,T,Pre,Post)$, where $P=\{p_1,p_2,\dots ,p_m\}$ is a set of m places and $T=\{t_1,t_2,\cdots ,t_n\}$ is a set of n transitions with $P\cup T\ne \varnothing$ and $P\cap T=\varnothing$. $Pre:P\times T\to \mathbb{N}$ and $Post:P\times T\to \mathbb{N}$ ($\mathbb{N}$ denotes the set of non-negative integer numbers) are the pre- and post-incidence functions designating arcs from places to transitions and from transitions to places, respectively, in a net, and they are represented as matrices in ${\mathbb{N}}^{m\times n}$. The incidence matrix of a PN is defined by $C=Post-Pre$.

A marking is a mapping $M:P\to \mathbb{N}$ that attributes to each place a non-negative integer number of tokens. A PN system with initial marking $M_0$ is denoted by a couple $(N,M_0)$. A transition $t_i$ is enabled at a marking M, denoted by $M[t_i\rangle$, if $M\ge Pre(·,i)$, where $Pre(·,i)$ is the ith column of matrix $Pre$. Firing an enabled transition yields a marking $M^{\prime }$ with

$$\begin{array}{c}\hfill M^{\prime }=M+C(·,t),\end{array}$$

(1)

where $C(·,t)$ is a column vector that denotes the token change generated by firing t. Given a transition sequence $\sigma \in T^{*}$, $\left|\sigma \right|$ denotes the length of $\sigma$. Let $\pi :T^{*}\to {\mathbb{N}}^n$ be a function that allocates a Parikh vector $y\in {\mathbb{N}}^n$ to a transition sequence $\sigma \in T^{*}$, called the firing vector of $\sigma$. The notations $M[\sigma \rangle$ and $M[\sigma \rangle M^{\prime }$ indicate, respectively, that $\sigma$ is enabled at M and the firing of $\sigma$ at M yields $M^{\prime }$, following the equation:

$$\begin{array}{c}\hfill M^{\prime }=M+C·\pi (\sigma ).\end{array}$$

(2)

Equation (2) is called the state equation of $(N,M_0)$. We denote by $L(N,M_0)=\{\sigma \in T^{*}|M_0[\sigma \rangle \}$ the set of all firable transition sequences in $(N,M_0)$, and by $R(N,M_0)$ the reachability set of $(N,M_0)$. A PN is said to be acyclic if there is no directed circuit and bounded if there exists a positive constant $k\in \mathbb{N}$, such that, for all $M\in R(N,M_0)$ and $p\in P$, $M(p)\le k$, where $M(p)$ is the tokens number in place p.

2.2. Partially Observed Petri Nets

A partially observed Petri net is a PN system equipped with place sensors that display the number of tokens in some places, known as observable places, and (or) transition sensors that display the labels of observable transitions, when fired. In this sense, POPNs can be seen as a generalization of LPNs, since any LPN can be represented as a POPN. However, not all POPNs can be represented as LPNs. This is because POPNs allow for the presence of place sensors, which LPNs do not.

The set of observable places is denoted by $P_o\subseteq P$. We re-index observable places in $P_o$ from 1 to $m_o$, such that $P_o=\{p_{o_1},p_{o_2},\dots ,p_{o_{m_o}}\}$ with $o_i\in \{1,2,\dots ,m\}$ and $p_{o_i}\in P$ for $i\in \{1,2,\dots ,m_o\}$. A partially observed Petri net is a quintuple-tuple $Q=(N,M_0,E,V,\delta )$, where $(N,M_0)$ is a PN system with m places and n transitions, E is an alphabet (a set of labels), and $V=(v_{ij})\in {\{0,1\}}^{m_o\times m}$ is a place sensor configuration matrix, where $v_{ij}=1$ if $j=o_i$ and $v_{ij}=0$, otherwise. A labeling function, $\delta :T\to E\cup \left\{\epsilon \right\}$, represents the transition sensor configuration, which allocates a label from E or the empty string $\epsilon$ to a transition $t\in T$. Based on these allocations, we divide the set of transitions T into two disjoint sets $T_o$ and $T_u$, satisfying $T=T_o\cup T_u$ and $T_o\cap T_u=\varnothing$, where $T_o=\{t\in T|\delta (t)\in E\}$ is the set of observable transitions and $T_u=\{t\in T|\delta (t)=\epsilon \}$ is the set of unobservable transitions. Thus, a label $\delta (t)$ is displayed only when we fire a transition $t\in T_o$. We denote by $\widehat{M}=V·M$ the marking measurement of M using a place sensor configuration matrix V. Arguably, matrix V characterizes a marking M projection on $P_o$.

Definition 1. 

Let $(N,M_0)$ be a PN system with $N=(P,T,Pre,Post)$. An evolution of N starting from $M_0$ is denoted as a transition-marking sequence.

$$\begin{array}{c}\hfill M_0{t}_1{M}_1{t}_2{M}_2\dots t_h{M}_h,\end{array}$$

satisfying $M_0[t_1\rangle M_1[t_2\rangle M_2\dots [t_h\rangle M_h$, where $t_i\in T$, $M_i\in R(N,M_0)$ for $i\in \{1,\dots ,h\},h\ge 1$.

Definition 2. 

Given a POPN $Q=(N,M_0,E,V,\delta )$, the collected measure associated with $M[t\rangle M^{\prime }$ is given as follows:

$$\begin{array}{c}\hfill \rho (M,t)=\left\{\begin{array}{cc}{\epsilon }_p,\hfill & \mathit{if}(\widehat{M}={\widehat{M}}^{\prime })\wedge (\delta (t)=\epsilon )\hfill \\ \widehat{M}\delta (t){\widehat{M}}^{\prime },\hfill & \mathit{otherwise},\hfill \end{array}\right.\end{array}$$

where $\widehat{M}=V·M$, ${\widehat{M}}^{\prime }=V·M^{\prime }$ and ${\epsilon }_p$ denotes an empty observation.

We denote by $\rho (M,\sigma )$ the extension of the operation ρ to transition sequences. Specifically, let $M{t}_1{M}_1{t}_2{M}_2\dots M_{h-1}{t}_h{M}_h$ be the evolution produced by firing $\sigma =t_1{t}_2\dots t_h\in T^{*}$ at M. We define the associated measurement sequence by concatenating the successive collected measures, as seen below:

$$\begin{array}{cc}\hfill \rho (M,\sigma )& =\rho (M,t_1)\rho (M_1,t_2)\dots \rho (M_{h-1},t_h)\hfill \\ \hfill & ={\widehat{M}}_{}{e}_1{\widehat{M}}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho},\hfill \end{array}$$

where $e_i\in E\cup \left\{\epsilon \right\}$ and $ho\le h$. Given a measurement sequence ${\widehat{M}}_0{e}_1\dots {\widehat{M}}_i{\widehat{M}}_i\dots e_{ho}{\widehat{M}}_{ho}$, $1\le i\le ho-1$, the operation Λ fuses each two adjacent ${\widehat{M}}_i$ as follows:

$$\Lambda ({\widehat{M}}_0{e}_1\dots {\widehat{M}}_i{\widehat{M}}_i\dots e_{ho}{\widehat{M}}_{ho})={\widehat{M}}_0{e}_1\dots {\widehat{M}}_i\dots e_{ho}{\widehat{M}}_{ho}.$$

Definition 3. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN, M be a marking from $R(N,M_0)$, and $\sigma =t_1{t}_2\dots t_h\in T^{*}$ be a transition sequence, such that $M[\sigma \rangle$. The observation sequence generated when σ fires at M is

$$\begin{array}{cc}\hfill w(M,\sigma )& =\Lambda (\rho (M,\sigma ))\hfill \\ \hfill & =\Lambda ({\widehat{M}}_{}{e}_1{\widehat{M}}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho})\hfill \\ \hfill & ={\widehat{M}}_{}{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho}.\hfill \end{array}$$

Marking measurements are displayed by sensors whenever observable events fire or when token variations occur in observable places. After obtaining $\rho (M,\sigma )$, each two adjacent measures ${\widehat{M}}_i{\widehat{M}}_i$ are merged into one measure, using the operation $\Lambda$. For simplification purposes, if no confusion is caused, we use the symbol w to designate an observation sequence in a POPN.

Example 1. 

Consider a POPN in Figure 1 with $M_0={[100000]}^T$. The place sensor configuration is derived from $P_o=\{p_1,p_5\}$ as follows:

$$V{=}_{p_{o_2}}^{p_{o_1}}\left(\begin{array}{cccccc}{p}_1& p_2& p_3& p_4& p_5& p_6\\ 1& 0& 0& 0& 0& 0\\ 0& 0& 0& 0& 1& 0\end{array}\right).$$

We have $T_o=\{t_1,t_4\}$ and $T_u=\{t_2,t_3,t_5\}$. Given $E=\{a,b\}$, we define the event sensor configuration using the labeling function δ as $\delta (t_1)=a$, $\delta (t_4)=b$, and $\delta (t_2)=\delta (t_3)=\delta (t_5)=\epsilon$. Let $\sigma =t_1{t}_3{t}_4$ be a transition sequence that is enabled at $M_0$. By Definition 1, ${[100000]}^T{t}_1{[011010]}^T{t}_3{[010011]}^T{t}_4{[000111]}^T$ is the evolution generated by firing σ at $M_0$. We have $\rho ({[011010]}^T,t_3)={\epsilon }_p$; by Definition 3, the associated observation sequence is $\Lambda (\rho (M_0,\sigma ))={[10]}^{T}a{[01]}^{T}b{[01]}^T$.

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and M be a marking from $R(N,M_0)$. We define by

$$\begin{array}{c}\hfill \mathcal{O}(Q,M)=\left\{w\right|\exists \sigma \in T^{*},M[\sigma \rangle ,\Lambda (\rho (M,\sigma ))=w\}\end{array}$$

the set of feasible observation sequences generated by Q from M, and by

$$\begin{array}{c}\hfill \mathcal{S}(w)=\{\sigma \in T^{*}|M_0[\sigma \rangle ,\Lambda (\rho (M_0,\sigma ))=w\}\end{array}$$

the set of transition sequences consistent with w.

3. Quasi-Unobservable and Discernible Transitions

Let Q be a POPN with a sensor configuration $(V,\delta )$ and $C_o\in {\mathbb{N}}^{m_o\times n}$ be the restriction of C to $P_o$. Based on $C_o$, the set of unobservable transitions $T_u$ can be partitioned into two disjoint sets ${\tilde{T}}_q$ and ${\tilde{T}}_u$, such that $T_u={\tilde{T}}_q\cup {\tilde{T}}_u$ and ${\tilde{T}}_q\cap {\tilde{T}}_u=\varnothing$, where ${\tilde{T}}_q=\{t\in T_u|C_o(·,t)\ne {\overrightarrow{\mathbf{0}}}_{m_o}$ (${\overrightarrow{\mathbf{0}}}_{m_o}$ is an $m_o$-dimensional column vector with all entries being 0)} is a set of quasi-observable transitions and ${\tilde{T}}_u=\{t\in T_u|C_o(·,t)={\overrightarrow{\mathbf{0}}}_{m_o}\}$ is a set of truly unobservable transitions. We define $T_d=T_o\cup {\tilde{T}}_q$ as the set of discernible transitions. For $e\in E\cup \left\{\epsilon \right\}$, $T(e)=\{t\in T|\delta (t)=e\}$ and $T_d(e)=\{t\in T_d|\delta (t)=e\}$, respectively, represent the subsets of transitions in T and $T_d$, having the same label, e. We denote by ${\Gamma }_e=\left\{{\overrightarrow{v}}_t\right|{\overrightarrow{v}}_t=C_o(·,t),t\in T(e)\}$ the set of column vectors in matrix $C_o$ associated with transitions in $T(e)$.

Example 2. 

Consider the POPN with the sensor configuration $(V,\delta )$ specified in Example 1. Matrix $C_o$ is given as follows:

$$C_o{=}_{p_5}^{p_1}\left[\begin{array}{ccccc}{t}_1(a)& t_2(\epsilon )& t_3(\epsilon )& t_4(b)& t_5(\epsilon )\\ -1& 0& 0& 0& 1\\ 0& 0& 0& 0& -1\end{array}\right].$$

It is evident that ${\tilde{T}}_u=\{t_2,t_3\}$, ${\tilde{T}}_q=\left\{t_5\right\}$, and $T_d=\{t_1,t_4,t_5\}$.

Definition 4. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and ${\tilde{T}}_u$ be the set of its truly unobservable transitions. A truly unobservable subnet of Q is defined as $\tilde{Q}=(\tilde{N},E,M_0,V,\delta )$, where $\tilde{N}=(P,{\tilde{T}}_u,{\widetilde{Pre}}_u,{\widetilde{Post}}_u)$, with ${\widetilde{Pre}}_u$ and ${\widetilde{Post}}_u$ being, respectively, the restrictions of $Pre$ and $Post$ on ${\tilde{T}}_u$. A discernible subnet of Q is defined as $Q_d=(N_d,M_0,E,V,\delta )$, where $N_d=(P,T_d,Pr{e}_d,Pos{t}_d)$, with $Pr{e}_d$ and $Pos{t}_d$ being, respectively, the restrictions of $Pre$ and $Post$ on $T_d$. ${\tilde{C}}_u$ and $C_d$, respectively, denote the incidence matrices of $\tilde{Q}$ and $Q_d$. Let $|{\tilde{T}}_u|={\tilde{n}}_u$ and $|T_d|=n_d$.

4. Language-Based Opacity

We assume that an intruder is only interested in a limited number of secret sequences, i.e., the secret is a finite sub-language of the net system.

Definition 5. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a finite secret language. Q is said to be language-opaque, with regard to $L_s$, if, for all $\sigma \in L_s$, there exists a sequence ${\sigma }^{\prime }\in L(N,M_0)\setminus L_s$, such that $\Lambda (\rho (M_0,\sigma ))=\Lambda (\rho (M_0,{\sigma }^{\prime }))$.

Definition 6. 

Given a POPN $Q=(N,M_0,E,V,\delta )$ and a finite secret language $L_s\subseteq L(N,M_0)$, the set of secret observation sequences associated with $L_s$ is defined as

$$\begin{array}{c}\hfill \mathcal{O}(L_s)=\left\{w\right|\exists \sigma \in L_s,\Lambda (\rho (M_0,\sigma ))=w\}.\end{array}$$

Let $w\in \mathcal{O}(L_s)$ be a secret observation sequence. The set of secret transition sequences consistent with w is given by

$$\begin{array}{c}\hfill {\mathcal{L}}_s(w)=\{\sigma \in L_s|M_0[\sigma \rangle ,\Lambda (\rho (M_0,\sigma ))=w\}.\end{array}$$

Note that each $w\in \mathcal{O}(L_s)$ can be associated with at least one transition sequence from $L_s$, i.e., $|{\mathcal{L}}_s(w)|\ge 1$. Knowing that $L_s$ is finite, then $\mathcal{O}(L_s)$ is also finite, with $|\mathcal{O}(L_s)|\le |L_s|$.

Now we reformulate the definition of LBO in a POPN, by exploiting the concept of secret observation sequences.

Definition 7. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a finite secret language. An observation sequence $w\in \mathcal{O}(L_s)$ is language-opaque, with regard to $L_s$, if and only if, at least, there is a sequence $\sigma \in L(N,M_0)\setminus L_s$, such that $\Lambda (\rho (M_0,\sigma ))=w$, i.e., $\mathcal{S}(w)⊈L_s$ holds.

Based on Definition 7, a POPN system is language-opaque, with regard to a secret language $L_s$, if for any $w\in \mathcal{O}(L_s)$ there exists a transition sequence $\sigma$ satisfying the following two properties:

• Consistency property: $\sigma \in \mathcal{S}(w)$;
• Non-secrecy property: $\sigma \notin L_s$.

Proposition 1. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. Q is language-opaque, with regard to $L_s$, if and only if, for any $w\in \mathcal{O}(L_s)$, w is language-opaque, with regard to $L_s$.

Proof. 

(If) Suppose that for any $w\in \mathcal{O}(L_s)$, w is LBO, with respect to $L_s$. Thus, for any $w\in \mathcal{O}(L_s)$ (i.e., $\sigma \in L_s$), there is at least a sequence ${\sigma }^{\prime }\in L(N,M_0)\setminus L_s$, such that $\Lambda (\rho (M_0,{\sigma }^{\prime }))=\Lambda (\rho (M_0,\sigma ))=w$. Based on Definition 5, Q is language-opaque, with regard to $L_s$.

(Only if) By contradiction, assume that Q is language-opaque, with respect to $L_s$, and that there exists an observation sequence $w\in \mathcal{O}(L_s)$ such that w is not language-opaque, with regard to $L_s$, i.e., $\mathcal{S}(w)\subseteq L_s$. In other words, for $\sigma \in \mathcal{S}(w)\subseteq L_s$, there does not exist ${\sigma }^{\prime }\in L(N,M_0)\setminus L_s$, such that $\Lambda (\rho (M_0,{\sigma }^{\prime }))=\Lambda (\rho (M_0,\sigma ))=w$. Thus, following Definition 5, Q is not LBO, which opposes the assumption. □

If a secret observation sequence w has several consistent transition sequences from $L_s$, i.e., $|{\mathcal{L}}_s(w)|>1$, it is more efficient to verify the opacity of w instead of investigating LBO separately for each $\sigma \in {\mathcal{L}}_s(w)$. Using this proposition, we put our focus on a portion of the reachability space that allows checking the secret language occurrence $\mathcal{O}(L_s)$, rather than checking the entire PN system language.

Example 3. 

Consider the POPN in Figure 1. Let $L_s=\{t_1{t}_3{t}_4,t_1{t}_3{t}_2{t}_5,t_1{t}_2{t}_3{t}_5\}$ be a secret language. Its associated secret observation sequences are given by $\mathcal{O}(L_s)=\{w_1,w_2\}$, where $w_1={[10]}^{T}a{[01]}^{T}b{[01]}^T$, $w_2={[10]}^{T}a{[01]}^T{[10]}^T$, ${\mathcal{L}}_s(w_1)=\left\{t_1{t}_3{t}_4\right\}$, and ${\mathcal{L}}_s(w_2)=\{t_1{t}_3{t}_2{t}_5,t_1{t}_2{t}_3{t}_5\}$. We have $\mathcal{S}(w_1)=\{t_1{t}_3{t}_4,t_1{t}_4{t}_3\}$ and $\mathcal{S}(w_2)=\{t_1{t}_2{t}_3{t}_5,t_1{t}_3{t}_2{t}_5\}$. We observe that $\mathcal{S}(w_1)⊈L_s$, implying that $w_1$ is LBO, with respect to $L_s$. However, we can see that $\mathcal{S}(w_2)\subseteq L_s$. Hence, based on Definition 7, $w_2$ is not LBO, which, based on Proposition 1, implies the non-language opacity of Q.

5. Mathematical Characterization of LBO

In this section, we suggest a linear algebraic characterization, to check LBO in a POPN Q. The following assumption supports this characterization: The truly unobservable subnet $\tilde{Q}$ and the discernible subnet $Q_d$ are acyclic.

Unfortunately, the majority of studies dealing with the opacity problem in PN systems [10,11,13], including the proposed approach, have a limitation, due to the assumption that the unobservable (observable) part of the Petri net is structurally acyclic, which is a strong requirement that limits their application to more general systems. This assumption ensures that the state equation is necessary and sufficient to capture the set of reachable markings by firing unobservable transitions. In this case, the mathematical characterization of a PN system using the state equation becomes a double-edge sword that reduces the exhaustive computation load on the one hand, but affects negatively the system generality on the other hand.

As far as we know, the only research that addresses the verification of language-based opacity that does not make the assumption of the unobservable subnet being acyclic is our earlier study, which we introduced in [18], where a verification algorithm employing a depth-first search approach verifies the presence of a non-secret transition sequence that is consistent with a secret observation sequence.

5.1. Consistency Assurance

With an observation sequence $w\in \mathcal{O}(Q,M_0)$ being observed, an intruder with full knowledge of the system structure tries to establish an estimation of the event sequences consistent with w. In the following proposition, we prove that each $\sigma \in \mathcal{S}(w)$ can be represented by a linear system.

Proposition 2. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $w={\widehat{M}}_0{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho}\in \mathcal{O}(Q,M_0)$ be an observation sequence. A transition sequence ${\sigma }^{\prime }$ is consistent with w if ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }$ and its firing vectors ${\overrightarrow{\sigma }}_{u_1}^{\prime },{\overrightarrow{\sigma }}_{u_2}^{\prime },\cdots ,{\overrightarrow{\sigma }}_{u_{ho+1}}^{\prime },{\overrightarrow{\sigma }}_{e_1}^{\prime },{\overrightarrow{\sigma }}_{e_2}^{\prime },\dots ,{\overrightarrow{\sigma }}_{e_{ho}}^{\prime }$ satisfy the following constraint set $\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)=$

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}{M}_0+{\tilde{C}}_u{\displaystyle \sum _{i=1}^{ho+1}}{\overrightarrow{\sigma }}_{u_i}^{\prime }+C_d{\displaystyle \sum _{j=1}^{ho}}{\overrightarrow{\sigma }}_{e_j}^{\prime }\ge \overrightarrow{\mathbf{0}}\hfill & (a)\hfill \\ \left.\begin{array}{c}{M}_0+{\tilde{C}}_u{\displaystyle \sum _{i=1}^l}{\overrightarrow{\sigma }}_{u_i}^{\prime }+C_d{\displaystyle \sum _{j=1}^{l-1}}{\overrightarrow{\sigma }}_{e_j}^{\prime }\ge Pr{e}_d·{\overrightarrow{\sigma }}_{e_l}^{\prime }\hfill \\ l\in \{1,\dots ,ho\}\hfill \end{array}\right\}\hfill & (b)\hfill \\ \left.\begin{array}{c}V·{\tilde{C}}_u·{\overrightarrow{\sigma }}_{u_i}^{\prime }=\overrightarrow{\mathbf{0}}\hfill \\ V·C_d·{\overrightarrow{\sigma }}_{ej}^{\prime }={\widehat{M}}_j-{\widehat{M}}_{(j-1)}\hfill \end{array}\right\}\hfill & (c)\hfill \\ \left.\begin{array}{c}{\displaystyle \sum _{t\in T_d(e_j)}}{\overrightarrow{\sigma }}_{e_j}^{\prime }(t)=1\hfill \\ {\displaystyle \sum _{t\notin T_d(e_j)}}{\overrightarrow{\sigma }}_{e_j}^{\prime }(t)=0\hfill \end{array}\right\}\hfill & (d)\hfill \\ \left.\begin{array}{c}{\overrightarrow{\sigma }}_{u_i}^{\prime }\in {\mathbb{N}}^{{\tilde{n}}_u},i\in \{1,\dots ,ho+1\}\hfill \\ {\overrightarrow{\sigma }}_{e_j}^{\prime }\in {\mathbb{N}}^{n_d},j\in \{1,\dots ,ho\}\hfill \end{array}\right\}\hfill & (e),\hfill \end{array}\right.\end{array}$$

(3)

where

• $|{\sigma }_{u_i}^{\prime }|\ge 0$, $i\in \{1,\dots ,ho+1\}$;
• $|{\sigma }_{e_j}^{\prime }|=1$, $j\in \{1,\dots ,ho\}$;
• Constraints (3.a) represent the state equation;
• Constraints (3.b) represent the enabling condition of discernible transitions;
• Constraints (3.c) represent the token variation generated by firing ${\sigma }_{u_i}^{\prime }$ and ${\sigma }_{e_j}^{\prime }$;
• Constraints (3.d) define a mutual exclusion condition, to prevent firing more than one discernible transition.

Proof. 

(Only if) Suppose that ${\sigma }^{\prime }$ is consistent with w, then ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }$, where ${\sigma }_{e_j}^{\prime }\in T_d(e_j)$ with $|{\sigma }_{e_j}^{\prime }|=1$, $j\in \{1,\dots ,ho\}$, and ${\sigma }_{u_i}^{\prime }\in {\tilde{T}}_u^{*}$, $i\in \{1,\dots ,ho+1\}$. Evidently, the associated firing vectors satisfy Constraints (3.a), (3.d) and (3.e).

When fired at $M_0$, ${\sigma }^{\prime }$ generates a trajectory:

$$\begin{array}{c}\hfill M_0[{\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }\rangle M_1\dots M_{ho-1}[{\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }\rangle M_{ho}[{\sigma }_{u_{ho+1}}^{\prime }\rangle M_{ho+1}.\end{array}$$

If a discernible transition fires ${\sigma }_{e_j}^{\prime }$, we have $\rho (M_{i-1}$, ${\sigma }_{u_i}^{\prime }{\sigma }_{e_j}^{\prime })={\widehat{M}}_{i-1}{e}_j{\widehat{M}}_i$. The firing of ${\overrightarrow{\sigma }}_{u_i}^{\prime }$ at $M_{i-1}$ enables ${\overrightarrow{\sigma }}_{e_j}^{\prime }$ but does not produce any token variations in observable places (i.e., $V·C_u·{\overrightarrow{\sigma }}_{u_i}^{\prime }=\overrightarrow{\mathbf{0}}$), while the firing of ${\overrightarrow{\sigma }}_{e_j}^{\prime }$ generates a token variation given by ${\widehat{M}}_i-{\widehat{M}}_{(i-1)}$. Therefore, the enabling Constraints (3.b) and the token variation Constraints (3.c) hold.

(If) Assume that there exists ${\sigma }^{\prime }$, such that ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }$, satisfying the Constraints Set (3). By Constraints (3.a) and (3.b), ${\sigma }^{\prime }$ is enabled at $M_0$ and generates the following trajectory when fired at $M_0$:

$$\begin{array}{c}\hfill M_0[{\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }\rangle M_1\dots M_{ho-1}[{\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }\rangle M_{ho}[{\sigma }_{u_{ho+1}}^{\prime }\rangle M_{ho+1}.\end{array}$$

Constraints (3.c) and (3.d) demonstrate the congruity between the transition sequences, the associated labels, and the marking measurements, which suggests that $\Lambda (\rho (M_0,{\sigma }^{\prime }))={\widehat{M}}_0{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho}$. Hence, $\sigma \in \mathcal{S}(w)$. □

5.2. Non-Secrecy Assurance

To ensure the language opacity of a POPN, we simply prove that for each observation sequence w, there exists one transition sequence ${\sigma }^{\prime }\in \mathcal{S}(w)$, such that ${\sigma }^{\prime }\notin {\mathcal{L}}_s(w)$. In other words, for all $\sigma \in {\mathcal{L}}_s(w)$, we prove that ${\sigma }^{\prime }\ne \sigma$. Let $z_i\in {\mathbb{Z}}^{{\tilde{n}}_u}$ and $q_j\in {\mathbb{Z}}^{n_d}$ be two vectors satisfying $z_i={\overrightarrow{\sigma }}_{u_i}^{\prime }-{\overrightarrow{\sigma }}_{u_i},i\in \{1,\dots ,ho+1\}$ and $q_j={\overrightarrow{\sigma }}_{e_j}^{\prime }-{\overrightarrow{\sigma }}_{e_j},j\in \{1,\dots ,ho\}$. An entry $z_{ik}$ of vector $z_i$ can be characterized as follows:

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}{z}_{ik}=0,\hfill & \mathrm{if}{\overrightarrow{\sigma }}_{u_i}^{\prime }={\overrightarrow{\sigma }}_{u_i}\hfill \\ |z_{ik}|⩾1,\hfill & \mathrm{otherwise}.\hfill \end{array}\right.\end{array}$$

(4)

Similarly, an entry $q_{jk}$ of vector $q_j$ can be characterized by

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}{q}_{jk}=0,\hfill & \mathrm{if}{\overrightarrow{\sigma }}_{e_j}^{\prime }={\overrightarrow{\sigma }}_{e_j}\hfill \\ |q_{jk}|⩾1,\hfill & \mathrm{otherwise}.\hfill \end{array}\right.\end{array}$$

(5)

To verify that $\sigma \ne {\sigma }^{\prime }$, we have to prove that there is at least one entry $z_{ik}$ of $z_i$ ($q_{jk}$ of $q_j$), such that $|z_{ik}|⩾1$ ($|q_{jk}|⩾1$).

Proposition 3. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN, $w={\widehat{M}}_0{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho}\in \mathcal{O}(Q,M_0)$ be an observation sequence, and $\sigma ={\sigma }_{u_1}{\sigma }_{e_1}{\sigma }_{u_2}{\sigma }_{e_2}\dots {\sigma }_{u_{ho}}{\sigma }_{e_{ho}}{\sigma }_{u_{ho+1}}$ be a transition sequence, such that $\sigma \in \mathcal{S}(w)$. A transition sequence ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }\in \mathcal{S}(w)\setminus \left\{\sigma \right\}$ if and only if ${\overrightarrow{\sigma }}_{u_1}^{\prime },{\overrightarrow{\sigma }}_{u_2}^{\prime },\cdots ,{\overrightarrow{\sigma }}_{u_{ho+1}}^{\prime },{\overrightarrow{\sigma }}_{e_1}^{\prime },{\overrightarrow{\sigma }}_{e_2}^{\prime },\dots ,{\overrightarrow{\sigma }}_{e_{ho}}^{\prime }$ satisfy $\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)$, together with the following constraint set:

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}\left.\begin{array}{c}{\overrightarrow{z}}_i={\overrightarrow{\sigma }}_{u_i}^{\prime }-{\overrightarrow{\sigma }}_{u_i}\hfill \\ {\displaystyle \sum _{i=1}^{ho+1}\sum _{k=1}^{{\tilde{n}}_u}}\left|z_{ik}\right|\ge 1·y_1\hfill \\ {\overrightarrow{z}}_i={(z_{ik})}_{k\in [1,\dots ,{\tilde{n}}_u]}\hfill \end{array}\right\}\hfill & (a)\hfill \\ \left.\begin{array}{c}{\overrightarrow{q}}_j={\overrightarrow{\sigma }}_{e_j}^{\prime }-{\overrightarrow{\sigma }}_{e_j}\hfill \\ {\displaystyle \sum _{j=1}^{ho}\sum _{k=1}^{n_d}}\left|q_{jk}\right|\ge 1·y_2\hfill \\ {\overrightarrow{q}}_j={(q_{jk})}_{k\in [1,\dots ,n_d]}\hfill \end{array}\right\}\hfill & (b)\hfill \\ \left.\begin{array}{c}{M}_{i-1}=M_0+{\tilde{C}}_u{\displaystyle \sum _{k=1}^{i-1}}{\overrightarrow{\sigma }}_{u_k}^{\prime }+C_d{\displaystyle \sum _{k=1}^{i-1}}{\overrightarrow{\sigma }}_{e_k}^{\prime }\hfill \\ M_{i-1}+{\tilde{C}}_u({\displaystyle \sum _{k=1}^{r-1}}{\overrightarrow{x}}_{ik})\ge {\widetilde{Pre}}_u·{\overrightarrow{x}}_{ir}\hfill \\ {\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}\le {\overrightarrow{\sigma }}_{u_i}^{\prime }\hfill \\ v_i={\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}(t_{ik})\hfill \\ {\displaystyle \sum _{i=1}^{ho+1}}{v}_i\le {\displaystyle \sum _{i=1}^{ho+1}}{L}_i-y_3\hfill \\ i=1,\dots ,ho+1,j\in \{1,\dots ,ho\},\hfill \\ r=1,\dots ,L_i,l=1,\dots ,L_i-1,\hfill \\ {\overrightarrow{x}}_{ik}\in {\{0,1\}}^{{\tilde{n}}_u},v_i\in \mathbb{N}\hfill \end{array}\right\}\hfill & (c)\hfill \\ \left.\begin{array}{c}{y}_1+y_2+y_3\ge 1\hfill \\ y_1,y_2,y_3\in \{0,1\}\hfill \end{array}\right\}\hfill & (d),\hfill \end{array}\right.\end{array}$$

(6)

where:

• ${\sigma }_{u_i}={(t_{ik})}_{k\in [1,\dots ,L_i]}$, with $L_i=\left|{\sigma }_{u_i}\right|$ if $|{\sigma }_{u_i}|\ge 1$ and $L_i=1$ otherwise, for $i\in \{1,\dots ,ho+1\}$;
• Const. (6.a) checks the difference between ${\overrightarrow{\sigma }}_{u_i}^{\prime }$ and ${\overrightarrow{\sigma }}_{u_i}$;
• Const. (6.b) expresses the difference between ${\overrightarrow{\sigma }}_{e_j}^{\prime }$ and ${\overrightarrow{\sigma }}_{e_j}$;
• Const. (6.c) indicates whether ${\overrightarrow{\sigma }}_{u_i}$ and ${\overrightarrow{\sigma }}_{u_i}^{\prime }$ have the same firing order or not;
• Const. (6.d) uses three binary variables, $y_1,y_2$, and $y_3$, to ensure that at least one of Constraints (6.a), (6.b) or (6.c) is satisfied.

Proof. 

(If) If there exists ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }$${\sigma }_{u_{ho+1}}^{\prime }$, whose firing vectors ${\overrightarrow{\sigma }}_{u_1}^{\prime }$, ${\overrightarrow{\sigma }}_{u_2}^{\prime }$, ⋯, ${\overrightarrow{\sigma }}_{u_{ho+1}}^{\prime }$, ${\overrightarrow{\sigma }}_{e_1}^{\prime }$, ${\overrightarrow{\sigma }}_{e_2}^{\prime }$, …, ${\overrightarrow{\sigma }}_{e_{ho}}^{\prime }$ satisfy the Constraint Set $\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)$, then by Proposition 2, ${\sigma }^{\prime }\in \mathcal{S}(w)$. In Constraint Set (6.a), we compute the difference between the firing vectors of ${\sigma }^{\prime }$ and the associated firing vectors of $\sigma$, using ${\overrightarrow{z}}_i$ and ${\overrightarrow{q}}_j$. Then, we check for each ${\overrightarrow{z}}_i,i\in \{1,\dots ,ho+1\}({\overrightarrow{q}}_j,j\in \{1,\dots ,ho)\}$ if there exists at least an entry $z_{ik}(q_{jk})$, such that $|z_{ik}|\ge 1(|q_{jk}|\ge 1)$, to ensure that ${\sigma }^{\prime }$ is different from $\sigma$ for at least one firing vector. In fact, ${\sigma }_{e_j}^{\prime }$ and ${\sigma }_{e_j}$ are both composed of one transition (i.e., $|{\sigma }_{e_j}|=|{\sigma }_{e_j}^{\prime }|=1$), so it is easy to check whether ${\sigma }_{e_j}={\sigma }_{e_j}^{\prime }$, using the firing vectors only. However, in the case of ${\overrightarrow{\sigma }}_{u_i}^{\prime }={\overrightarrow{\sigma }}_{u_i}$, only the transition firing order can distinguish ${\sigma }_{u_i}^{\prime }$ from ${\sigma }_{u_i}$. In this situation, for $L_i\ge 1$, we split ${\overrightarrow{\sigma }}_{u_i}^{\prime }$ into $L_i$ sub-firing vectors ${\overrightarrow{x}}_{ik}$, using the enabling condition $M_{i-1}+{\tilde{C}}_u{\displaystyle \sum _{k=1}^{r-1}}{\overrightarrow{x}}_{ik}\ge {\widetilde{Pre}}_u·{\overrightarrow{x}}_{ir}$, such that ${\overrightarrow{\sigma }}_{u_i}^{\prime }={\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}$. The value $v_i={\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}(t_{ik})$ corresponds to the number of unobservable transitions with the same firing order in ${\sigma }_{u_i}^{\prime }$ and ${\sigma }_{u_i}$. Therefore, if $v_i\le L_i-y_3$ holds, where $y_3$ is a binary decision variable, then ${\sigma }_{u_i}^{\prime }$ is different from ${\sigma }_{u_i}$ for at least one transition. Given the binary decision variables $y_1,y_2$, and $y_3$, Constraints (6.d) indicate that the satisfaction of either (6.a), (6.b) or (6.c) correspond to the satisfaction of the linear constraint $y_1+y_2+y_3\ge 1$. Thus, $\sigma$ and ${\sigma }^{\prime }$ are different for at least one transition. Accordingly, ${\sigma }^{\prime }\in \mathcal{S}(w)\setminus \left\{\sigma \right\}$ holds.

(Only if) Given a transition sequence $\sigma \in \mathcal{S}(w)$, assume that there exists ${\sigma }^{\prime }\in \mathcal{S}(w)\setminus \left\{\sigma \right\}$. By Proposition 2, ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }$, such that its firing vectors satisfy $\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)$. In addition, we have $\sigma \ne {\sigma }^{\prime }$, which possibly implies the existence of a particular step i, such that ${\overrightarrow{\sigma }}_{u_i}^{\prime }\ne {\overrightarrow{\sigma }}_{u_i}$ or a step j, such that ${\overrightarrow{\sigma }}_{e_j}^{\prime }\ne {\overrightarrow{\sigma }}_{e_j}$. Thus, Constraints (6.a) and (6.b) hold. If not, there exist two sub-sequences ${\sigma }_{u_i}^{\prime }$ and ${\sigma }_{u_i}$ with identical firing vectors but different transition firing orders, and then Constraint (6.c) holds. Finally, the satisfaction of either (6.a), (6.b) or (6.c) implies the satisfaction of Constraint (6.d). □

Evidently, with the use an absolute value function in (6.a) and (6.b), the problem becomes non-linear. In this case, it is difficult to apply standard ILP solvers to solve it. However, it is possible to linearize the absolute value of an integer variable (i.e., $|z_{ik}|$), by replacing $z_{ik}$ and $|z_{ik}|$, using two integer variables $z_{ik}^{+}$ and $z_{ik}^{-}$ as follows:

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}{z}_{ik}=z_{ik}^{+}-z_{ik}^{-}\hfill & (a)\hfill \\ |z_{ik}|=z_{ik}^{+}+z_{ik}^{-}\hfill & (b)\hfill \\ z_{ik}^{+}\le U·a_{ik}\hfill & (c)\hfill \\ z_{ik}^{-}\le U·(1-a_{ik})\hfill & (d).\hfill \\ a_{ik}\in \{0,1\},z_{ik}^{+},z_{ik}^{-}\in \mathbb{N}\hfill \end{array}\right.\end{array}$$

(7)

U is an integer satisfying $U\ge max\{B(p)|p\in P\}$, where $B(p)$ denotes place p upper bound [19]. Constraints (7.c) and (7.d) guarantee that either $z_{ik}^{+}$ or $z_{ik}^{-}$ (or both, if $z_{ik}=0$) will be 0. Thus, $z_{ik}=z_{ik}^{+}$ when $z_{ik}\ge 0$, and $z_{ik}=z_{ik}^{-}$ when $z_{ik}\le 0$. We can exploit the notation in (7) to remove $|z_{ik}|$ in (6.a) and $|q_{jk}|$ in (6.b), to relax (6) into a set of linear constraints $\mathfrak{NS}(M_0,C_d,{\tilde{C}}_u,\sigma )=$

$$\begin{array}{c}\hfill \left\{\begin{array}{cc}\left.\begin{array}{cc}{\overrightarrow{z}}_i^{+}-{\overrightarrow{z}}_i^{-}={\overrightarrow{\sigma }}_{u_i}^{\prime }-{\overrightarrow{\sigma }}_{u_i}\hfill & (a_1)\hfill \\ {\displaystyle \sum _{i=1}^{ho+1}\sum _{k=1}^{{\tilde{n}}_u}}{z}_{ik}^{+}+z_{ik}^{-}\ge 1·y_1\hfill & (a_2)\hfill \\ \left.\begin{array}{c}{z}_{ik}^{+}\le U·a_{ik}\hfill \\ z_{ik}^{-}\le U·(1-a_{ik})\hfill \end{array}\right\}\hfill & (a_3)\hfill \\ {\overrightarrow{z}}_i^{+}={(z_{ik}^{+})}_{k\in [1,\dots ,{\tilde{n}}_u]},\hfill \\ {\overrightarrow{z}}_i^{-}={(z_{ik}^{-})}_{k\in [1,\dots ,{\tilde{n}}_u]},\hfill \end{array}\right\}\hfill & (a)\hfill \\ \left.\begin{array}{cc}{\overrightarrow{q}}_j^{+}-{\overrightarrow{q}}_j^{-}={\overrightarrow{\sigma }}_{e_j}^{\prime }-{\overrightarrow{\sigma }}_{e_j}\hfill & (b_1)\hfill \\ {\displaystyle \sum _{i=1}^{ho}\sum _{k=1}^{n_d}}{q}_{jk}^{+}+q_{jk}^{-}\ge 1·y_2\hfill & (b_2)\hfill \\ \left.\begin{array}{c}{q}_{jk}^{+}\le U·b_{jk}\hfill \\ q_{jk}^{-}\le U·(1-b_{jk})\hfill \end{array}\right\}\hfill & (b_3)\hfill \\ {\overrightarrow{q}}_j^{+}={(q_{jk}^{+})}_{k\in [1,\dots ,n_d]},\hfill \\ {\overrightarrow{q}}_j^{+}={(q_{jk}^{-})}_{k\in [1,\dots ,n_d]}\hfill \end{array}\right\}\hfill & (b)\hfill \\ \left.\begin{array}{cc}{M}_{i-1}=M_0+{\tilde{C}}_u{\displaystyle \sum _{k=1}^{i-1}}{\overrightarrow{\sigma }}_{u_k}^{\prime }+C_d{\displaystyle \sum _{k=1}^{i-1}}{\overrightarrow{\sigma }}_{e_k}^{\prime }\hfill & (c_1)\hfill \\ M_{i-1}+{\tilde{C}}_u({\displaystyle \sum _{k=1}^{r-1}}{\overrightarrow{x}}_{ik})\ge {\widetilde{Pre}}_u·{\overrightarrow{x}}_{ir}\hfill & (c_2)\hfill \\ {\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}\le {\overrightarrow{\sigma }}_{u_i}^{\prime }\hfill & (c_3)\hfill \\ v_i={\displaystyle \sum _{k=1}^{L_i}}{\overrightarrow{x}}_{ik}(t_{ik})\hfill & (c_4)\hfill \\ {\displaystyle \sum _{i=1}^{ho+1}}{v}_i\le {\displaystyle \sum _{i=1}^{ho+1}}{L}_i-y_3\hfill & (c_5)\hfill \\ i=\{1,\dots ,ho+1\},j\in \{1,\dots ,ho\}\hfill \\ r=\{1,\dots ,L_i\},l=\{1\dots ,L_i-1\},\hfill \\ {\overrightarrow{x}}_{ik}\in {\{0,1\}}^{{\tilde{n}}_u},v_i\in \mathbb{N}\hfill \end{array}\right\}\hfill & (c)\hfill \\ \left.\begin{array}{c}{y}_1+y_2+y_3\ge 1\hfill \\ y_1,y_2,y_3\in \{0,1\}\hfill \end{array}\right\}\hfill & (d).\hfill \end{array}\right.\end{array}$$

(8)

Theorem 1. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. Q is language-opaque, with regard to $L_s$, if, for any $w\in \mathcal{O}(L_s)$, the following system of linear equations and inequalities (combining (3) and (6)), denoted by $\mathcal{G}(w)$,

$$\mathcal{G}(w)=\left\{\begin{array}{cc}\hfill & \mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w),\hfill \\ \hfill & \mathfrak{NS}(M_0,C_d,{\tilde{C}}_u,\sigma ),\sigma \in L_s\hfill \end{array}\right.$$

(9)

admits at least one feasible solution.

Proof. 

Let $w\in \mathcal{O}(Q,M_0)$ be an observation sequence. Assume that there exists ${\sigma }^{\prime }$, such that ${\sigma }^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }\dots {\sigma }_{u_{ho}}^{\prime }{\sigma }_{e_{ho}}^{\prime }{\sigma }_{u_{ho+1}}^{\prime }$ satisfying the Constraints Set $\mathcal{G}(w)$. We have the firing vectors of ${\sigma }^{\prime }$ satisfy the constraint set $\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)$. According to Proposition 2, ${\sigma }^{\prime }\in \mathcal{S}(w)$. We also have the firing vectors of ${\sigma }^{\prime }$ satisfy $\mathfrak{NS}(M_0,C_d,{\tilde{C}}_u,\sigma )for\sigma \in L_s$. Based on Proposition 3, ${\sigma }^{\prime }\in \mathcal{S}(w)\setminus \left\{\sigma \right\}$ for each $\sigma \in L_s$: that is to say, ${\sigma }^{\prime }\in \mathcal{S}(w)\setminus L_s$. According to Defintion 7, w is LBO, with regard to $L_s$. □

Note that the Constraint set $\mathcal{G}(w)$ is usually referred to as a “feasibility problem”. One way to solve a feasibility problem is to convert it into an optimization problem with a dummy objective function, and then solve it using ILP solvers. This objective function could be a linear combination of the subset of decision variables. When we aim to maximize it, we will discover a feasible solution, provided one exists. Conversely, if we aim to minimize it, we will attain a different feasible solution, typically located on the opposite side of the feasible region. One option for the objective function would be

$$min{\overrightarrow{\mathbf{1}}}_{{\tilde{n}}_u}^T·{\displaystyle \sum _{i=1}^{ho+1}}{\overrightarrow{\sigma }}_{u_i}^{\prime }.$$

5.3. Complexity Analysis and Comparison

Theoretically, an ILP problem is NP-hard, and the computational overhead of its resolution depends on its variables and constraints numbers. In

Table 1. Integer variables of ILPP $\mathcal{G}(w)$.

Variable	Type	Size	Range	Total
${\overrightarrow{\sigma }}_{u_i}$	Integer	${\tilde{n}}_u\times 1$	$i\in \{1,\dots ,ho+1\}$	${\tilde{n}}_u·(ho+1)$
${\overrightarrow{\sigma }}_{e_j}$	Integer	$n_d\times 1$	$i\in \{1,\dots ,ho+1\}$	$n_d·ho$
$z_{ik}^{+}$	Integer	$1\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, ${\tilde{n}}_u$}	${\tilde{n}}_u·(ho+1)·\eta$
$z_{ik}^{-}$	Integer	$1\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, ${\tilde{n}}_u$}	${\tilde{n}}_u·(ho+1)·\eta$
$q_{jk}^{+}$	Integer	$1\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, nd}	$n_d·ho·\eta$
$q_{jk}^{-}$	Integer	$1\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, nd}	$n_d·ho·\eta$
$a_{ik}$	Binary	$1\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, ${\tilde{n}}_u$}	${\tilde{n}}_u·(ho+1)·\eta$
$b_{jk}$	Binary	$j\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, nd}	$n_d·ho·\eta$
U	Integer	$1\times 1$	1	$1·\eta$
$M_{i-1}$	Integer	$m\times 1$	$i\in \{1,\dots ,ho+1\}$	$m·(ho+1)·\eta$
${\overrightarrow{x}}_{ik}$	Binary	${\tilde{n}}_u\times 1$	$i\in \{1,\dots ,ho+1\}$ k ∈ {1, …, Li}	${\tilde{n}}_u·(ho+1)·L_i·\eta$
$v_i$	Integer	$1\times 1$	$i\in \{1,\dots ,ho+1\}$	$(ho+1)·\eta$
$y_1$	Binary	$1\times 1$	1	$1·\eta$
$y_2$	Binary	$1\times 1$	1	$1·\eta$
$y_3$	Binary	$1\times 1$	1	$1·\eta$

, we analyze the number of variables and constraints of ILPP (9). Columns $1,2$, and 3 denote the lists of variables, their types, and their sizes, respectively. Column 4 indicates the range of subscripts associated with each variable, and Column 5 denotes the total number of variables in scalar form. From the presented results, it is obvious that the numbers of variables in the worst case is

$${\tilde{n}}_u·(ho+1)·(1+3·\eta +L_i·\eta )+n_d·ho·(1+3·\eta )+(ho+1)·\eta ·(m+1)+4·\eta ,$$

where $\eta =|{\mathcal{L}}_s(w)|$.

In

Table 2. Constraints of ILPP $\mathcal{G}(w)$.

Constraint Set	Sub-Constraints	Extent	Range	Total
f	1	1	1	1
$\mathfrak{C}(M_0,C_d,{\tilde{C}}_u,w)$	3.a	m	1	m
	3.b	m	$l\in \{1\dots ho\}$	$m·ho$
	3.c	$m_o$	$i\in \{1\dots ho+1\}$ j ∈ {1 … ho}	$m_o·(ho+1)$ mo·ho
	3.d	2	$j\in \{1\dots ho\}$	$2·ho$
$\mathfrak{NS}(M_0,C_d,{\tilde{C}}_u,\sigma )$$\sigma \in {\mathcal{L}}_s(w)$	8.a1	${\tilde{n}}_u$	$i\in \{1\dots ho+1\}$	${\tilde{n}}_u·(ho+1)·\eta$
	8.b1	$n_d$	$j\in \{1\dots ho\}$	$n_d·ho·\eta$
	8.a2	1	1	$1·\eta$
	8.b2	1	1	$1·\eta$
	8.a3	2	$i\in \{1\dots ho+1\}$ k {1 …nu}	$2·{\tilde{n}}_u·(ho+1)·\eta$
	8.b3	2	$j\in \{1\dots ho\}$ k {1 …nd}	$2·n_d·ho·\eta$
	8.c1	m	$i\in \{1\dots ho+1\}$	${\tilde{n}}_u·(ho+1)·\eta$
	8.c2	m	$i\in \{1\dots ho+1\}$ r ∈ {1 … Li}	$m·L_i(ho+1)·\eta$
	8.c3	1	$i\in \{1\dots ho+1\}$	$(ho+1)·\eta$
	8.c4	1	$i\in \{1\dots ho+1\}$	$(ho+1)·\eta$
	8.c5	1	1	$1·\eta$
	8.d	1	1	$1·\eta$

, the first column denotes the constraint sets involved in ILPP (9), the second column represents the sub-constraints of each constraint set, the third column shows the extent in lines of each sub-constraint, and the fourth column denotes the range of their associated indexes. Finally, Column 5 denotes the total number of constraints contained in each sub-constraint set. According to the results reported in Table 2, we can deduce the number of constraints in ILPP (9), which is given by $(ho+1)·(4·{\tilde{n}}_u·\eta +m_o+m·L_i·\eta +2·\eta +m)+ho·(m_o+3·n_d·\eta +2)+4·\eta +1$. As a result, the variables and constraints numbers are polynomial in the secret observation sequence length.

In

Table 3. LBO verification approaches.

	Framework	Graph	Secret Nature	Complexity
[5]	Automaton	No	Labels	Exponential
[10]	LPN	Yes	Observable transitions	Exponential
[13]	LPN	No	Labels	NP-hard
Proposed approach	POPN	No	Transitions	NP-hard

, the proposed approach is compared to previous works on LBO verification presented in [5,10,13]. The second column presents the application framework. The third column indicates whether the verification approach is based on an off-line graph computation or not. The fourth column denotes the secret nature. Finally, the fifth column reports the complexity of each approach.

6. Experimental Results: A Manufacturing System

In this section, we exhibit the above results, using the example of an automated manufacturing system from [20], as shown in Figure 2. It contains 46 places and 39 transitions, including two inputs (I1 and I2), two outputs (O1 and O2), four machines (M1–M4), one buffer with finite capacity (B), and four robots (R1–R4). In [20], the operation of this system is discussed in detail. Assume that I1 and I2 each include a sensor that displays the number of items handled by the corresponding lines L1 and L2. Furthermore, sensors are installed on the machines (M1–M4), the two robots (R1 and R2), and the buffer (B), to indicate when an item is added. This PN might be considered as a POPN.

We have:

$T_d=\{t_1,t_2,t_6,t_7,t_8,t_9,t_{13},t_{14},t_{15},t_{16},t_{17},t_{21},t_{22},t_{23},$$t_{24},t_{28},t_{29},t_{30},t_{34},$$t_{35},t_{38},t_{39}\}.$

${\tilde{T}}_u=\{t_3,t_4,t_5,t_{10},t_{11},t_{12},t_{18},t_{19},t_{20},t_{25},t_{26},t_{27},t_{31},t_{32},$$t_{33},t_{36},t_{37}\}.$

Let $L_s=\{{\sigma }_1,{\sigma }_2,{\sigma }_3,{\sigma }_4,{\sigma }_5,{\sigma }_6,{\sigma }_7,{\sigma }_8,{\sigma }_9,{\sigma }_{10},{\sigma }_{11},{\sigma }_{12}\}$ be a secret language and $\mathcal{O}(L_s)=\{w_1,w_2,w_3\}$ be its associated secret observation sequences, as specified in

Table 4. Secret transition sequences.

${\mathit{\sigma }}_{\mathit{i}}$	Value	${\mathcal{L}}_{\mathit{s}}(\mathit{\sigma })$
${\sigma }_1$	$t_1{t}_2{t}_4{t}_3{t}_5{t}_6$	$w_1$
${\sigma }_2$	$t_1{t}_2{t}_{16}$	$w_2$
${\sigma }_3$	$t_1{t}_2{t}_{16}{t}_3,t_1{t}_2{t}_3{t}_4{t}_5{t}_{36}{t}_{16}$	$w_2$
${\sigma }_4$	$t_1{t}_2{t}_3{t}_4{t}_5{t}_{16},t_1{t}_2{t}_3{t}_4{t}_{16}{t}_5$	$w_2$
${\sigma }_5$	$t_1{t}_2{t}_3{t}_4{t}_5{t}_{36}{t}_{34}$	$w_1$
${\sigma }_6$	$t_1{t}_2{t}_3{t}_4{t}_5{t}_{16}{t}_{36}$	$w_2$
${\sigma }_7$	$t_1{t}_2{t}_3{t}_4{t}_{16}$	$w_2$
${\sigma }_8$	$t_1{t}_2{t}_3{t}_4{t}_{16}{t}_5{t}_{36}$	$w_2$
${\sigma }_9$	$t_1{t}_2{t}_{16}{t}_3{t}_4{t}_5$	$w_2$
${\sigma }_{10}$	$t_1{t}_2{t}_{16}{t}_3{t}_4$	$w_2$
${\sigma }_{11}$	$t_1{t}_2{t}_{16}{t}_3{t}_4{t}_5{t}_{36}$	$w_2$
${\sigma }_{12}$	$t_1{t}_2{t}_3{t}_4{t}_5{t}_6{t}_7{t}_8{t}_9{t}_{10}{t}_{11}{t}_{12}{t}_{13}$	$w_3$

and

Table 5. Secret observation sequences.

${\mathit{w}}_{\mathit{i}}$	Value
$w_1$	${[1108111111]}^{T}a{[0108111111]}^T{[0118110111]}^{T}b{[0118111111]}^T$
$w_2$	${[1108111111]}^{T}a{[0108111111]}^T{[0118110111]}^{T}e{[0008110111]}^T$
$w_3$	${[1108111111]}^{T}a{[0108111111]}^T{[0118110111]}^{T}b{[0118111111]}^T$
	${[0117111111]}^{T}b{[0118111111]}^T{[0118111101]}^{T}c{[0118011111]}^T$

, respectively. The results reported in this paper were obtained by solving (9) using CPLEX, which is a commercial Python library for linear programming optimization.

For $\mathcal{G}(w_1)$, there exists a sequence ${\sigma }_1^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }{\sigma }_{u_3}^{\prime }{\sigma }_{e_3}^{\prime }{\sigma }_{u_4}^{\prime }=t_1{t}_2{t}_3{t}_4{t}_5{t}_6$ enabled at $M_0$, such that ${\sigma }_1^{\prime }\notin L_s$ and $\Lambda (\rho (M_0,{\sigma }_1^{\prime }))=w_1$, whose firing vectors ${\overrightarrow{\sigma }}_{u_1}^{\prime }=\overrightarrow{\mathbf{0}}$, ${\overrightarrow{\sigma }}_{e_1}^{\prime }=b_1,{\overrightarrow{\sigma }}_{u_2}^{\prime }=\overrightarrow{\mathbf{0}},{\overrightarrow{\sigma }}_{e_2}^{\prime }=b_2,{\overrightarrow{\sigma }}_{u_3}^{\prime }=a_1+a_2+a_3,{\overrightarrow{\sigma }}_{e_3}^{\prime }=b_3,{\overrightarrow{\sigma }}_{u_4}^{\prime }=\overrightarrow{\mathbf{0}}$ satisfy (9), where $a_i$ and $b_i$ are called standard basis vectors for ${\mathbb{N}}^{{\tilde{n}}_u}$ and ${\mathbb{N}}^{n_d}$, respectively, having all entries zero, except that the $i^{th}$ entry equals 1. Notice that the solver takes into account the firing order of transitions, since ${\sigma }^{\prime }$ has the same firing vector as the secret sequence $t_1{t}_2{t}_4{t}_3{t}_5{t}_6$.

For $\mathcal{G}(w_2)$, there exists a sequence ${\sigma }_2^{\prime }={\sigma }_{u_1}^{\prime }{\sigma }_{e_1}^{\prime }{\sigma }_{u_2}^{\prime }{\sigma }_{e_2}^{\prime }{\sigma }_{u_3}^{\prime }{\sigma }_{e_3}^{\prime }{\sigma }_{u_4}^{\prime }=t_1{t}_2{t}_4{t}_{16}$ enabled at $M_0$, such that ${\sigma }_2^{\prime }\notin L_s$ and $\Lambda (\rho (M_0,{\sigma }_2^{\prime }))=w_2$, whose firing vectors ${\overrightarrow{\sigma }}_{u_1}^{\prime }=\overrightarrow{\mathbf{0}}$, ${\overrightarrow{\sigma }}_{e_1}^{\prime }=b_1$, ${\overrightarrow{\sigma }}_{u_2}^{\prime }=\overrightarrow{\mathbf{0}}$, ${\overrightarrow{\sigma }}_{e_2}^{\prime }=b_2$, ${\overrightarrow{\sigma }}_{u_3}^{\prime }=a_2$, ${\overrightarrow{\sigma }}_{e_3}^{\prime }=b_{10}$, and ${\overrightarrow{\sigma }}_{u_4}^{\prime }=\overrightarrow{\mathbf{0}}$ satisfy (9).

For $\mathcal{G}(w_3)$, however, the ILP solver does not find any feasible solution, which implies the non-language opacity of the considered POPN.

7. LBO in Decentralized Setting

Modern networking technologies have rendered distributed systems increasingly more broadly used. These systems are composed of multiple networked components that communicate and coordinate actions, to achieve a common goal and appear to end-users as a single coherent entity. Figure 3 illustrates the privacy risks in an IoT-based smart house, where a set of intruders, distributed at different sites, are collecting sensing data and trying to deduce private information.

7.1. Decentralized Opacity with Coordinator

At this point, language-based opacity has been discussed in a centralized framework, where only a single intruder is trying to infer the system’s secret behavior. In this section, we consider decentralized settings, as shown in Figure 4, where a POPN is watched by a set of intruders $\mathcal{J}=\{1,2,\dots ,n\}$ who collaborate to verify, under a given observation sequence, if their language estimation is entirely contained in a secret. Formally, the system Q, with regard to the $j^{th}$ intruder, can be described as follows:

$Q_j=(N,M_0,E_j,V_j,{\delta }_j)$ is a POPN system, where $N=(P,T,Pre,Post)$ and $E_j\subseteq E$ is the set of observable labels by the $j^{th}$ local intruder. As in the previous section, it holds that $P=P_{o,j}\cup P_{u,j}$ and $P_{o,j}\subseteq P_o(P_{u,j}=P\setminus P_{o,j})$ comprise the set of locally observable (unobservable) places of intruder j. In addition, $T=T_{o,j}\cup T_{u,j}$ and $T_{o,j}\subseteq T_o(T_{u,j}=T\setminus T_{o,j})$ comprise the set of locally observable (silent) transitions of intruder j. Moreover, we denote by $T_{d,j}\subseteq T_d$ (${\tilde{T}}_{u,j}=T\setminus T_{d,j}$) the set of locally discernible (truly unobservable) transitions of intruder j. It holds that $|P_{o,j}|=m_{o,j}$, $|P_{u,j}|=m_{u,j}$, $|T_{d,j}|=n_{d,j}$ and $|{\tilde{T}}_{u,j}|={\tilde{n}}_{u,j}$. The matrices ${\tilde{C}}_{u,j}={\widetilde{Post}}_{u,j}-{\widetilde{Pre}}_{u,j}$ and $C_{d,j}=Pos{t}_{d,j}-Pr{e}_{d,j}$, respectively, denote the restrictions of C to ${\tilde{T}}_{u,j}$ and $T_{d,j}$.

The following assumptions are now introduced to this decentralized setting:

A1:

Each intruder has full understanding of the system’s structure and initial marking, but uses his own sensor configuration ${\theta }_j=(V_j,{\delta }_j)$ to track its evolution, where $V_j=(v_{ik})\in {\{0,1\}}^{m_{o,j}\times m}$, such that $v_{ik}=1$ if the $i^{th}$ observable place by intruder j corresponds to place $p_k$ and to 0, otherwise, and where ${\delta }_j$ is a local labeling function, such that ${\delta }_j(t)=\delta (t)$ if $t\in T_{d,j}$ and ${\delta }_j(t)=\epsilon$, otherwise.

A2:

An observable place is observed by at least one local intruder, i.e., ${\bigcup }_{j\in J}{P}_{o,j}=P_o$.

A3:

A discernible transition is discerned by at least one local intruder, i.e., ${\bigcup }_{j\in J}{T}_{d,j}=T_d$.

A4:

Let $⪯$ be an ordering relation defined between sensor configurations, such that ${\theta }_i⪯{\theta }_j$ if intruder j observes more than intruder i, i.e., ${\theta }_i⪯{\theta }_j$ if $T_{d,i}\subseteq T_{d,j}\wedge P_{o,i}\subseteq P_{o,j}$.

Given $M[t\rangle M^{\prime }$, a state transition, the obtained measurement with respect to a sensor configuration ${\theta }_j$ associated with the jth local intruder is defined as follows:

$$\begin{array}{c}\hfill {\rho }_j(M,t)=\left\{\begin{array}{cc}{\epsilon }_p,\hfill & \mathrm{if}(\widehat{M}={\widehat{M}}^{\prime })\wedge ({\delta }_j(t)=\epsilon )\hfill \\ \widehat{M}{\delta }_j(t){\widehat{M}}^{\prime },\hfill & \mathrm{otherwise}.\hfill \end{array}\right.\end{array}$$

Given $\sigma =t_1{t}_2\dots t_h\in T^{*}$ and $M{t}_1{M}_1{t}_2{M}_2\dots M_{h-1}{t}_h{M}_h$, the evolution generated by firing $\sigma$ at M, the measurement sequence associated with each local intruder j is defined as

$$\begin{array}{cc}\hfill {\rho }_j(M,\sigma )& ={\rho }_j(M,t_1){\rho }_j(M_1,t_2)\dots {\rho }_j(M_{h-1},t_h)\hfill \\ \hfill & ={\widehat{M}}_{}{e}_1{\widehat{M}}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{h{o}_j-1}{\widehat{M}}_{h{o}_j-1}{e}_{h{o}_j}{\widehat{M}}_{h{o}_j},\hfill \end{array}$$

where $e_i\in E_j\cup \left\{\epsilon \right\}$, $h{o}_j\le h$, and the associated local observation sequence for each intruder j is defined as $w_j=\Lambda ({\rho }_j(M,\sigma ))={\widehat{M}}_{}{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{h{o}_j-1}{e}_{h{o}_j}{\widehat{M}}_{h{o}_j}$.

The firing sequences consistent with a local observation $w_j$ are denoted by ${\mathcal{S}}_j(w_j)=\{\sigma \in T^{*}|\Lambda ({\rho }_j(M_0,\sigma ))=w_j\}$. As illustrated in Figure 4, after the firing of a transition sequence $\sigma$, each intruder j performs an event sequence estimation ${\mathcal{S}}_j(w_j)$, using its local observation sequence $w_j$, then sends it to a coordinator C. Based on the received information from all intruders, the coordinator evaluates its general estimation $\Gamma (w)$ by finding the intersection of the received local estimations. Therefore, the coordination between intruders is called an intersection-based coordination protocol $\mathcal{P}$.

Definition 8. 

An intersection-based coordination protocol $\mathcal{P}$ is defined by the following rules:

R1: 

The $T_{u,j}$-induced subnet and the $T_{o,j}$-induced subnet are acyclic for any local intruder $j\in \mathcal{J}$.

R2: 

The general estimation is $\Gamma (w)={\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)$.

R3: 

The more an intruder observes, the better its estimation will be, i.e., ${\theta }_i⪯{\theta }_j$ if, for all $w\in \mathcal{O}(Q,M_0)$, ${\mathcal{S}}_j(w_j)\subseteq {\mathcal{S}}_i(w_i)$.

R4: 

The coordinator collects the event sequence estimation generated by each intruder without delay.

Remark 1. 

Let Q be a POPN, and $\mathcal{P}$ be an intersection-based coordination protocol; $T_{d,c}\subseteq T_d$ and $P_{o,c}\subseteq P_o$ are, respectively, the discernible transitions and observable places of Q, with regard to a coordinator C. Protocol $\mathcal{P}$ allows the coordinator to see the system’s original behavior: namely, $T_{d,c}=T_d$ and $P_{o,c}=P_o$.

In detail, we have $\Gamma (w)={\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)$; then, for all $w\in \mathcal{O}(Q,M_0)$, $\Gamma (w)\subseteq {\mathcal{S}}_j(w_j),j\in \mathcal{J}$. We denote by ${\theta }_c$ the sensor configuration of the coordinator. Under Rule R3, ${\theta }_j⪯{\theta }_c$ for $j\in \mathcal{J}$; thus, we can say that the coordinator observes more than all intruders $j\in \mathcal{J}$. According to Assumption (A4), for all $j\in \mathcal{J}$, we have $T_{d,j}\subseteq T_{d,c}$ and $P_{o,j}\subseteq P_{o,c}$. As ${\bigcup }_{j\in J}{T}_{d,j}=T_d$ and ${\bigcup }_{j\in J}{P}_{o,j}=P_o$, we have $T_d\subseteq T_{d,c}$ and $P_o\subseteq P_{o,c}$. Consequently, $T_{d,c}=T_d$ and $P_{o,c}=P_o$. Finally, we conclude that our coordination protocol allows the coordinator to see the system’s original behavior, by taking off the observation masks associated with intruders.

Now, let us characterize LBO in a decentralized setting with coordination: namely, co-language-based opacity (co-LBO).

Definition 9. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. Q is co-LBO, with regard to $L_s$, if and only if, for all $w\in \mathcal{O}(L_s)$, $\Gamma (w)⊈L_s$ holds.

In simple terms, a PN system is co-LBO if it is language-opaque, with regard to the coordinator. Specifically, if two observations are indistinguishable for the coordinator, they are indistinguishable for any intruder $j\in \mathcal{J}$.

Proposition 4. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. If there is at least $w\in \mathcal{O}(L_s)$ and $j\in \mathcal{J}$, such that ${\mathcal{S}}_j(w_j)\subseteq L_s$, then Q is not co-LBO, with regard to $L_s$.

Proof. 

Let $w\in \mathcal{O}(L_s)$ be a secret observation sequence. By Rule R2, we have $\Gamma (w)={\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)$, which implies $\Gamma (w)\subseteq {\mathcal{S}}_j(w_j),j\in \mathcal{J}$. If there exists $w\in \mathcal{O}(L_s)$ and $j\in \mathcal{J}$, such that ${\mathcal{S}}_j(w_j)\subseteq L_s$, then $\Gamma (w)\subseteq L_s$ holds. Therefore, by Definition 9, Q is not co-LBO, with regard to $L_s$. □

The main feature of investigating decentralized opacity consists in preventing a comprehensive computation of all possible sequences that could have fired. According to Proposition 4, if we find at least one intruder j, such that ${\mathcal{S}}_j(w_j)\subseteq L_s$ holds, then Q is not co-LBO, with regard to $L_s$.

If there is no coordination between the intruders, we simply check the LBO for each intruder separately, as indicated in the previous sections. Accordingly, the achieved results can be extended from centralized to decentralized opacity. Therefore, we apply the results of Theorem 1 to each intruder $j\in J$ as follows:

Let $Q=(N,M_0,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. Q is language-opaque, with regard to $L_s$, if, for all $w\in \mathcal{O}(L_s)$, the following ILPP,

$$\left\{\begin{array}{cc}min\hfill & f\hfill \\ s.t.\hfill & \mathfrak{C}(M_0,C_{d,j},{\tilde{C}}_{u,j},w_j),j\in J\hfill \\ \hfill & \mathfrak{NS}(M_0,C_{d,j},{\tilde{C}}_{u,j},\sigma ),\sigma \in L_s\hfill \end{array}\right.$$

(10)

admits at least one feasible solution.

Definition 10. 

Let $L_s$ be a secret language, $w={\widehat{M}}_{}{e}_1{\widehat{M}}_1{e}_2\dots {\widehat{M}}_{ho-1}{e}_{ho}{\widehat{M}}_{ho}(ho\ge 1)$ be a secret observation sequence, i.e., $w\in \mathcal{O}(L_s)$, and $w_j={\widehat{M^{\prime }}}_{}{e}_1^{\prime }{\widehat{M^{\prime }}}_1{e}_2^{\prime }\dots {\widehat{M^{\prime }}}_{h{o}_j-1}{\widehat{M^{\prime }}}_{h{o}_j-1}{e}_{h{o}_j}^{\prime }{\widehat{M^{\prime }}}_{h{o}_j}$$(h{o}_j\le ho)$ be the word projection of w, with regard to the local intruder $j\in J$. We define by $J_{max}(w)=\{j\in J|h_j\ge h_{j^{\prime }},j^{\prime }\in J\}$ the set of local intruders that can observe the maximum of w, called the maximal observers.

Proposition 5. 

Let $Q=(N,M_0,E,V,\delta )$ be a POPN and $L_s\subseteq L(N,M_0)$ be a secret language. Q is co-LBO, with regard to $L_s$, if and only if for each secret observation sequence $w\in \mathcal{O}(L_s)$ and, for at least $j\in J_{max}(w)$, there exists $\sigma \in \mathcal{S}(w_j)\setminus {\mathcal{L}}_s(w)$, such that for each local intruder $j^{\prime }\in \mathcal{J}$, $\Lambda ({\rho }_{j^{\prime }}(M_0,\sigma ))=w_{j^{\prime }}$.

Proof. 

(If) Suppose that, for all $w\in \mathcal{O}(L_s)$ and for at least $j\in J_{max}(w)$, there exists $\sigma \in \mathcal{S}(w_j)\setminus {\mathcal{L}}_s(w)$, such that for each local intruder $j^{\prime }\in \mathcal{J}$, $\Lambda ({\rho }_{j^{\prime }}(M_0,\sigma ))=w_{j^{\prime }}$. Consequently, $\sigma$ is a non-secret transition sequence that is consistent with $w_{j^{\prime }}$ for $j^{\prime }\in \mathcal{J}$ (i.e., $\sigma \in \mathcal{S}(w_{j^{\prime }}),j^{\prime }\in \mathcal{J}$).

We have $\Gamma (w)={\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)$, and thus, $\sigma \in \Gamma (w)\setminus {\mathcal{L}}_s(w)$. Based on Proposition 4, Q is co-LBO, with regard to $L_s$.

(Only if) Let us suppose that Q is co-LBO, with regard to $L_s$, and for at least $w\in \mathcal{O}(L_s)$, and for each $j\in J_{max}(w)$, there does not exist $\sigma \in \mathcal{S}(w_j)\setminus L_s$, such that for each $j^{\prime }\in \mathcal{J}$, $\Lambda ({\rho }_{j^{\prime }}(M_0,\sigma ))=w_{j^{\prime }}$; thus, ${\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)\subseteq L_s$. We have $\Gamma (w)={\bigcap }_{j\in \mathcal{J}}{\mathcal{S}}_j(w_j)\subseteq L_s$ and, therefore, Q is not co-LBO, with regard to $L_s$, which opposes the hypothesis. □

Example 4. 

Consider the POPN in Figure 1. Let $L_s=\{t_1{t}_3{t}_4,t_1{t}_3{t}_2{t}_5,t_1{t}_2{t}_3{t}_5\}$ be a secret language. Its associated secret observation sequences are given by $\mathcal{O}(L_s)=\{w_1,w_2\}$, where $w_1={[10]}^{T}a{[01]}^{T}b[01]$, $w_2={[10]}^{T}a{[01]}^T{[10]}^T$, ${\mathcal{L}}_s(w_1)=\left\{t_1{t}_3{t}_4\right\}$, and ${\mathcal{L}}_s(w_2)=\{t_1{t}_3{t}_2{t}_5,t_1{t}_2{t}_3{t}_5\}$. We have $\mathcal{S}(w_1)=\{t_1{t}_3{t}_4,t_1{t}_4{t}_3\}$ and $\mathcal{S}(w_2)=\{t_1{t}_2{t}_3{t}_5,t_1{t}_3{t}_2{t}_5\}$. Let $J=\{1,2,3\}$ be three local intruders satisfying Assumptions (A1–A4). Their observable places are $P_{o,1}=\left\{p_1\right\}$, $P_{o,2}=\{p_1,p_5\}$, and $P_{o,3}=\varnothing$, respectively, and their discernible transitions are $T_{d,1}=\{t_1,t_5\}$, $T_{d,2}=\left\{t_1\right\}$, and $T_{d,3}=\{t_1,t_5\}$, respectively.

Based on the results reported in

Table 6. Secret words associated with each intruder.

Intruder	Projection of ${\mathit{w}}_1$	Projection of ${\mathit{w}}_2$
1	$[1]a[0]$	$[1]a[0][1]$
2	${[10]}^T{[01]}^T$	${[10]}^T{[01]}^T{[10]}^T$
3	$ab$	a

, we have:

$•{\mathcal{J}}_{max}(w_1)=\left\{3\right\}$; then, we only need to consider the estimation of intruder 3, which is given by ${\mathcal{S}}_3(ab)=\{t_1{t}_3{t}_4,t_1{t}_4{t}_3,t_1{t}_3{t}_4{t}_5,t_1{t}_4{t}_3{t}_5\}$. We have $t_1{t}_4{t}_3\notin L_s$, $\Lambda ({\rho }_1(M_0,t_1{t}_4{t}_3))=[1]a[0]$ and $\Lambda ({\rho }_2(M_0,t_1{t}_4{t}_3))={[10]}^T{[01]}^T$; then, $w_1$ is co-LBO, with regard to $L_s$.

$•{\mathcal{J}}_{max}(w_2)=\{1,2\}$. Since intruders 1 and 2 observe two discernible transitions, while intruder 3 only observes one discernible transition, then we only need to consider the estimation of either intruder 1 or 2. Let us consider the estimation of intruder 2, which is given by ${\mathcal{S}}_2({[10]}^T{[01]}^T{[10]}^T)=\{t_1{t}_2{t}_3{t}_5,t_1{t}_4{t}_3{t}_5,t_1{t}_3{t}_2{t}_5,t_1{t}_3{t}_4{t}_5\}$. We have ${\mathcal{S}}_2(w_2)\setminus {\mathcal{L}}_s(w_2)=\{t_1{t}_4{t}_3{t}_5,t_1{t}_3{t}_4{t}_5\}$. For intruder 3, $\Lambda ({\rho }_3(M_0,t_1{t}_3{t}_4{t}_5))=\Lambda ({\rho }_3(M_0,t_1{t}_4{t}_3{t}_5))=ab\ne a$, then $w_2$ is not co-LBO, with regard to $L_s$.

7.2. Study Case: Temperature Control System

Modern inference techniques, such as machine learning algorithms, can provide enough data to infer user activities, including house occupancy, sleeping patterns, and work schedules. For instance, innocuous data, such as in-home temperatures, could violate the user’s privacy of location, which is the right of individuals to be present in a space without being tracked or monitored or without anyone knowing where they are.

We use a smart thermostat as a case study, which controls the heating and air conditioning in Alice and Bob’s bedroom, shown in Figure 5. The bedroom mainly includes one bed, a window, a door, an air conditioner (AC), a smart thermostat connected to an HVAC (heating, ventilation, and air conditioning) system, a camera, and sensors to measure the necessary data. The thermostat allows for creating a heating and cooling schedule during the day, to save energy. It can also use sensors to check room occupancy, and it automatically sets itself to a standby temperature when the room is empty. The thermostat temperature-control system is modeled by a POPN, as shown in Figure 6. The system turns off (place $p_1$) at 8:00 a.m. (transition $t_4$), when Bob and Alice are outside for work, and starts around 7:00 p.m. (transition $t_1$), then goes directly into a standby state (place $p_3$), which prepares the room for the arrival of Bob and Alice in the evening. From this time on, the system is either in an ON state (place $p_2$), when the presence sensor detects someone inside the room (place $p_4$) or in a Standby state, when the presence sensor does not detect anyone inside the room. Note that the token number in place $p_5$ indicates the number of persons inside the bedroom. When the system goes into the ON state, a quick user identification process starts (place $p_5$), based on a smart facial recognition camera powered by artificial intelligence and placed in the room’s upper left corner. At the end of this process, there are four possibilities:

• Bob is identified (transition $t_9$); then, his preferred reference temperature $T_1^o$ (place $p_6$) will be displayed.
• Alice is identified (transition $t_{10}$) in the room. In this case, the preferred reference temperature will be $T_2^o$ (place $p_7$).
• Bob and Alice are simultaneously present in the room (transition $t_{11}$); then, the reference temperature $T_3^o$ (place $p_8$), on which Bob and Alice have agreed, will be displayed.
• Neither Bob nor Alice is identified (transition $t_8$).

The chosen temperature will remain activated for a duration of $20s$ (transitions $t_{12},t_{13},t_{14}$). At the end of this period, the system saves a temperature record (place $p_9$), to keep track of the user’s schedule and habits, and it then programs itself to match his temperature patterns.

Now, let us check whether intruders can violate Bob and Alice’s privacy of location. Let the secret information be

“Alice is alone inside the bedroom”.

Intruder 1 is observing the occupancy sensor’s activity, and intruder 2 is observing the thermostat’s activity. We have:

$T_{d,1}=\{t_5,t_6\}$

${\tilde{T}}_{u,1}=\{t_1,t_2,t_3,t_4,t_7,t_8,t_9,t_{10},t_{11},t_{12},t_{13},t_{14},t_{15}\}$

$T_{d,2}=\{t_2,t_3,t_7,t_9,t_{10},t_{11},t_{12},t_{13},t_{14},t_{15},t_1,t_4\}$

${\tilde{T}}_{u,2}=\{t_5,t_6,t_8\}$.

When Alice enters the bedroom at 7:30 pm, transition sequence $t_1{t}_6{t}_3{t}_7{t}_8$ fires, and intruder 1 observes $w_1=[0][1]$, which makes him conclude that someone is alone inside the room, but he is not sure whether it is Alice or not.

On the other hand, intruder 2 observes $w_2={[100000]}^{T}a{[001000]}^T{[010000]}^T{[000000]}^T$${[000010]}^T$, and the presence of a token in places $p_7$ indicates that Alice is inside the room, but intruder 2 is not sure whether she is alone or not. We check the opacity for each intruder separately, using Theorem 1. We find that both ILPPs $\mathcal{G}(w_1)$ and $\mathcal{G}(w_2)$ admit a feasible solution. Therefore, the temperature-control system is LBO, with regard to to intruders 1 and 2. However, there is no solution available for ILPP (10). Consequently, the coordination between intruders 1 and 2 can disclose the secret information and infer that Alice is alone inside the room.

8. Conclusions and Future Work

The formulation and verification of LBO in the context of DESs modeled with POPNs were discussed in this research. We provided a necessary and sufficient condition for LBO verification, based on a mathematical description of a net system. Specifically, we proposed linear constraints to check the consistency and non-secrecy aspects of transition sequences. Moreover, these findings were extended to encompass scenarios of decentralized opacity. In these scenarios, the system was examined by multiple intruders, who subsequently shared their observation outcomes with a coordinator, in order to disclose a secret behavior. The proposed approach is more general and scalable than the existing methods for LBO verification in LPNs, as it can be applied to both bounded and unbounded POPNs without requiring any expensive offline computation.

Our future study will extend the proposed ILP-based approach to fault diagnosis in a POPN. Furthermore, it would be of interest to investigate other security problems and potential vulnerabilities, such as unauthorized access, cyber-attacks, intrusion detection, prevention, etc.