Sage Journals: Discover world-class research

Abstract

This work deals with the language-based opacity verification and enforcement problems in discrete event systems modeled with labeled Petri nets. Opacity is a security property that relates to privacy protection by hiding secret information of a system from an external observer called an “intruder”. A secret can be a subset of a system's language. In this case, opacity is referred to as language-based opacity. A system is said to be language-based opaque if an intruder, with a partial observation on the system's behavior, cannot deduce whether the sequences of events corresponding to the generated observations are included in the secret language or not. We propose a novel and efficient approach for language-based opacity verification and enforcement, using the concepts of basis markings and basis partition. First, a sufficient condition is formulated to check language-based opacity for labeled Petri nets by solving an integer-programming problem. A unique graph, called a modified basis reachability graph (MBRG), is then derived to verify different language-based opacity properties. The proposed method relaxes the acyclicity assumption of the unobservable transition subnet thanks to the basis partition notion. A new embedded insertion function technique is also provided to deal with opacity enforcement. This technique ensures that no new observed behavior is created. A verification algorithm is developed to check the enforceability of a system. Finally, once a system is proved to be enforceable, an algorithm is given to construct a new structure, called an insertion automaton, which synthesizes all possible insertion functions that ensure opacity.

Keywords

Language-based opacity labeled Petri net basis reachability graph discrete event system

Introduction

With more and more information exchanges in cyber systems, ensuring information flow properties, in particular opacity, has become a new preoccupation in discrete event systems (DESs). Opacity reflects the ability of a system to hide a given secret from an intruder during the system evolution. The strength of opacity lies in the fact that it can formalize the majority of information flow properties. Therefore, it can be used not only to formalize security and privacy, but also to unify three important properties of DESs, namely detectability, diagnosability, and observability, as special cases. The opacity notion is first introduced in¹ for transition systems and extended later in² and³ using Petri nets and automata. In DESs, opacity can be classified mainly into two classes: state-based opacity (SBO), in which a secret is defined as a state sub-space, and language-based opacity (LBO), where a secret is defined as a subset of a system’s language.

This work focuses on language-based opacity verification and enforcement in DESs modeled with Petri nets. Here, the following setting is involved: (1) a system has a secret behavior, (2) an intruder has full knowledge of the system structure, and (3) the intruder has a partial observation of the system evolution. We have chosen to model the studied system with labeled Petri nets (LPNs) since they are extensively used to model discrete event systems to address many problems such as deadlocks, fault diagnosis, fault identification⁴, and opacity verification. As well, LPNs are chosen in order to present the observation structure of the studied system⁵, to benefit from the advantages of the compact representation of a traditional state space, and to exploit some computation results on reachability in PNs to verify opacity.

The work in⁶ introduced language-based opacity for the first time in the context of automata. Two properties of language-based opacity are defined later in⁷: strong and weak opacity. A language is strongly (resp. weakly) opaque with respect to another language if all (resp. some (not all)) strings in the former are confused with some strings in the latter. Verification and enforcement of opacity properties are addressed using both automata and Petri nets. The opacity verification problem has been treated in various ways to deal with different categories of opacity^8–10. If the opacity is violated, several approaches have been proposed to solve the opacity enforcement problem in diverse manners, such as supervisory control¹¹, dynamic observer¹², and enforcement mechanisms¹³.

In the context of automaton framework, the work in⁷ proposed algorithms to verify both strong and weak LBO, in which the author assumed that the languages involved in a system should be all regular and the information mapping should be a state-based projection. This work requires the construction of nine types of graphs, while the opacity verification in our research demands only the construction of one graph without any requirement to exhaustively enumerate the whole reachability set. The two approaches are computationally expensive. However, the approach in this work is easier to implement. Later, weak opacity has been checked by a polynomial time complexity algorithm proposed in¹⁴. Furthermore, the verification approach in this work not only verifies the different properties of LBO but also identifies the non-opaque secret words that must be distinguished in order to smooth the path of the enforcement, which represents a gap in⁷ and¹⁴.

Petri nets have been recognized as a powerful modeling formalism for DESs in a wide variety of applications^15,16. Nevertheless, only works in¹⁷ and¹⁸ studied language-based opacity verification using Petri nets. The study in¹⁷ verifies language-based opacity using a special structure called a verifier, under the assumption that an intruder is interested in the set of observable transitions only. This work constructs the basis reachability graph (BRG) of a given PN and apply the related approach proposed in⁷. The verifier graph has to be reconstructed each time to check all the elements of the secret language, which means that if the cardinality of a secret language is n, the verifier needs to be reconstructed n times, where the complexity to construct the verifier at a time is $O (n_{s} \times 2^{n b} \times 2^{n b})$ .¹ In¹⁸, an approach based on integer linear programming is proposed, where an algebraic representation of LPN is exploited and two conditions are derived to check LBO with respect to a given finite secret language. The authors in¹⁷ and¹⁸ assume that the subnet derived from $T_{u}$ of a given system is acyclic. This assumption is related to the structure of a system, which means that the approaches with such an assumption cannot be applied if the $T_{u}$ -derived subnet is acyclic. However, the assumption made in this paper requires that the $T_{I}$ -derived subnet should be acyclic. This assumption is negligible comparing with the acyclicity requirement of the $T_{u}$ -derived subnet since the assumption made in this paper is used for computation only and not related to the system’s structure. Therefore, the $T_{I}$ -derived subnet can be adjusted as needed, while the acyclicity of the $T_{u}$ -derived subnet is fixed because it is related to the structure of the system. Thus, our approach is still applicable if the $T_{u}$ -derived subnet is acyclic.

The notion of modified basis reachability graph (MBRG) has been used for couple of years. However, an MBRG is specifically generated depending on the purpose of the research. For instance, the work in¹⁹ constructed an MBRG based on fault transitions through a particular equation in order to compute a graph called basis reachability diagnoser (BRD) to test diagnosability. Meanwhile, in our work, the MBRG construction is based on the properties of the computed basis markings, that is, they are misleading or not misleading. In a similar way, the work in⁵ studied current-state opacity in Petri nets using a modified basis reachability graph. As mentioned above, in this work, we relaxed the acyclicity assumption of the subnet derived from $T_{u}$ made in⁵. In addition, herein, we introduced a unique graph, which is the proposed MBRG, to verify different properties of LBO, while both works in⁵ and¹⁹ require the construction of the MBRG to compute another graph to check the studied properties, i.e., to compute the MBRG observer and the BRD to check CSO and diagnosability, respectively.

For opacity enforcement, the use of enforcement mechanisms allows a system to fully execute its behavior. An insertion function is one of the most popular techniques for these enforcement mechanisms. Such a technique is first introduced in²⁰ and extended later in²¹ and¹³ in the context of automaton framework. This insertion function monitors a system by inserting additional events to the observed behavior of a system when necessary at a run-time. However, the proposed insertion function in this work is embedded into the system itself, rather than being an output monitoring interface. After that, the authors in²² provide an embedded version of the insertion function proposed in²⁰. Recently, the work in²³ focuses on opacity enforcement as well by proposing an extended insertion technique of the one proposed in²². This technique can enforce opacity in a practical manner, i.e., in an embedded way, by inserting symbols before and after an actual system output. The approach in²³ appears to be very close to our proposed enforcement approach. However, herein, we address opacity verification and enforcement while the work in²³ deals with opacity enforcement only. In this manuscript, the insertion function is more powerful for enforcing opacity than the documented ones in the literature as it considers additional enforcement cases that are not previously touched upon in the existing approaches. In the same manner as the proposed function in²³ and contrary to the one proposed in²², the embedded function in this paper inserts not only additional events before an observable event, but it can insert an additional event after the occurrence of an observable event, in which the additional event could be either an observable event or $ε$ . As well, the estimators here are built from a BRG, not an RG or an automaton, which does not require consideration of the whole state space. Therefore, the computational cost of building the estimators is reduced.

In this work, we focus on language-based opacity verification and enforcement in DESs modeled with LPNs. First, based on the notion of explanation, a sufficient condition is provided to decide the opacity of a system by solving an integer programming problem. Unobservable events are then exploited to hide secret information. A unique graph called a modified basis reachability graph (MBRG) is proposed to verify different properties of LBO (strongly opaque, weakly opaque, and non-opaque). The proposed verification approach is based on the concept of basis marking. Thus, there does not exist any requirement to exhaustively enumerate the whole reachability set, which is an important advancement in terms of computational efficiency. In addition to that, the proposed MBRG is exploited to address LBO enforcement, where a new enforcement technique using an embedded insertion function is provided. This technique modifies the observations that reveal secret information with respect to the original language of a system. The provided embedded insertion function is more powerful for enforcing opacity than the earlier proposed ones as it considers additional enforcement cases that are not previously considered in the formerly documented approaches. A verification algorithm for enforceablity is introduced to check whether a system is enforceable or not. Finally, once a system is proved to be enforceable, an algorithm is reported to construct an insertion automaton (IA) that synthesizes all the possible insertion functions.

The remainder of the paper is organized as follows. Some necessary concepts are recalled in Section PRELIMINARIES. The proposed MBRG is shown in Section LANGUAGE-BASED OPACITY VERIFICATION APPROACH. In Section LANGUAGE-BASED OPACITY ENFORCEMENT APPROACH, based on the proposed graph, a new insertion function technique is proposed to address the enforcement of a verified non-opaque system. Conclusions are reached in Section CONCLUSION, where the future work is outlined.

Preliminaries

Petri Net

A Petri net is a four-tuple $N = (P, T, P r e, P o s t)$ , where P is a finite set of m places, graphically represented by circles; T is a finite set of n transitions, graphically represented by bars; $P r e : P \times T \to N$ and $P o s t : T \times P \to N$ are the pre- and post-incidence functions that respectively specify the arcs directed from places to transitions and vice versa. The pre- (post-) incidence function $P r e$ $(P o s t)$ can be represented by a matrix indexed by P and T. $C = P o s t - P r e$ represents the incidence matrix of the net.

A marking is a mapping $M : P \to N$ that presents the number of tokens in a place at a state; graphically a token is drawn by a black dot. The marking of a place p is denoted by $M (p)$ . For economy of space, the multi-set notation is used, i.e., we use $M = Σ_{p \in P} M (p) \cdot p$ to denote a marking M.

A Petri net system $⟨ N, M_{0} ⟩$ is a net N equipped with an initial marking $M_{0}$ . A transition t is enabled at a marking M if $M \geq P r e (\cdot, t)$ . The firing of t at M yields a new marking $M^{'}$ , satisfying $M^{'} = M + C (\cdot, t)$ . We write $M [t ⟩$ to denote that t is enabled at M and $M [t ⟩ M^{'}$ to denote that the firing of t drives a system from M to $M^{'}$ .

$M [σ ⟩$ denotes that a sequence of transitions $σ = t_{1} \dots t_{i} \in T^{*}$ is sequentially enabled at a given marking M such that $M [t_{1} ⟩ M_{1} [t_{2} ⟩ M_{2} \dots [t_{i} ⟩ M_{i}$ holds, written as $M [σ ⟩ M_{i}$ . The set of all firable (feasible) transition sequences in $⟨ N, M_{0} ⟩$ is denoted as $L (N, M_{0}) = {σ \in T^{*} |$ $M_{0} [σ ⟩}$ . The set of all the prefixes of a sequence $σ \in L (N, M_{0})$ , denoted as $\bar{σ}$ , is defined as $\bar{σ} = {σ^{'} \in T^{*} | \exists σ ″ \in T^{*}, σ = σ^{'} σ ″}$ . The prefix-closure of $L (N, M_{0})$ , denoted as $\bar{L (N, M_{0})}$ , is defined as $\bar{L (N, M_{0})} = \underset{σ \in L (N, M_{0})}{\cup} \bar{σ}$ . Given a transition sequence $σ \in T^{*}$ , function $τ : T^{*} \to N^{n}$ defines the firing count vector of the transition sequence $σ$ , i.e., $τ (σ) \in N^{n}$ , where $τ (σ) = y$ with $y (t) = k$ representing that the number of occurrences of t in $σ$ is k.

A marking M is said to be reachable in $⟨ N, M_{0} ⟩$ if there exists a transition sequence $σ \in T^{*}$ such that $M_{0} [σ ⟩ M$ . The reachability set of $⟨ N, M_{0} ⟩$ , denoted by $R (N, M_{0})$ , contains all markings of the net system reachable from $M_{0}$ . If $M_{0} [σ ⟩ M$ , then the state equation of the net is $M = M_{0} + C \cdot y$ , where $y = τ (σ)$ .

Labeled Petri Net

$A$ $l a b e l e d$ Petri net (LPN) is a four-tuple $G = (N, M_{0}, E, λ)$ , where $⟨ N, M_{0} ⟩$ is a net system, E is an alphabet, and $λ : T \to E$ is a labeling function that assigns an event from E to a transition $t \in T$ . The extended labeling function $λ : T^{*} \to E^{*}$ is defined as follows: $λ (σ t) = λ (σ) λ (t)$ , where $σ \in T^{*}$ and $t \in T$ .

Taking into account the partially observed behavior of a system, the set E is partitioned into two disjoint parts: namely $E_{o}$ and $E_{u}$ , representing the observable and unobservable events, respectively. As a result, T is accordingly divided into two disjoint sets $T = T_{o} \cup T_{u}$ , where $T_{o} = {t \in T | λ (t) \in E_{o}}$ is the set of observable transitions, while $T_{u} = T ∖ T_{o} = {t \in T | λ (t) \in E_{u}}$ is the set of unobservable transitions, called also $s i l e n t$ transitions.

Given an event $e \in E$ , its observation is the output of a natural projection function $P r : E \to E_{o}$ , where $P r (e) = e$ if $e \in E_{o}$ and $P r (e) = ε$ otherwise. The natural projection $P r$ can be in an usual manner extended to $P r : E^{*} \to E_{o}^{*}$ , which is recursively defined as $P r (ω e) = P r (ω) P r (e)$ , where $ω \in E^{*}$ and $e \in E$ . $P r$ can also be extended to $P r : 2^{E^{*}} \to 2^{E_{o}^{*}}$ , i.e., for $L \subseteq E^{*}$ , $P r (L) = {P r (ω) \in E_{o}^{*} | ω \in L}$ . The inverse project of $P r$ , denoted by $P r^{- 1}$ , can be accordingly defined by its primary and extended versions.

The language generated by an LPN system $G = (N, M_{0}, E, λ)$ from $M_{0}$ that defines its behavior is given by

\begin{matrix} L (G, M_{0}) = {ω \in E^{*} | \exists σ \in T^{*} : M_{0} [σ ⟩, λ (σ) = ω} \end{matrix}

(1)

The set of all the prefixes of a string

s \in L (G, M_{0})

, denoted as

\bar{s}

, is defined as

\begin{matrix} \bar{s} = {u \in E^{*} | \exists v \in E^{*}, s = u v} \end{matrix}

(2)

The prefix-closure of

L (G, M_{0})

, denoted by

\bar{L (G, M_{0})}

, is defined as

\begin{matrix} \bar{L (G, M_{0})} = \underset{s \in L (G, M_{0})}{\cup \bar{s}} \end{matrix}

(3)

The set

\bar{L (G, M_{0})}

consists of all the prefixes of all the strings in

L (G, M_{0})

. Note that, as usual, we use

| \cdot |

to denote the cardinality of a set.

Basis reachability graph

An observer for a net system, called a basis reachability graph (BRG), is first introduced in²⁴. A generalization of BRG is later introduced in²⁵ to provide a more basic structure, containing basis markings only, regardless of the system's observability, to deal with more general reachability problems.

Definition 1 (Basis Partition²⁵):

Given a Petri net $N = (P, T, P r e, P o s t),$ a pair $π = (T_{E}, T_{I})$ is called a basis partition of T if $T_{I} \subseteq T$ , $T_{E} = T ∖ T_{I}$ , and the $T_{I}$ -induced subnet is acyclic.

$T_{E}$ and $T_{I}$ represent the explicit and implicit transition sets, respectively. In simple words, $π$ divides T into two disjoint sets $T_{E}$ and $T_{I}$ such that the $T_{I}$ -induced subnet is acyclic .

Definition 2 (Explanations²⁵):

Given a Petri net $N = (P, T, P r e, P o s t)$ , a basis partition $π = (T_{E}, T_{I})$ , a marking $M$ , and a transition $t \in T_{E}$ , the set of $e x p l a n a t i o n s$ of t at M is defined as

\begin{matrix} Σ (M, t) = {σ \in T_{I}^{*} | M_{0} [σ ⟩ M^{'}, M^{'} \geq P r e (\cdot, t)} \end{matrix}

(4)

In other words, the firing of any implicit transition sequence $σ \in Σ (M, t)$ leads the system to a new marking at which an explicit transition t is enabled. Let $n_{I} = | T_{I} |$ . The set of e - $v e c t o r s$ (explanation vectors), representing the firing vectors associated with the sequences in $Σ (M, t)$ , is defined as $Y (M, t) = {y_{σ} \in N^{n_{I}} | σ \in Σ (M, t) : y_{σ} = τ (σ)}$ .

Definition 3 (Minimal Explanations²⁵):

Given a Petri net $N = (P, T, P r e, P o s t)$ , a basis partition $π = (T_{E}, T_{I})$ , a marking $M$ , and an explicit transition $t \in T_{E}$ , the set of $m i n i m a l$ $e x p l a n a t i o n s$ of t at M is defined as

\begin{matrix} Σ_{m i n} (M, t) = {σ \in Σ (M, t) | ⧸ \exists σ^{'} \in Σ (M, t) : y_{σ^{'}} \leq y_{σ}} \end{matrix}

(5)

and the corresponding set of

m i n i m a l

e

v e c t o r s

is defined by

Y_{m i n} (M, t) = {y_{σ} \in N^{n_{I}} | σ \in Σ_{m i n} (M, t) : y_{σ} = τ (σ)} .

Definition 4 (Basis Marking²⁵):

Given a Petri net $N = (P, T, P r e, P o s t)$ with initial marking $M_{0}$ and a basis partition $π = (T_{E}, T_{I})$ , the set of its basis markings $M$ is a subset of $R (N, M_{0})$ such that:

$M_{0} \in M$ ;

If $M \in M$ , then for all $t \in T_{E}$ , for all $y_{I} \in Y_{m i n} (M, t)$ , it holds $M^{'} \in M$ , where $M^{'} = M + C_{I} \cdot y_{I} + C (\cdot, t)$ .

Note that $C_{I}$ is the incidence matrix of the subnet derived from $T_{I}$ . A marking $M \in M$ is called a basis marking with respect to $π = (T_{E}, T_{I})$ .

Definition 5 (Basis Reachability Graph²⁵):

Given a Petri net $N = (P, T, P r e, P o s t)$ with initial marking $M_{0}$ and a basis partition $π = (T_{E}, T_{I})$ , its basis reachability graph (BRG) is a non-deterministic finite state automaton $B = (M, T_{r}, Δ, M_{0})$ , where:

the state set $M$ is the set of basis markings;

the event set $T_{r}$ is the set of pairs $(t, y_{I}) \in T_{E} \times N^{n_{I}}$ ;

the transition relation $Δ \subseteq M \times T_{r} \times M$ is defined as: $Δ = {(M, (t, y_{I}), M^{'}) | t \in T_{E}, y_{I} \in Y_{m i n} (M, t), M^{'} = M + C_{I} \cdot y_{I} + C (\cdot, t)}$

the initial marking $M_{0}$ of Petri net N is the initial state.

Language-based opacity

The definition of LBO of DESs is initially formulated based on automata⁶ and then consistently extended to the Petri net framework¹⁷, where a secret is represented as a set of transition sequences. However, in this work, the secret is defined as a set of sequences of events (labels) consistent with what is usually suggested in the context of automaton.

Definition 6 (Language-based Opacity²⁶):

Given an LPN $G = (N, M_{0}, E, λ)$ , a natural projection $P r$ , and secret language $L_{S} \subseteq L (G, M_{0})$ , $G$ is said to be language-opaque if for all $ω \in L_{S}$ , there exists $ω^{'} \in L (G, M_{0}) ∖ L_{S}$ such that $P r (ω) = P r (ω^{'})$ .

Definition 7 (Language Opacity Properties⁷):

Given an LPN $G = (N, M_{0}, E, λ)$ and two disjoint languages $L_{S}$ (secret), $L_{N S}$ (non-secret) $\subseteq L (G, M_{0})$ , $G$ is said to be:

Strongly opaque if $L_{S} \subseteq P r^{- 1} [P r (L_{N S})]$ .

Weakly opaque if $L_{S} \cap P r^{- 1} [P r (L_{N S})] \neq \emptyset$ .

Non-opaque if $L_{S} \cap P r^{- 1} [P r (L_{N S})] = \emptyset$ .

In other words, by Definition 7, $G$ is strongly opaque with respect to $P r$ if every string in $L_{S}$ is confused with at least one string in $L_{N S}$ ; $G$ is weakly opaque if some strings in $L_{S}$ are confused with some strings in $L_{N S}$ under $P r$ ; and $G$ is non-opaque if it is neither strongly nor weakly opaque, implying that there is no string in $L_{S}$ confused with those in $L_{N S}$ . In the literature, LBO refers to the strong opacity property, which is consistent with Definition 6, i.e., $G$ is language-opaque if all strings in $L_{S}$ are confused with at least one in $L_{N S}$ .

Language-based opacity verification approach

In this section, a novel approach for LBO verification using the notions of basis partition and basis markings is presented. The idea consists in defining a new modified BRG (MBRG) to effectively check language opacity without enumerating the whole reachability set. The proposed approach deals not only with opacity verification but also opacity enforcement. To guarantee that the behavior of a system can be described by the proposed graph, the set of observable transitions $T_{o}$ is supposed to be included in $T_{E}$ . The set of unobservable transitions, which are contained in the transition sequences representing the secret words, is formally defined as ${\hat{T}}_{u} = {t \in T_{u} | \exists ω \in L_{S}, λ (σ) = ω, σ \in L (N, M_{0}), t \in t σ^{2}}$ . We also propose that ${\hat{T}}_{u}$ is included in the set $T_{E}$ . ${\hat{T}}_{u} \subseteq T_{E}$ is assumed to treat a particular case where unobservable transitions can make a system opaque. More precisely, for an unobservable transition t from the transition sequences representing the secret words, the existence of a non-null e-vector is sufficient to make a system opaque. Thus, the equation $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ holds.

In this paper, the transition set of a Petri net is partitioned into explicit and implicit transitions instead of observable and unobservable events. This partition is proposed to avoid being restricted by a system’s structure. Thus, the chosen partition allows the proposed approach to be widely applied to any Petri net structure, regardless of its observation. The chosen basis partition helps then to apply easily our approach to a wide range of Petri nets while conserving the system's observation since the set of observable transitions $T_{o}$ is supposed to be included in $T_{E}$ . The chosen basis partition assists also to check opacity deeply since some secret words could be opaque through unobservable transitions, which is why we assumed to include ${\hat{T}}_{u}$ in $T_{E}$ . The proposed method is achieved under the following assumption:

A1) The subnet derived from $T_{I}$ of $G$ is acyclic.

The use of the generalized BRG makes A1 negligible compared with the assumption used in¹⁷ and¹⁸, where the unobservable transition subnet requires to be acyclic. The acyclicity assumption in¹⁷ and¹⁸ is related to the structure of the system, while the acyclicity assumption made in this paper is not based on the structure of a system but on the chosen basis partition. Therefore, our proposed approach can be applied to a wide range of net systems, where the unobservable subnet is cyclic.

Verification of language-based opacity

Let $G = (N, M_{0}, E, λ)$ be an LPN, $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ be a basis partition, and $L_{S}$ be a secret language. Note that $L_{S}$ can contain different elements with the same observation. Therefore, the set of explicit transition sequences corresponding to secret words that generate the same observation $η$ under the natural projection $P r$ is defined as

\begin{matrix} L (η) = {σ \in T_{E}^{*} | M_{0} [σ ⟩, λ (σ) = ω \in L_{S}, P r (ω) = η} . \end{matrix}

(6)

In addition, the set of explicit transition sequences possessing an observation

η

with respect to

L_{S}

under

P r

is defined as

\begin{matrix} Γ (η) = {σ \in T_{E}^{*} | M_{0} [σ ⟩, \exists ω \in L_{S}, λ (σ) = ω^{'}, P r (ω) = P r (ω^{'}) = η} . \end{matrix}

(7)

The set

Γ (η)

contains the explicit transition sequences generating an observation

η

as a given secret word

ω \in L_{S}

, i.e.,

P r (ω) = η

, including the explicit transition sequences that represent secret words and generate

η

under the natural projection

P r

Proposition 1

Given an LPN $G = (N, M_{0}, E, λ)$ , a basis partition $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , and a finite secret language $L_{S}$ , $G$ is language-opaque if for all $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , there exists $σ^{'} \in T_{E}^{*}$ , with $λ (σ^{'}) = ω^{'} \in L_{N S} = L (G, M_{0}) ∖ L_{S}$ and $M_{0} [σ^{'} ⟩$ , such that $P r (ω) = P r (ω^{'})$ .

Proof

By Definition 6, an opaque system means that for all $ω \in L_{S}$ , one can find a string $ω^{'} \in L_{N S}$ such that $P r (ω) = P r (ω^{'})$ . Let $S = {σ \in L (N, M_{0}) | \exists ω \in L_{S}, λ (σ) = ω}$ be the set of transition sequences representing the secret language. By defining the secret language as a transition sequences set, a system is opaque if for all $σ \in S$ , one can find a transition sequence $σ^{'} \in L (N, M_{0}) ∖ S$ such that $P r (λ (σ)) = P r (λ (σ^{'}))$ . Thanks to $T_{E}^{*} \subseteq T^{*}$ , consistent with Definition 3.1 in¹⁷, a system is language opaque if for all $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , there exists $σ^{'} \in T_{E}^{*}$ , with $λ (σ^{'}) = ω^{'} \in L_{N S}$ and $M_{0} [σ^{'} ⟩$ , such that $P r (ω) = P r (ω^{'})$ .

Proposition 2

Given an LPN $G = (N, M_{0}, E, λ)$ , its BRG under a basis partition $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , and a finite secret language $L_{S}$ , if for all $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , there exist $t \in σ$ , $σ ″ \in \bar{σ}$ , and $M \in M$ such that $M_{0} [σ ″ ⟩ M$ and $Y (M, t) \neq {\vec{0}}$ , then $G$ is language-opaque.

Proof

Suppose that for all $σ \in T_{E}^{*}$ with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , there exist $t \in σ$ , $σ ″ \in \bar{σ}$ , and $M \in M$ such that $M_{0} [σ ″ ⟩ M$ and $Y (M, t) \neq {\vec{0}}$ . Thus, for all $σ \in T_{E}^{*}$ with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , there exists an e-vector $y_{I} \in Y (M, t)$ , with $y_{I} \neq \vec{0}$ , such that one can find an explanation $σ_{I} \in Σ (M, t)$ whose firing at M enables t, where $τ (σ_{I}) = y_{I}$ . This implies that there exist a sequence $σ_{I} \in T_{I}^{*}$ and a marking $M^{'} \in R (N, M_{0})$ such that $M [σ_{I} ⟩ M^{'} [t ⟩$ . Hence, for all $σ \in T_{E}^{*}$ with $λ (σ) = ω \in L_{S}$ and $M_{0} [σ ⟩$ , one can find a sequence $σ^{'} \in T^{*}$ satisfying $λ (σ^{'}) = ω^{'} \in L_{N S}$ , $σ \neq σ^{'}$ (i.e. $σ_{I} \in σ^{'}$ and $σ_{I} \notin σ$ )¹, and $P r (ω) = P r (ω^{'})$ . By Definition 6, $G$ is language-opaque.

Example 1

We consider the LPN in Figure 1, where $T_{o} = {t_{1}}$ and $T_{u} = {t_{2}, t_{3}}$ . Let $L_{S} = {b}$ be a secret language, where b is the corresponding observation of $t_{1}$ . According to Proposition 2, we have $\bar{t_{1}} = {ε, t_{1}}$ , $M_{0} [ε M_{0}$ . At $M_{0} = p_{1} + p_{2}$ , the transition $t_{1}$ could be firable. The set of explanations of $t_{1}$ is $Σ (M_{0}, t_{1}) = {ε, t_{2}, t_{2} t_{3}}$ and $Y (M_{0}, t_{1}) = {\vec{0}, {[10]}^{T}, {[11]}^{T}}$ . Since $Y (M_{0}, t_{1}) \neq {\vec{0}}$ , there exists at least a transition sequence $t_{2} t_{1}$ such that $λ (t_{2} t_{1}) = d b \in L_{N S}$ and $P r (d b) = P r (b) = b$ . Thus, the LPN is opaque.

The condition in Proposition 1 is sufficient to check the opacity of a system. However, if not satisfied, we cannot conclude that a system is non-opaque. Hence, Proposition 2 presents another sufficient condition to decide the opacity of a system when Propositions 1 is not satisfied.

Figure 1.

A Labeled Petri net.

Theorem 1

Given an LPN $G = (N, M_{0}, E, λ)$ , its BRG under a basis partition $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , and a finite secret language $L_{S}$ , $G$ is language-opaque if for all $σ \in T_{E}^{*}$ satisfying $λ (σ) = ω \in L_{S}$ , $| Γ (P r (ω)) | > | L (P r (ω)) |$ holds or there exist a transition $t \in σ$ , a sequence $σ ″ \in \bar{σ}$ , and a basis marking $M \in M$ such that $M_{0} [σ ″ ⟩ M$ holds and the following integer programming problem (IPP) admits a feasible solution:

\begin{aligned} M i n i m i z e : \vec{1} \cdot \vec{y_{I}} \\ S u b j e c t e d t o : \\ \begin{matrix} M - P r e (\cdot, t) + C_{I} \cdot y_{I} \geq 0 \end{matrix} \\ y_{I} \in N^{n_{I}} \\ y_{I} > \vec{0} \end{aligned}

(8)

Proof

Let us suppose that for all $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ , either $| Γ (P r (ω)) | > | L (P r (ω)) |$ holds or there exist $t \in σ$ , $σ ″ \in σ$ and $M \in M$ such that $M_{0} [σ ″ ⟩ M$ holds and IPP (8) has a feasible solution. According to Equations (6) and (7), if there exists $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ such that $| Γ (P r (ω)) | > | L (P r (ω)) |$ , then there exists $σ^{'} \in T_{E}^{*}$ satisfying $λ (σ^{'}) = ω^{'} \notin L_{S}$ and generating the same observation $P r (ω)$ as $ω$ . In addition, if there exists $σ \in T_{E}^{*}$ such that $λ (σ) = ω \in L_{S}$ and there exist $t \in σ$ , $σ ″ \in \bar{σ}$ , and $M \in M$ in which $M_{0} [σ ″ ⟩ M$ holds and IPP (8) has a feasible solution, then there exists $y_{I} \in Y (M, t)$ with $y_{I} \neq \vec{0}$ , which implies that there exist $σ_{I} \in Σ (M, t)$ and $M^{'} \in M$ verifying $τ (σ_{I}) = y_{I}$ and satisfying $M [σ_{I} ⟩ M^{'} [t ⟩$ . Thus, one can find $σ^{'} \in T^{*}$ such that $λ (σ^{'}) = ω^{'} \in L_{N S}$ and $P r (ω) = P r (ω^{'})$ . Consequently, if for all $σ \in T_{E}^{*}$ , with $λ (σ) = ω \in L_{S}$ , either $| Γ (P r (ω)) | > | L (P r (ω)) |$ holds or there exist $t \in σ$ , $σ ″ \in \bar{σ}$ , and $M \in M$ such that $M_{0} [σ ″ ⟩ M$ holds and IPP (8) has a feasible solution, then $G$ is opaque.

In order to guarantee the opacity of a net system $G$ , it is necessary to find in $G$ a transition sequence different from the transition sequences representing the secret words but having the same observation. Theorem 1 provides a sufficient condition to verify the opacity of a system by studying the observable and unobservable transitions in hiding the secret.

Modified basis reachability graph (MBRG)

To verify different properties of LBO, a modified BRG (MBRG) is proposed. We assume that an LPN is bounded to guarantee that its MBRG is finite. Given an LPN $G = (N, M_{0}, E, λ)$ and a basis partition $π = (T_{E}, T_{I})$ , with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , the set of basis markings reachable, from the initial marking $M_{0}$ , by firing a transition sequence $σ \in T_{E}^{*}$ that generates a secret word $ω \in L_{S}$ is defined as

\begin{matrix} \bar{M} = {M \in M | \exists ω \in L_{S}, \exists σ \in T_{E}^{*}, λ (σ) = ω, M_{0} [σ ⟩ M} \end{matrix}

(9)

Definition 8 (Misleading marking):

Let $G$ $= (N$ , $M_{0}$ , $E$ , $λ)$ be an LPN and $L_{S}$ a secret language. A marking $M \in \bar{M}$ is said to be $m i s l e a d i n g$ if for all $ω \in L_{S}$ , with $λ (σ) = ω$ , $σ \in T_{E}^{*}$ , and $M_{0} [σ ⟩ M$ , either $| Γ (P r (ω)) | > | L (P r (ω)) |$ or there exist $t \in σ$ , $σ ″ \in \bar{σ}$ , and $M^{'} \in M$ such that $M_{0} [σ ″ ⟩ M^{'}$ holds and IPP (8) has a feasible solution.

Based on Definition 8, given an LPN $G = (N, M_{0}, E, λ)$ and a finite secret language $L_{S}$ , for all, $M \in \bar{M},$ a $b i n a r y$ $s c a l a r$ $α (M)$ is defined as follows:

α (M) = {\begin{matrix} 1, & i f M i s m i s l e a d i n g; \\ 0, & o t h e r w i s e \end{matrix}

(10)

Based on the concept of binary scalar, basis marking and basis partition, a modified BRG (MBRG) graph is defined.

Definition 9 (MBRG):

Given an LPN $G = (N, M_{0}, E, λ)$ and a basis partition $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , its modified BRG (MBRG) is a non-deterministic finite automata (NFA) $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ , where

the state set ${\ddot{M}}_{B} = \tilde{M} \cup \overset{˘}{M}$ is the set of modified basis markings with

$\tilde{M} = {(M, - 1) | M \in M ∖ \bar{M}}$ being the set of unselected basis markings .

$\overset{˘}{M} = {(M, α (M)) | M \in \bar{M}}$ being the set of selected basis markings.

the set E is the set of events.

the transition relation $δ \subseteq {\ddot{M}}_{B} \times E \times {\ddot{M}}_{B}$ is defined as:

δ = {(M, λ (t), M^{'}) | t \in T_{E}, y_{I} \in Y_{m i n} (M, t), M^{'} = M + C_{I} \cdot y_{I} + C (\cdot, t)}

${\ddot{M}}_{B_{0}}$ is the initial state, where ${\ddot{M}}_{B_{0}} = (M_{0}, - 1)$ if $M_{0} \in M ∖ \bar{M}$ ; otherwise ${\ddot{M}}_{B_{0}} = (M_{0}, α (M_{0}))$ if $M_{0} \in \bar{M}$ .

In plain words, the set of modified basis markings of $β$ is divided into two disjoint subsets: unselected basis markings and selected basis markings. The unselected basis marking set represents the states that are composed by the basis markings reachable by firing transition sequences generating non-secret words and the integer $- 1$ . However, a selected basis marking is represented by a pair of elements that are the marking reachable by firing a transition sequence generating a secret word and its associated binary scalar. Note that the transition relation $δ$ can be as usual extended to $δ \subseteq {\ddot{M}}_{B} \times E^{*} \times {\ddot{M}}_{B}$ .

Definition 10 (MBRG Generated Language):

The language generated by an MBRG $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ from its initial state ${\ddot{M}}_{B_{0}}$ is defined as

\begin{matrix} L (β, {\ddot{M}}_{B_{0}}) = {ω \in E^{*} | δ ({\ddot{M}}_{B_{0}}, ω)!} \end{matrix}

(11)

The procedure of constructing MBRG is summarized in Algorithm 1. First, $x_{0}$ is initialized to be the initial state of the system. Different sets are then initially marked as an empty set. However, state $x_{0}$ is added to the set of unchecked states $M_{N e w}$ . While the set of unchecked states $M_{N e w}$ is not empty, a state x from $M_{N e w}$ is selected and its associated marking is considered. Steps 3–14 show the computation of the basis marking set by finding the minimum e-vectors feasible at each marking from $M_{N e w}$ . Once the set $M_{N e w}$ is empty, we need to distinguish the set of markings reachable by firing the transition sequences representing the secret words. Hence, the computation of $\bar{M}$ according to Equation (9) is done. The initial marking of the MBRG is then initialized based on the initial marking $M_{0}$ and added to the set ${\ddot{M}}_{B}$ . After that, $M := M ∖ {M_{0}}$ is done and for all basis markings $M \in M$ , if $M \in M ∖ \bar{M}$ , then a composed pair $(M, - 1)$ is added to the set $\tilde{M}$ . Once $M \notin M ∖ \bar{M}$ , the binary scalar of M is computed according to Equation (10), i.e., $α (M)$ , and the pair $(M, α (M))$ is added to the set . At the end, the set of markings of $β$ is (Steps 15 to 32).

The construction of an MBRG avoids the exhaustive enumeration to the whole reachability set. The computation of $α (M)$ is required when constructing an MBRG, where an integer programming problem should be solved since we exploit unobservabe transitions to hide secret information. An integer-programming problem is NP-Complete, but the computation burden here is lowered since this method reduces the number of constraints and variables.

Theorem 2:

Given an LPN $G = (N, M_{0}, E, λ)$ , a basis partition $π = (T_{E}, T_{I})$ with $T_{o} \cup {\hat{T}}_{u} \subseteq T_{E}$ , and a finite secret language $L_{S}$ , let $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ be the associated MBRG and $M, M^{'} \in M$ be basis markings. Then, $G$ is:

(i) Strongly opaque if and only if there does not exist ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ such that ${\ddot{M}}_{B} = (M, 0)$ .

(ii) Non-opaque if and only if there does not exist ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ such that ${\ddot{M}}_{B} = (M, 1)$ .

(iii) Weakly opaque if and only if there exists ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ such that ${\ddot{M}}_{B} = (M, 1)$ .

Proof

Let $L_{S}$ be a secret language and $ω \in L_{S}$ a secret word.

(If) The fact that a system is not strongly opaque means that it is either non-opaque or weakly opaque. Suppose that $G$ is non-opaque. By Definition 7, a non-opaque system means that for all $ω \in L_{S}$ , there does not exist any $ω^{'} \in L_{N S}$ such that $P r (ω) = P r (ω^{'})$ . Based on the MBRG construction given in Algorithm 1 and Eq. (10), this means that for any state ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ that satisfies $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ there exists a basis marking $M \in M$ such that ${\ddot{M}}_{B} = (M, 0)$ holds. Let us now suppose that $G$ is weakly opaque. By Definition 7, a weakly opaque system means that there exists at least one secret word $ω \in L_{S}$ such that one cannot find any $ω^{'} \in L_{N S}$ verifying $P r (ω) = P r (ω^{'})$ . Based on the MBRG construction given in Algorithm 1 and Equation (10), this means that there exists a state ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ and a basis marking $M \in M$ such that $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and ${\ddot{M}}_{B} = (M, 0)$ .

(Only if) First by contrapositive, let us suppose that there exist at least one ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ and $M \in M$ such that ${\ddot{M}}_{B} = (M, 0)$ . Thus, based on MBRG construction, there exists at least one secret word $ω \in L_{S}$ such that $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ . By Equation (10), ${\ddot{M}}_{B} = (M, 0)$ implies that M is a non-misleading marking. Thus, according to Definition 8, $| Γ (P r (ω)) | = | L (P r (ω)) |$ holds and for all $t \in σ$ with $σ \in T_{E}^{*}$ and $λ (σ) = ω$ , the IPP (8) does not have a feasible solution. By Equations (6) and (7), $| Γ (P r (ω)) | = | L (P r (ω)) |$ means that there does not exist any $σ^{'} \in T_{E}^{*}$ that satisfies $λ (σ^{'}) = ω^{'} \in L_{N S}$ and $P r (ω) = P r (ω^{'})$ . Thus, by Definition 7, $G$ is weakly opaque. In addition, for all $t \in σ$ with $σ \in T_{E}^{*}$ and $λ (σ) = ω$ , the fact that the IPP (8) does not have a feasible solution means that there does not exist any $y_{I} \in Y (M, t)$ verifying $y_{I} \neq \vec{0}$ , which implies that there does not exist any $σ_{I} \in Σ (M, t)$ verifying $τ (σ_{I}) = y_{I}$ and satisfying $M [σ_{I} ⟩ M^{'} [t ⟩$ . Thus, there does not exist any $σ^{'} \in T^{*}$ such that $λ (σ^{'}) = ω^{'} \in L_{N S}$ and $P r (ω) = P r (ω^{'})$ . As a result, by Definition 7, $G$ is weakly opaque.

Second, let us now suppose that for all ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ that satisfies $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and $ω \in L_{S}$ , there exists a basis marking $M \in M$ such that ${\ddot{M}}_{B} = (M, 0)$ . By following the same way and according to the MBRG construction, this means that for all $ω \in L_{S}$ , one cannot find a non-secret word $ω^{'} \in L_{N S}$ verifying $P r (ω) = P r (ω^{'})$ . By Definition 7, $G$ is non-opaque.

In summary, we conclude that $G$ is either weakly opaque if there exist at least a state ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ and basis marking $M \in M$ such that ${\ddot{M}}_{B} = (M, 0)$ or non-opaque if for all ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ that satisfies $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and $ω \in L_{S}$ , there exists a basis marking $M \in M$ such that ${\ddot{M}}_{B} = (M, 0)$ . In other words, $G$ is strongly opaque if there does not exist any $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ such that ${\ddot{M}}_{B} = (M, 0)$ , in which M is a basis marking.

(If) Since there do not exist any state ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ and a basis marking $M \in M$ such that ${\ddot{M}}_{B} = (M, 1)$ , according to the MBRG, construction for all $ω \in L_{S}$ satisfying $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ , one cannot find a non-secret word $ω^{'} \in L_{N S}$ such that $δ ({\ddot{M}}_{B_{0}}, ω^{'})!$ and $P r (ω) = P r (ω^{'})$ , where $δ ({\ddot{M}}_{B_{0}}, ω^{'})!$ means that it is defined. Hence, by Definition 7, $G$ is non-opaque.

(Only if) The fact that a system is non-opaque means that for all $ω \in L_{S}$ , there does not exist any $ω^{'} \in L_{N S}$ such that $P r (ω) = P r (ω^{'})$ . By Equations (6) and (7), this means that for all $ω \in L_{S}$ , $| Γ (P r (ω)) | = | L (P r (ω)) |$ holds and for all $t \in σ$ with $σ \in T_{E}^{*}$ and $λ (σ) = ω$ , the IPP (8) does not have a feasible solution. Based on the MBRG construction and Eq (10), for all ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ satisfying $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ , ${\ddot{M}}_{B} = (M, 0)$ holds. The other states of MBRG represent the set of unselected markings. Hence, for all ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ , we have either ${\ddot{M}}_{B} = (M, 0)$ or ${\ddot{M}}_{B} = (M, - 1)$ .

(If) Since there exists ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ satisfying ${\ddot{M}}_{B} = (M, 1)$ in which M represents a basis markings, by Equation (10), the marking M is misleading. According to the MBRG construction, there exists $ω \in L_{S}$ that verifies $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ such that one can find $ω^{'} \in L_{N S}$ in which $P r (ω^{'}) = P r (ω)$ holds. By Definition 7, $G$ is weakly opaque.

(Only if) The fact that a system is weakly opaque means that there exists $ω \in L_{S}$ such that one can find $ω^{'} \in L_{N S}$ satisfying $P r (ω^{'}) = P r (ω)$ . Based on the proposed MBRG, this means that there exists ${\ddot{M}}_{B} \in {\ddot{M}}_{B}$ satisfying $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ such that ${\ddot{M}}_{B} = (M, 1)$ , where the marking $M \in M$ is a basis marking.

Example 2.

Consider the LPN system $G$ in Figure 2. Let $T_{o} = {t_{1}, t_{3}, t_{4}, t_{6}, t_{8}}$ be the observable transitions, $T_{u} = {t_{2}, t_{5}, t_{7}}$ be the unobservable transitions, $E_{o} = {b, c}$ be the observable events, $E_{u} = {a, d}$ be the unobservable events, and $L_{S} = {b a c, b a b}$ be the secret language, in which $b a c$ and $b a b$ are the generated strings corresponding to $t_{1} t_{2} t_{8}$ and $t_{1} t_{2} t_{3}$ , respectively. According to the proposed basis partition $π = (T_{E}, T_{I})$ , we have $T_{E} = T_{o} \cup {\hat{T}}_{u} = {t_{1}, t_{2}, t_{3}, t_{4}, t_{6}, t_{8}}$ and $T_{I} = {t_{5}, t_{7}}$ . The transition $t_{2}$ is an unobservable transition that belongs to $T_{E}$ since it is contained in the transition sequences that represent the secret. However, $t_{5}$ and $t_{7}$ are not contained in any transition sequence representing a secret word. The resulting MBRG construction, with respect to $π$ , is shown in Figure 3. The secret language observation under the natural projection is $P r (L_{S}) = {b c, b b}$ . Note that the secret language elements are arbitrary. Based on the MBRG in Figure 3 and by Eq. (7), we have two sets: $Γ (b c) = {t_{1} t_{2} t_{8}}$ and $Γ (b b) = {t_{1} t_{2} t_{3}, t_{4} t_{6}}$ . Thus, $| Γ (b c) | = 1$ and $| Γ (b b) | = 2$ . The selected basis markings reachable by the transition sequences representing the secret words are: $M_{0}$ and $M_{4}$ , i.e., $\bar{M} = {M_{0}, M_{4}}$ . Among the transition sequences leading to $M_{0}$ (resp., $M_{4}$ ), only one transition sequence represents a secret word. $M_{4}$ is reachable by firing a transition sequence generating the observation $b b$ corresponding to the secret $b a b$ . The cardinality of the transition sequences representing secret words from $L_{S}$ generating $b b$ is $| L (b b) | = 1$ . However, the cardinality of transition sequences generating $b b$ is $| Γ (b b) | = 2$ . Thus, $| Γ (b b) | > | L (b b) |$ and $α (M_{4}) = 1$ according to Equation (10). We conclude that $M_{4}$ is a $m i s l e a d i n g$ marking. Now, let us focus on $M_{0}$ that is reachable by firing the transition sequence generating the observation $b c$ corresponding to the secret $b a c$ . Obviously, $| Γ (b c) | = | L (b c) | = 1$ and $| Y (M_{1}, t_{1}) | = | Y (M_{3}, t_{2}) | = | Y (M_{0}, t_{8}) | = 1$ hold. Hence, according to Equation (10), $α (M_{0}) = 0$ holds and the marking $M_{0}$ is then mentioned as non-misleading. Based on Algorithm 1, the obtained MBRG is portrayed in Figure 3 and according to Theorem 2, the system is weakly opaque.

Language-based opacity enforcement approach

In this section, we propose a new enforcement strategy for LBO that takes the advantages of the proposed MBRG. The proposed strategy is inspired by the insertion function technique proposed in.²⁰ and²² The insertion function inserts additional dummy events to the event sequences that reveal a secret in order to mislead the intruder and establish the opacity of a system.

Figure 2.

An LPN $G$ .

Figure 3.

The MBRG of the LPN in Figure 2.

In this paper, the proposed strategy is presented in the context of PNs unlike the strategies in²⁰ and²² that are established in the context of automaton framework. As the same as the one proposed in,²² the insertion function here is embedded into the structure of a system, while the one proposed in²⁰ is a run-time monitoring interface at the output of a system. Here, similar to the insertion function proposed in,²³ the embedded function inserts not only additional events before an observable event, but also inserts an additional event after an observable event, in which the additional event could be either an observable event or $ε$ . Finally, the proposed insertion function is more general and more powerful for enforcing opacity as it addresses further enforcement cases that the previously proposed insertion functions had not been considered.

Example 3.

Consider the net system $G$ in Figure 4, where $E_{o}$ = ${a, b, c}$ , $E_{u}$ = ${d}$ and accordingly $T_{o} = {t_{1}, t_{3}, t_{4}, t_{5}, t_{6}, t_{7}, t_{8}, t_{10}, t_{11}, t_{12}}$ and $T_{u} = {t_{2}, t_{9}}$ . Let $L_{S} = {d c}$ be a secret language, where $d c$ is the corresponding string of $t_{9} t_{10}$ . Thus, based on the proposed basis partition, $T_{E} = {t_{1}, t_{3}, t_{4}, t_{5}, t_{6}, t_{7}, t_{8}, t_{9}, t_{10}, t_{11}, t_{12}}$ and $T_{I} = {t_{2}}$ hold. The corresponding MBRG is given in Figure 5. By mapping the secret event sequences to secret markings (states), the set of secret states is $S = {{\ddot{M}}_{B_{6}}}$ . In this example, the insertion mechanisms introduced in and are inadequate. Indeed, at state ${\ddot{M}}_{B_{0}}$ , the firing of d could be effected; however, this event is unobservable. Therefore, the insertion function cannot be effected. The firing of d leads to ${\ddot{M}}_{B_{3}}$ . At ${\ddot{M}}_{B_{3}}$ , the firable event is $c$ . We can insert before c either $a_{v}$ , $b_{v}$ , $c_{v}$ or $ε$ . The modified output could then be either $d a_{v} c$ , $d b_{v} c$ , $d c_{v} c$ or $d ε c$ . Let us choose $d ε c$ since there does not exist any string that has an equivalent observation to $d a_{v} c$ , $d b_{v} c$ , and $d c_{v} c$ in the system's language. As well, we can insert either $a_{v}$ , $b_{v}$ , $c_{v}$ or $ε$ after $c$ . let us choose to insert $b_{v}$ . Thus, the state estimate of $d ε c b_{v}$ is the state estimate of its observation, which is $d c b$ , i.e., $δ ({\ddot{M}}_{B_{0}}, d c b) = {\ddot{M}}_{B_{8}} \notin S$ . The secret behavior $d c$ could then be protected by $d ε c b_{v}$ since its observation is legal and equivalent to a string that does not violate the secret. Upon the occurrence of the event $c$ , the intruder observes immediately $c b$ in order to avoid its ability to infer that $d c$ has been occurred since he/she can notice that $d c$ has been fired when he/she observes c only. Hence, the enforceability property (details will be given later) is satisfied, while the system is neither i-enforceable nor e-enforceable according to works in²⁰ and,²² respectively.

Insertion function

Given a non-opaque or a weakly opaque system, we assume that an intruder is unable to distinguish the inserted events from the genuine ones. The inserted events are denoted by a virtual label $e_{v} \in E_{v}$ where $E_{v} = E_{o} \cup {ε}$ .

Figure 4.

An LPN example.

Figure 5.

MBRG of LPN in example 3.

Definition 11 (Insertion function):

For all $e_{v}, e {^{'}}_{v} \in E_{v}$ and for all $e \in E_{o}$ , an insertion function $f : E_{v} \times E_{o} \times E_{v} \to E^{*}$ is defined by

\begin{matrix} f (e_{v}, e, e {^{'}}_{v}) = e_{v} e e {^{'}}_{v} \end{matrix}

(12)

The insertion function here can insert additional virtual events $e_{v}, e {^{'}}_{v} \in E_{v}$ before and after an observable original event e. Notice that $e_{v}$ and $e {^{'}}_{v}$ can be either an observable event or $ε$ . The function f outputs an observed behavior with insertions denoted as $e_{v} e e {^{'}}_{v}$ , which implies that f inserts $e_{v}$ and $e {^{'}}_{v}$ respectively before and after e. The implementation of the proposed insertion function technique in a system can be performed according to the following assumptions:

A2) A given system $G$ is deadlock-free.

A3) The system $G$ is either non-opaque or weakly opaque.

A4) The system $G$ is enforceable (Definition will be given later).

Verification of enforceability

Compared with other existing enforcement mechanisms, an insertion function allows all the behavior of a system and does not create a new observation that does not exist in the original behavior of a system. To ensure this property, the following definitions are proposed.

Definition 12 (Valid Insertion Sequence):

Let $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ be an MBRG of an LPN $G$ = (, $M_{0}$ , $E$ , $λ)$ and $ω \in L_{S}$ be a secret word, with $ω = e_{1} \dots e_{n}$ , $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ , and ${\ddot{M}}_{B} = (M, 0)$ , where M is a basis marking. For all $e_{v}, e {^{'}}_{v} \in E_{v}$ , an insertion sequence $ω^{'} = f (e_{v}, e_{1}, e {^{'}}_{v}) \dots f (e_{v}, e_{n}, e {^{'}}_{v})$ is said to be valid if there exists $\ddot{M} {^{'}}_{B} \in {\ddot{M}}_{B}$ with $δ ({\ddot{M}}_{B_{0}}, ω^{'}) = \ddot{M} {^{'}}_{B}$ such that either $\ddot{M} {^{'}}_{B} = (M, 1)$ or $\ddot{M} {^{'}}_{B} = (M, - 1)$ holds.

In other words, an insertion sequence of a given secret word $ω \in L_{S}$ with $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and ${\ddot{M}}_{B} = (M, 0)$ is valid if it mimics an original behavior of a system and hides secret information to the intruder.

Definition 13 (Enforceable Insertion Function):

Let $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ be an MBRG of an LPN $G - = (N, M_{0}, E, λ)$ and $ω \in L_{S}$ be a secret word, with $ω = e_{1} \dots e_{n}$ , $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ , and ${\ddot{M}}_{B} = (M, 0)$ , where M is a basis marking. The insertion function f specified in Definition 11 is said to be enforceable for $G$ if for all $e_{v}, e {^{'}}_{v} \in E_{v}$ , the insertion sequence $ω^{'} = f (e_{v}, e_{1}, e {^{'}}_{v}) \dots f (e_{v}, e_{n}, e {^{'}}_{v})$ is valid.

Definition 14 (Enforceability):

Given an MBRG $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ of an LPN $G - = (N, M_{0}, E, λ)$ and a secret language $L_{S}, G$ is said to be enforceable if for all $ω \in L_{S}$ in which $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and ${\ddot{M}}_{B} = (M, 0)$ , with $M \in M$ , there exists an enforceable insertion function f.

In this paper, we refer to the enforceability verification of a system as the i-enforceability property, which is defined in.²⁰ Checking enforceability may require the construction of a structure called “E-verifier”. The E-verifier construction starts by building the desired estimator $E_{d} = (D, E, δ_{d}, D_{0})$ from the MBRG $β$ . The estimator $E_{d}$ is retrieved from $β$ by removing all sequences representing secret words that lead to a non-misleading marking and only keeping the accessible part. Then, we build the applicable estimator $E_{A} = (A, E, δ_{a}, A_{0})$ also from the associated MBRG $β$ by deleting all the strings from the set $ϕ = {s \in L (β, {\ddot{M}}_{B_{0}}) | \exists ω \in L_{S}, s = ω e^{+}, δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}, {\ddot{M}}_{B} = (M, 0), δ ({\ddot{M}}_{B}, e) = \ddot{M} {^{'}}_{B}, \ddot{M} {^{'}}_{B} \neq (M, 0)}$ . The feasible estimator $E_{f} = (A, E \cup E_{v}, δ_{f}, A_{0})$ is later constructed by adding self-loop of every possible inserted observable event (which can be inserted to hide the secret) at all the states that belong to the trajectories that represent secret words in $E_{A}$ . As well, the required estimator $E_{r} = (D, E, δ_{r}, D_{0})$ is extracted from the desired estimator $E_{d}$ by adding self-loops of the unobservable events contained in secret words, i.e., $λ ({\hat{T}}_{u})$ , at all the states of $E_{d}$ . The synchronization between $E_{r}$ and $E_{f}$ by the dashed parallel composition (see²⁰⁾ results in the I-verifier automaton $I V = (V, E \cup E_{v}, δ_{i v}, V_{0})$ . Finally, we need to prune the blocking (see²⁰⁾ and excess states (according to Definition 15) in an iterative way as the manner of Basic Supervisory Control Problem-Nonblocking Case (BSCP-NB) (see²⁰⁾ to obtain the E-verifier V. Formally, an E-verifier $V = (X, E \cup E_{v}, δ_{v}, X_{0})$ is an NFA, where $X = {V \in V ∖ [V_{E S} \cup V_{B S}] | \exists s \in L (I V, V_{0}), δ_{i v} (V_{0}, s) = V}$ , $δ_{v} : X \times (E \cup E_{v}) \to X$ is the transition relation which is defined as $δ_{v} = {(X, e, X^{'}) | X, X^{'} \in X, δ_{v} (X, e) = X^{'}, e \in (E \cup E_{v})}$ , where $δ_{v} (X, e) = X^{'}$ means that the execution of the event e from the state X leads the system to the state $X^{'}$ , and the initial state is $X_{0} = V_{0}$ . The enforceability verification of $G$ is outlined in Algorithm 2.

Definition 15 (Excess states):

Given an I-verifier $I V = (V, E \cup E_{v}, δ_{i v}, V_{0})$ , the set of excess states $V_{E S}$ is defined as

\begin{aligned} V_{E S} & = {V \in V | \exists V^{'}, V ″ \in V, \exists e_{v}, e {^{'}}_{v} \in E_{v}, \\ δ_{i v} (V^{'}, e_{v}) & = V, δ_{i v} (V, e {^{'}}_{v}) = V ″, ⧸ \exists e \in E, δ_{i v} (V, e)!} \end{aligned}

Example 4.

Consider again the net system $G$ in Figure 4. Let $L_{S}$ = ${a b, d c}$ be a secret language, where $a b$ and $d c$ are the corresponding strings of $t_{6} t_{7}$ and $t_{9} t_{10}$ , respectively. The MBRG is then given in Figure 6. Although we are using the same graph as Example 3, the MBRG in this example is different since we suggest here another $L_{S}$ . To construct the E-verifier $V$ , building $E_{d}$ , $E_{A}$ , $E_{f}$ , and $E_{r}$ is required. First, we start by the construction of the desired estimator $E_{d}$ . We have $δ ({\ddot{M}}_{B_{0}}, a b) = {\ddot{M}}_{B_{5}} = (M_{5}, 0)$ and $δ ({\ddot{M}}_{B_{0}}, d c) = {\ddot{M}}_{B_{6}} = (M_{6}, 0)$ . Thus, we need to remove the trajectories representing $a b$ and $d c$ from $β$ and take the accessible part. The construction of the desired estimator is shown in Figure 7(a).

Figure 6.

MBRG of LPN in example 4.

Figure 7.

(A) The desired estimator $E_{d}$ , (b) the applicable estimator $E_{A}$ , (c) the feasible estimator $E_{f}$ , and (d) the required estimator $E_{r}$ .

To construct the applicable estimator, the set $ϕ$ needs to be computed. According to MBRG in Figure 6 and $L_{S}$ , we have $ϕ = {d c {(b)}^{+}}$ as the string $d c \in L_{S}$ represents a secret word that satisfies $δ ({\ddot{M}}_{B_{0}}, d c) = {\ddot{M}}_{B_{6}}$ and there exists $b \in E_{o}$ that satisfies $δ ({\ddot{M}}_{B_{6}}, b) = {\ddot{M}}_{B_{8}}$ , in which ${\ddot{M}}_{B_{8}}$ is an unselected basis marking. Thus, the applicable estimator construction is done by deleting the trajectory corresponding to $d c {(b)}^{+}$ . The applicable estimator is shown in Figure 7(b)

The feasible estimator $E_{f}$ is retrieved from $E_{A}$ by adding self-loop of each possibly inserted observable event at all the states of the trajectories containing secret words in $E_{A}$ . The only trajectory representing a secret word in $E_{A}$ is $δ ({\ddot{M}}_{B_{0}}, a b) = {\ddot{M}}_{B_{5}}$ . The possibly inserted observable event set is $E_{v} = E_{o} = {a_{v}, b_{v}, c_{v}}$ . Therefore, to obtain the feasible estimator, we add self-loops of $a_{v}, b_{v}$ , and $c_{v}$ to ${\ddot{M}}_{B_{0}}$ , ${\ddot{M}}_{B_{2}}$ , and ${\ddot{M}}_{B_{5}}$ . The feasible estimator is shown in Figure 7(c).

In the same way, the required estimator is extracted from the desired estimator $E_{d}$ by adding self-loops of the unobservable events contained in secret words, i.e., $λ ({\hat{T}}_{u})$ , at all the states of $E_{d}$ . The required estimator is shown in Figure 7(d). The synchronization of $E_{r}$ and $E_{f}$ with dashed parallel composition (see²⁰⁾ is mandatory to obtain $I V$ , as shown in Figure 8. After obtaining $I V$ , we need to prune the blocking states in an iterative way. At the first round, the unique blocking state is $((M_{1}, - 1), (M_{7}, - 1))$ . After that, $I V$ does not contain blocking states. Then, pruning the excess states should be also effected in an iterative way. The first round for pruning excess state set includes $((M_{0}, - 1), (M_{7}, - 1))$ , $((M_{2}, - 1), (M_{7}, - 1))$ , $((M_{5}, 0), (M_{4}, - 1))$ and at the second round, the only excess state is $((M_{0}, - 1), (M_{4}, - 1))$ .

Figure 8.

The synchronization result $I V$ between $E_{r}$ and $E_{f}$ .

Finally, V is the resulting automaton after pruning the blocking and excess states (represented with dashed red lines in Figure 8) from $I V$ . The E-verifier V is shown in Figure 9(a).

Figure 9.

(a) The E-verifier V and (b) the rest estimator.

Theorem 3.

Given a non-opaque system $G$ and its MBRG $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ , $G$ is enforceable if for all $ω \in L_{S}$ such that $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B} \in {\ddot{M}}_{B}$ with ${\ddot{M}}_{B} = (M, 0)$ and $M \in M$ , one of the following conditions is satisfied:

There exists a string $s \in ϕ$ such that $s = ω {(e)}^{+}$ , where $e \in E_{o}$ .

There exists a state $x \in X$ from the E-verifier V that contains misleading and non-misleading markings.

Proof

Suppose that $G$ is not enforceable. The fact that a given system is not enforceable means that there exists $ω \in L_{S}$ satisfying $δ ({\ddot{M}}_{B_{0}}, ω) = {\ddot{M}}_{B}$ and ${\ddot{M}}_{B} = (M, 0)$ such that one cannot find any insertion function that could insert observable events to $ω$ in order to hide it. Thus, the construction of E-verifier is not feasible. Therefore, the condition (ii) does not hold. In addition, if there exists $s \in ϕ$ such that $s = ω {(e)}^{+}, e \in E_{o}$ , then an insertion function can be defined to insert observable events to $ω$ to hide it. Hence, the intruder will mistakenly estimate the reachable state. The fact that a system is not enforceable implies that the condition (i) is also not satisfied.

LBO enforcement

Once a given system $G$ is verified to be enforceable, then the application of an insertion function technique could be enforced. The E-verifier V considers only some secret words, however, some others are supposed to be enforceable based on a particular features (see Theorem 3). To enforce $G$ , we also need to study the secret words that were not taken into account when creating the E-verifier. Therefore, the following definition is presented.

Definition 16.

Given an MBRG $β = ({\ddot{M}}_{B}, E, δ, {\ddot{M}}_{B_{0}})$ of a system $G$ , a rest estimator of $β$ is defined as an NFA $E_{R} = (R, E, δ_{R}, R_{0})$ , where $R \subseteq {\ddot{M}}_{B} ∖ A$ , $δ_{R} = {(R, e, R^{'}) | R, R^{'} \in R, δ_{R} (R, e) = R^{'}, e \in E}$ , and $R_{0} = {\ddot{M}}_{B_{0}}$ . The estimator $E_{R}$ is retrieved from $β$ after deleting $E_{A}$ .

The possible insertion functions are encoded as an insertion automaton (IA). The IA construction is summarized in Algorithm 4. The construction of IA requires the construction of the rest estimator and the E-verifier. Therefore, the computational complexity of IA depends of the calculation of the worst-case space complexity of both rest estimator and E-verifier. Overall, the complexity analysis of IA building is $O (2^{| R | + | X |})$ .

Example 5.

Continue with Example 4. The system $G$ is checked to be enforceable by following Algorithm 2. Once a system is enforceable, the IA could be constructed according to Algorithm 3. To obtain IA, we need to construct the rest estimator, which is the automaton resulting by removing the applicable estimator from the MBRG, as visualised in Figure 9(b). Based on Algorithm 3, only state $R_{2}$ satisfies the condition of line 2 of Algorithm 3. Following steps 3–5, we redefine $δ_{R} (R_{1}, c b_{v}) = R_{2}$ . As well, following steps 6–12, we first remove state $X_{2} = (M_{0}, - 1), (M_{1}, - 1)$ and then redefine $δ_{v} (X_{0}, b_{v} a) = X_{4}$ , where $X_{0} = (M_{0}, - 1), (M_{0}, - 1)$ and $X_{4} = (M_{2}, - 1), (M_{4}, - 1)$ . Finally, the IA automaton is the result of combination between the rest estimator and the E-verifier (see Figure 10).

Conclusion

In this paper, a novel approach that does not require an exhaustive enumeration of the whole state space is proposed to verify different LBO types and enforce non-opaque secret words in the context of LPN under a generalization partition of transitions. Indeed, a unique graph called MBRG is designed to deal with the opacity verification issue by considering the unobservable transitions for hiding secret strings. The proposed MBRG is then investigated to deal with the opacity enforcement issue. A verification algorithm for checking the enforceability is given. An embedded insertion technique that is more general and powerful than the previously proposed techniques is provided to enforce a verified non-opaque system by adding fictitious occurrences of explicit transitions to change the system's output that is visible to an intruder. Finally, an algorithm is proposed to construct an insertion automaton (IA) that synthesizes different possible insertion functions.

Figure 10.

The IA of example 7.

For future work, we are interested in studying the verification and enforcement of opacity under external attacks and extending the enforcement strategy to an edit mechanism (add/erase events).

Footnotes

ORCID iDs

Salwa Habbachi

Zhiwu Li

Notes

References

Mazaré

. Using unification for opacity properties. In: Proc. 4th IFIP WG1.7 Workshop Issues Theory Security (WITS’04), Spain, 2004 165–176.

Bryans J

Koutny

Ryan P

. Modelling opacity using Petri nets. Electron Notes Theor Comput Sci 2005; 121: 101–115.

Saboori

Hadjicostis

. Notions of security and opacity in discrete event systems. In Proc. 46th IEEE Conf. Decision Control, 2007, 5056–5061.

Zhu

, et al. Fault identification of discrete event systems modeled by Petri nets with unobservable transitions. IEEE Transactions on Systems. Man, and Cybernetics: Systems 2019; 49: 333–345.

Tong

Seatzu

, et al. Verification of state-based opacity using Petri nets. IEEE Trans Autom Control 2017; 62: 2823–2837.

Badouel

Bednarczyk

Borzyszkowski

, et al. Concurrent secrets. Discrete Event Dyn. Syst 2007; 17: 425–446.

Lin

. Opacity of discrete event systems and its applications. Automatica 2011; 47: 496–503.

Jacob

Lesage J

Faure J

. Overview of discrete event systems opacity: models, validation, and quantification. Annu Rev Control 2016; 41: 135–146.

Lafortune

Lin

Hadjicostis C

. On the history of diagnosability and opacity in discrete event systems. Annu Rev Control 2018; 45: 257–266.

10.

Guo

Jiang

Guo

, et al. Overview of opacity in discrete event systems. IEEE Access 2020; 8: 48731–48741.

11.

Tong

Seatzu

, et al. Current-state opacity enforcement in discrete event systems under incomparable observations. Discrete Event Dyn. Syst 2018; 28: 161–182.

12.

Barcelos

Basilio

. Enforcing current-state opacity through shuffle in event observations. In: Proc. 14th International Workshop on Discrete Event Systems 2018; 51: 100–105.

13.

Wu Y

C-

Lafortune

. Enforcement of opacity by public and private insertion functions. Automatica 2018; 93: 369–378.

14.

Zhang

Shu

Lin

. Polynomial algorithms to check opacity in discrete event systems. In: Proc. 24th Control and Decision Conference (CCDC), 2012, 763–769.

15.

Cong

Fanti M

Mangini A

, et al. Decentralized diagnosis by Petri nets and integer linear programming. IEEE Transactions on Systems. Man, and Cybernetics: Systems 2018; 48: 1689–1700.

16.

Mahulea

Seatzu

Cabasino M

, et al. Fault diagnosis of discrete-event systems using continuous Petri nets. IEEE Transactions on Systems. Man, and Cybernetics - Part A: Systems and Humans 2012; 42: 970–984.

17.

Tong

, et al. Verification of language-based opacity in Petri nets using verifier. In: Proc. Amer. Control Conf., 2016, 757–763.

18.

Basile

De Tommasi

. An algebraic characterization of language-based opacity in labeled Petri nets. In: Proc. 14th International Workshop on Discrete Event Systems 2018; 51: 329–336.

19.

Cabasino

Giua

Seatzu

. Diagnosability of discrete-event systems using labeled Petri nets. IEEE Trans Autom Sci Eng 2014; 11: 144–153.

20.

Wu Y

Lafortune

. Synthesis of insertion functions for enforcement of opacity security properties. Automatica 2014; 50: 1336–1348.

21.

Wu Y

Lafortune

. Synthesis of optimal insertion functions for opacity enforcement. IEEE Trans Autom Control 2015; 61: 571–584.

22.

Keroglou

Lafortune

. Verification and synthesis of embedded insertion functions for opacity enforcement. In: Proc. 56th IEEE Conf. Decision Control, 2017, 4217–4223.

23.

Hadjicostis

. Extended insertion functions for opacity enforcement in discrete event systems. IEEE Trans Autom Control. doi: 10.1109/TAC.2021.3121249

24.

Giua

Seatzu

. Fault detection for discrete event systems using Petri nets with unobservable transitions. In: Proc. 44th IEEE Conf. Decision Control, 2005, 6323–6328.

25.

Tong

, et al. Basis marking representation of Petri net reachability spaces and its application to the reachability problem. IEEE Trans Autom Control 2017; 62: 1078–1093.

26.

Lafortune

. Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discrete Event Dyn. Syst 2013; 23: 307–339.

Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets

Abstract

Keywords

Introduction

Preliminaries

Petri Net

Labeled Petri Net

Basis reachability graph

Language-based opacity

Language-based opacity verification approach

Verification of language-based opacity

Modified basis reachability graph (MBRG)

Language-based opacity enforcement approach

Insertion function

Verification of enforceability

LBO enforcement

Conclusion

Footnotes

ORCID iDs

Notes

References