Transforming opacity verification to nonblocking verification in modular systems

TL;DR

This paper introduces a novel compositional method for verifying opacity in systems by transforming the problem into a nonblocking verification task, enabling efficient analysis of large systems.

Contribution

It presents a new abstraction-based approach that reduces opacity verification to nonblocking verification, applicable to current-state and K-step opacity in modular automata.

Findings

Efficient verification of current-state opacity in large systems

Transformation ensures equivalence between opacity and nonblocking properties

Applicable to both current-state and K-step opacity

Abstract

We consider the verification of current-state and K-step opacity for systems modeled as interacting non-deterministic finite-state automata. We describe a new methodology for compositional opacity verification that employs abstraction, in the form of a notion called opaque observation equivalence, and that leverages existing compositional nonblocking verification algorithms. The compositional approach is based on a transformation of the system, where the transformed system is nonblocking if and only if the original one is current-state opaque. Furthermore, we prove that $K$-step opacity can also be inferred if the transformed system is nonblocking. We provide experimental results where current-state opacity is verified efficiently for a large scaled-up system.

Figures

Tables

Table 1. Table 1: Experimental results

Model	Aut	Opa.	OOE	CSE	Nonb.
10 Players	20	False	0 ms	0 ms	94 ms
100 Players	200	False	0 ms	0 ms	359 ms
500 Players	${10}^3$	False	32 ms	16 ms	5.5 s
1000 Players	2$\cdot {10}^3$	False	31 ms	65 ms	16.6 s
2000 Players	4$\cdot {10}^3$	False	63 ms	78 ms	64.4 s
10 Houses	20	False	0 ms	1 ms	0 ms
100 Houses	200	False	15 ms	8 ms	188 ms
500 Houses	${10}^3$	False	62 ms	31 ms	1.1 s
1000 Houses	2$\cdot {10}^3$	False	109 ms	62 ms	3.9 s
2000 Houses	4$\cdot {10}^3$	False	152 ms	141 ms	11.7 s

Equations

$$\begin{split}G=G_{1}\mathbin{\parallel}G_{2}=\left\langle\Sigma_{1}\cup\Sigma_{2},Q_{1}\times Q_{2},\mbox{$\stackrel{{\scriptstyle}}{{\rightarrow}}$},Q^{\circ}_{1}\times Q^{\circ}_{2},Q_{1}^{m}\times Q_{2}^{m}\right\rangle\end{split}$$

$$\begin{array}[]{@{}r@{\quad}l@{}}(x_{1},x_{2})\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}(y_{1},y_{2})&\mbox{if }\sigma\in({{\Sigma}_{1}}\cap{{\Sigma}_{2}}),\\ &x_{1}\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}_{1}y_{1},\ \text{and}\ x_{2}\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}_{2}y_{2}\,;\\ (x_{1},x_{2})\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}(y_{1},x_{2})&\mbox{if }\sigma\in({\Sigma}_{1}\setminus{\Sigma}_{2})\ \cup\{\tau\}\\ &\text{and}\ x_{1}\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}_{1}y_{1}\,;\\ (x_{1},x_{2})\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}(x_{1},y_{2})&\mbox{if }\sigma\in({\Sigma}_{2}\setminus{\Sigma}_{1})\ \cup\{\tau\}\\ &\text{and}\ x_{2}\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}_{2}y_{2}\,;\end{array}$$

$${\to }_{\psi }=\to \cup \{(x,\psi ,\perp )|x\in X_{\psi }\}$$

$$\tilde{G}=\langle\Sigma_{\tau},\tilde{Q},\mbox{$\stackrel{{\scriptstyle}}{{\rightarrow}}$}/\mathord{\sim},\tilde{Q}^{\circ}\rangle\ ,$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&(\forall q_{0}\in Q^{o},\forall s\in\mathcal{L}(G,q^{\circ})\ \colon\ q^{\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{S})\\ &(\exists q^{\prime\circ}\in Q^{o})\ \textit{such~{}that}\ [\ q^{\prime\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{NS}]\end{array}$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&(\forall q_{0}\in Q^{o},\forall st\in\mathcal{L}(G,q^{\circ})\ \colon\ q^{\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{S})\\ &(\exists q^{\prime\circ}\in Q^{o})\ \textit{such~{}that}\ [\ q^{\prime\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{NS}\land q^{\prime\circ}\stackrel{{\scriptstyle st}}{{\Rightarrow}}]\end{array}$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&(\forall q_{0}\in Q^{o},\forall st\in\mathcal{L}(G,q^{\circ})\ \colon\ q^{\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{S}\land|t|\leq K)\\ &(\exists q^{\prime\circ}\in Q^{o})\ \textit{such~{}that}\ [\ q^{\prime\circ}\stackrel{{\scriptstyle s}}{{\Rightarrow}}Q^{NS}\land q^{\prime\circ}\stackrel{{\scriptstyle st}}{{\Rightarrow}}]\end{array}$$

$$H=\Delta (det(G))\parallel {\Delta }_R(det(G_R))$$

$$H\stackrel{s}{\to }(h_1,h_2)\text{implies}[h_1\cap h_2⊈Q^S\vee h_1\cap h_2=\varnothing ]$$

$$\begin{array}[]{@{}r@{\quad}l@{}}[\ h_{1}\cap\ h_{2}\subseteq Q^{S}\land\ h_{1}\cap h_{2}\not=\emptyset\ ]\ \Rightarrow\ |P_{\Delta}(s)|>K.\end{array}$$

$$\mathcal{G}=G_1\parallel \cdots \parallel G_n.$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[(X^i\cap X_R^i)⊈Q_i^S\vee (X^i\cap X_R^i)=\varnothing ,\forall 1\le i\le n]$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[(X^i\cap X_R^i)⊈Q_i^S\vee (X^i\cap X_R^i)=\varnothing ,\forall 1\le i\le n].$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[((X^1\cap X_R^1)\times \dots \times (X^n\cap X_R^n))⊈Q^S,\vee$$

$$((X^1\cap X_R^1)\times \dots \times (X^n\cap X_R^n))=\varnothing ].$$

$$H\stackrel{s}{\to }(X,X_R):[(X\cap X_R)⊈Q^S\vee (X\cap X_R)=\varnothing ].$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[\exists (X^i,X_R^i):(X^i\cap X_R^i)⊈Q_i^S\vee (X^i\cap X_R^i)=\varnothing ]$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[\exists (X^i,X_R^i):(X^i\cap X_R^i)⊈Q_i^S\vee (X^i\cap X_R^i)=\varnothing ].$$

$$H_1\parallel \dots \parallel H_n\stackrel{s}{\to }((X^1,X_R^1),\dots ,(X^n,X_R^n)):$$

$$[((X^1\cap X_R^1)\times \dots \times (X^n\cap X_R^n))⊈Q^S,\vee$$

$$((X^1\cap X_R^1)\times \dots \times (X^n\cap X_R^n))=\varnothing ].$$

$$H\stackrel{s}{\to }(X,X_R):[(X\cap X_R)⊈Q^S\vee (X\cap X_R)=\varnothing ].$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&[\exists(X^{i}\cap X_{R}^{i})\ :\ (X^{i}\cap X_{R}^{i})\subseteq Q_{i}^{S}\land\ (X^{i}\cap X_{R}^{i})\not=\emptyset]\\ &\Rightarrow|P_{\Delta}(s)|>K,\end{array}$$

$$[\exists (X^i\cap X_R^i):(X^i\cap X_R^i)\subseteq Q_i^S\wedge (X^i\cap X_R^i)\ne \varnothing ]$$

$$\Rightarrow |P_{\Delta }(s)|>K,$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&[((X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X^{n}_{R}))\subseteq Q^{S}\\ &\land\ ((X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X^{n}_{R}))\not=\emptyset]\Rightarrow|P_{\Delta}(s)|>K,\end{array}$$

$$\displaystyle[(X\cap X_{R})\subseteq Q^{S}\land(X\cap X_{R})\not=\emptyset]\ \Rightarrow\ |P_{\Delta}(s)|>K,\$$

$$\begin{array}[]{@{}r@{\quad}l@{}}&[(X^{i}\cap X_{R}^{i})\subseteq Q_{i}^{S}\land\ (X^{i}\cap X_{R}^{i})\not=\emptyset,\forall 1\leq i\leq n]\\ &\Rightarrow|P_{\Delta}(s)|>K,\end{array}$$

$$[(X^i\cap X_R^i)\subseteq Q_i^S\wedge (X^i\cap X_R^i)\ne \varnothing ,\forall 1\le i\le n]$$

$$\Rightarrow |P_{\Delta }(s)|>K,$$

Full text

Transforming opacity verification to nonblocking verification in modular systems

Sahar Mohajerani

Department of Electrical engineering and Computer Science

University of Michigan

sahar.mohajerani@gmail.com

&Stéphane Lafortune

Department of Electrical engineering and Computer Science

University of Michigan

stephane@umich.edu The work of the first author was supported by the Swedish Research Council. The work of the second author was supported in part by US NSF grant CNS-1421122.

1 Abstract

We consider the verification of current-state and $K$-step opacity for systems modeled as interacting non-deterministic finite-state automata. We describe a new methodology for compositional opacity verification that employs abstraction, in the form of a notion called opaque observation equivalence, and that leverages existing compositional nonblocking verification algorithms. The compositional approach is based on a transformation of the system, where the transformed system is nonblocking if and only if the original one is current-state opaque. Furthermore, we prove that $K$-step opacity can also be inferred if the transformed system is nonblocking. We provide experimental results where current-state opacity is verified efficiently for a large scaled-up system.

K****eywords Finite-state automata $\cdot$ abstraction $\cdot$ opacity $\cdot$ nonblocking verification $\cdot$ modular systems.

2 Introduction

While there is a large amount of information people willingly release everyday, there is some information that we wish to remain secret. Thus, various notions of security have been studied in the past decades; opacity is one such example. Opacity is an information flow property that identifies whether or not a secret is released to an external observer of the behavior of a known dynamic system. We refer to the external observer as the intruder in this paper.

The notion of opacity was introduced in the field of discrete event systems in [1], where the system is modeled as a Petri net. Later, a variety of notions of opacity were introduced to cope with different security requirements. Current-state opacity [2], initial-state opacity [3], initial-and-final-state opacity [4], $K$-step opacity [5, 6], infinite-step opacity [7], and language-based opacity [8] are some examples of state-based and language-based opacity notions. In [4], polynomial-time algorithms are presented to transform the verification of current-state, initial-state, initial-and-final-state opacity, and language based-opacity to one another. In this paper, we study the verification of current-state and $K$-step opacity under the framework of modular discrete event systems. A system is said to be current-state opaque if the intruder can never know for sure that the current state of the system is a secret state. On the other hand, a system is $K$-step opaque if the intruder cannot determine if the system had entered a secret state within the $K$ previous steps of its observed behavior (i.e., it is a smoothing property in system-theoretic terminology).

In this paper, we consider a class of modular systems that are modeled as partially observed (or non-deterministic) interacting finite state automata. The monolithic approach to verify any opacity property for modular systems is to synchronize all the components of the system and then use the corresponding verification algorithm on the resulting monolithic system. This approach is limited by the well-known state-space explosion problem, when composing a large number of system components.

Abstraction and modular approaches are standard techniques that can be used to alleviate the state-space explosion problem, either independently or jointly. In the opacity verification problem domain, the verification of initial-state opacity in a modular setting was studied in [9], where it is shown that the system is initial-state opaque if and only if the strings causing violations of opacity are disabled by synchronization. Abstraction-based bisimulation was used in [10] to reduce the complexity of the system when verifying infinite-step opacity. One method to alleviate the state-space explosion problem is the compositional approach based on abstraction. This approach is well-developed for nonblocking verification and supervisor synthesis in modular systems; see, e.g., [11, 12, 13, 14]. The compositional approach seeks to remove and merge states that are redundant for the purpose of verification or synthesis, and it proceeds in an incremental manner in terms of system components.

This paper presents a novel compositional approach for the verification of current-state, infinite-step, and $K$-step opacity. As infinite-step opacity is a limiting case of $K$-step opacity, we mainly focus on current-state and $K$-step opacity. In our framework, each system component is abstracted using a restricted version of observation equivalence or weak bisimulation [15], that we call opaque observation equivalence. After such abstraction, the current-state estimator [16] or the two-way observer [17] of each component is generated, depending on which opacity property is to be verified, either current-state or $K$-step. Next, the opacity verification problem is transformed to a suitable nonblocking verification problem. This makes it possible to use well-developed nonblocking verification algorithms to verify the different notions of opacity. In the case of current-state opacity, we show that the transformation to nonblocking leads to an equivalent problem, i.e., we show necessity and sufficiency. In the case of $K$-step opacity, we show sufficiency of the transformation. We used the software tool Supremica [18] to verify current-state opacity of a large modular system using our compositional approach. Specifically, we have successfully verified current-state opacity for a large system containing 4$\cdot 10^{3}$ automata under one minute on a standard laptop computer.

The presentation of our results is organized as follows. Sect. 3 gives a brief background about different notions of opacity. Sect. 4 explains the general compositional opacity problem. Next, Sections 5 and 7 explain the compositional approach for current-state and $K$-step opacity, respectively. Our experimental results on a scaled-up example are presented in Sect. 8. Finally, some concluding remarks can be found in Sect. 9.

3 Modeling framework

3.1 Automata and their composition

Discrete system behaviors can be modeled by deterministic or nondeterministic automata.

Definition 1

A (nondeterministic) finite-state automaton is a tuple $G=\langle{\Sigma},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$, where $\Sigma$ is a finite set of events, $Q$ is a finite set of states, \mbox{\stackrel{{\scriptstyle}}{{\rightarrow}}}\subseteq Q\times\Sigma\times Q is the state transition relation, and $Q^{\circ}\subseteq Q$ is the set of initial states. $G$ is deterministic if $|Q^{\circ}|=1$ and if $x\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y_{1}$ and $x\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y_{2}$ always implies that $y_{1}=y_{2}$.

When marking is important the above definition can be extended to $G=\langle{\Sigma},Q,\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ},Q^{m}\rangle$, where $Q^{m}\subseteq Q$ is the set of marked states. In this paper, we identify marked states in the figures using gray shading.

We assume that the intruder can only partially observe the system. Thus, ${\Sigma}$ is partitioned into two disjoint subsets, the set of observable events and the set of unobservable events. Since the identity of unobservable events are irrelevant they are all replaced by a special event $\tau$. The event $\tau$ is never included in the alphabet ${\Sigma}$, unless explicitly mentioned. For this, ${\Sigma}_{\tau}={\Sigma}\cup\{\tau\}$ is used [11]. Nondeterministic automata hereafter may contain transitions labeled by $\tau$. However, since $\tau$ represents unobservable events, deterministic automata will never have $\tau$ transitions. In opacity problems, the set of states is also partitioned into two disjoint subsets: $Q^{S}$ the set of secret states and $Q^{NS}=Q\setminus Q^{S}$ the set of non-secret states.

When automata are brought together to interact, lock-step synchronization in the style of [19] is used.

Definition 2

Let $G_{1}=\langle{\Sigma}_{1},\penalty 750Q_{1}^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}_{1}},\penalty 750Q^{\circ}_{1},\penalty 750Q_{1}^{m}\rangle$ and $G_{2}=\langle{\Sigma}_{2},\penalty 750Q_{2}^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}_{2}},\penalty 750Q^{\circ}_{2},\penalty 750Q_{2}^{m}\rangle$ be two nondeterministic automata, with sets of secret states $Q_{1}^{S}\subseteq Q_{1}$ and ${Q_{2}^{S}}\subseteq Q_{2}$. The synchronous composition of $G_{1}$ and $G_{2}$ is defined as

[TABLE]

where

[TABLE]

and where the set of secret states of $G$, $Q^{S}$, is defined in one of the two following ways:

1. (i)

$Q^{S}=\{(x_{1},x_{2})\ |\ x_{1}\in Q_{1}^{S}\ \land\ x_{2}\in Q_{2}^{S}\}$, 2. (ii)

$Q^{S}=\{(x_{1},x_{2})\ |\ x_{1}\in Q_{1}^{S}\ \lor\ x_{2}\in Q_{2}^{S}\}$.

Importantly, this definition of synchronous composition only imposes lock-step synchronization on common events in $\Sigma$.

In the following, whenever necessary, we use the notations $\mathbin{\parallel}_{\land}$ and $\mathbin{\parallel}_{\lor}$ to show that the secret states of synchronous composition are defined as in Def. 2 (i) or (ii), respectively. When $\mathbin{\parallel}_{\land}$ is used, a synchronized state is considered secret if all the composed states are secret. In $\mathbin{\parallel}_{\lor}$ however, if one of the states of the synchronized state is secret, then the synchronized state is considered secret. $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$ are the first natural constructs for joint secrecy.

${\Sigma}^{*}$ is the set of all finite traces of events from ${\Sigma}$, including the empty trace $\varepsilon$. The natural projection $P_{\tau}\colon\Sigma_{\tau}^{*}\to{\Sigma}^{*}$ is the operation that removes from traces $t\in{\Sigma}_{\tau}^{*}$ all events not in ${\Sigma}$, which affects only event $\tau$ in our setting.

The transition relation of an automaton $G$ is written in infix notation $x\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y$, and it is extended to strings in $\Sigma_{\tau}^{*}$ by letting $x\stackrel{{\scriptstyle\varepsilon}}{{\rightarrow}}x$ for all $x\in Q$, and $x\stackrel{{\scriptstyle t\sigma}}{{\rightarrow}}z$ if $x\stackrel{{\scriptstyle t}}{{\rightarrow}}y$ and $y\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}z$ for some $y\in Q$. Furthermore, $x\stackrel{{\scriptstyle t}}{{\rightarrow}}$ means that $x\stackrel{{\scriptstyle t}}{{\rightarrow}}y$ for some $y\in Q$, and $x\stackrel{{\scriptstyle}}{{\rightarrow}}y$ means that $x\stackrel{{\scriptstyle t}}{{\rightarrow}}y$ for some $t\in{\Sigma}_{\tau}^{*}$. These notations also apply to state sets, where $X\stackrel{{\scriptstyle t}}{{\rightarrow}}Y$ for $X,Y\subseteq Q$ means that $x\stackrel{{\scriptstyle t}}{{\rightarrow}}y$ for some $x\in X$ and $y\in Y$, and to automata, where $G\stackrel{{\scriptstyle t}}{{\rightarrow}}$ means that $Q^{\circ}\stackrel{{\scriptstyle t}}{{\rightarrow}}$, etc.

For brevity, $p\stackrel{{\scriptstyle s}}{{\Rightarrow}}q$, with $s\in{\Sigma}^{*}$, denotes the existence of a string $t\in{\Sigma}_{\tau}^{*}$ such that $P_{\tau}(t)=s$ and $p\stackrel{{\scriptstyle t}}{{\rightarrow}}q$. Thus, $p\stackrel{{\scriptstyle u}}{{\rightarrow}}q$, $u\in{\Sigma}_{\tau}^{*}$, means a path containing exactly the events in $u$, while $p\stackrel{{\scriptstyle u}}{{\Rightarrow}}q$, $u\in{\Sigma}^{*}$, means existence of a path between $p$ and $q$ with arbitrary number of $\tau$ events between the events of $u$. Similarly, $p\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}q$ denotes the existence of a string $t\in\{\tau\}^{*}$ such that $p\stackrel{{\scriptstyle t}}{{\rightarrow}}q$.

The language of an automaton $G$ is defined as $\mathcal{L}(G)=\{\,s\in{\Sigma}^{*}\mid G\stackrel{{\scriptstyle s}}{{\Rightarrow}}\,\}$ and the language generated by $G$ from $q\in Q$ is $\mathcal{L}(G,q)=\{s\in{\Sigma}^{*}\ |\ q\stackrel{{\scriptstyle s}}{{\Rightarrow}}\}$. Thus we do not include event $\tau$ in the strings in the language of an automaton. Moreover, from Def. 2, it follows that $s\in\mathcal{L}(G_{1}\mathbin{\parallel}G_{2})$ if and only if $P_{1}(s)\in\mathcal{L}(G_{1})$ and $P_{2}(s)\in\mathcal{L}(G_{2})$, where $P_{i}:{\Sigma}_{1}\cup{\Sigma}_{2}\to{\Sigma}_{i}$, for $i=1,2$ (and these functions are extended to strings in the usual manner).

Renamings $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ are two maps such that $\Delta(\sigma)=(\sigma,\epsilon)$ and $\Delta_{R}(\sigma)=(\epsilon,\sigma)$. Renamings are extended to traces $s\in{\Sigma}^{*}$ by applying them to each event, and to languages $L\subseteq{\Sigma}^{*}$ by applying them to all traces. They are also extended to automata with alphabet $\Sigma$ by replacing all transitions $x\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y$ with $x\xrightarrow{\Delta(\sigma)}y$ and $x\xrightarrow{\Delta_{R}(\sigma)}y$.

Given an automaton $G=\langle{\Sigma}_{\tau},Q,\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ}\rangle$ the reversed automaton of $G$ is a non-deterministic automaton $G_{R}=\langle\Sigma_{\tau},Q,\stackrel{{\scriptstyle}}{{\rightarrow}}_{R},Q\rangle$ where $\stackrel{{\scriptstyle}}{{\rightarrow}}_{R}=\{(x,\sigma,y)\ |\ y\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}x\}$ and all states are considered to be initial [4]. For non-deterministic automaton $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$, the set of unobservably reached states of $B\in 2^{Q}$, is $UR(B)=\bigcup\{C\subseteq Q\ |\ B\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}C\}$. The observer automaton $det(G)=\langle{\Sigma},X_{obs},\stackrel{{\scriptstyle}}{{\rightarrow}}_{obs},X_{obs}^{\circ}\rangle$ is a deterministic automaton, where $X_{obs}^{\circ}=UR(Q^{o})$ and $X_{obs}\subseteq 2^{Q}$, and $X\stackrel{{\scriptstyle}}{{\rightarrow}}_{obs}Y$, where $X,Y\subseteq X_{obs}$, if and only if $Y=\bigcup\{UR(y)\ |\ x\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y\ \textnormal{for some}\ x\in X\ \textnormal{and}\ y\in Q\}$. By convention, in this paper only reachable states from $X^{\circ}_{obs}$ under $\stackrel{{\scriptstyle}}{{\rightarrow}}_{obs}$ are considered in $X_{obs}$. Also, we will refer to the observer automaton as the current-state estimator, abbreviated as CSE.

In this paper, the special blocking event $\psi\notin{\Sigma}$ is used to label additional transitions going out of a special set of states, termed $\psi$-states and denoted by $X_{\psi}$.

Definition 3

Let $G=\langle{\Sigma},Q,\stackrel{{\scriptstyle}}{{\rightarrow}},q^{\circ}\rangle$ be a deterministic automaton with set of $\psi$-states $X_{\psi}\subseteq Q$. Then $G_{\psi}=\langle{\Sigma}\cup\{\psi\},Q\cup\{{\mathord{\perp}}\},\stackrel{{\scriptstyle}}{{\rightarrow}}_{\psi},q^{\circ},Q^{m}\rangle$ is a deterministic automaton such that ${\mathord{\perp}}$ is a new state, $Q^{m}=Q$, which means that all the original states are marked, and

[TABLE]

This “$\psi$-transformation” will be used later on to transform opacity verification to nonblocking verification. To check if a specific state of the system can be reached, the state can be considered as a $\psi$-state and nonblocking verification can be done on the transformed system, termed the $\psi$-system. In our setting the $\psi$-states are the states that violate opacity.

Another common automaton operation is the quotient modulo an equivalence relation on the state set.

Definition 4

Let $Z$ be a set. A relation $\mathord{\sim}\subseteq Z\times Z$ is called an equivalence relation on $Z$ if it is reflexive, symmetric, and transitive. Given an equivalence relation $\mathord{\sim}$ on $Z$, the equivalence class of $z\in Z$ is $[z]=\{\,z^{\prime}\in Z\mid z\sim z^{\prime}\,\}$, and $\tilde{Z}=\{\,[z]\mid z\in Z\,\}$ is the set of all equivalence classes modulo $\sim$.

Definition 5

Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be an automaton and let $\mathord{\sim}\subseteq Q\times Q$ be an equivalence relation. The quotient automaton of $G$ modulo $\sim$ is

[TABLE]

where \mbox{\stackrel{{\scriptstyle}}{{\rightarrow}}}/\mathord{\sim}=\mbox{\stackrel{{\scriptstyle}}{{\rightarrow}}}/\mathord{\sim}=\{\,([x],\sigma,[y])\mid\exists x^{\prime}\in[x],y^{\prime}\in[y]:x^{\prime}\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}y^{\prime}\,\} and $\tilde{Q}^{\circ}=\{\,[x^{\circ}]\mid x^{\circ}\in Q^{\circ}\,\}$.

3.2 Notions of opacity

In general, opacity addresses the issue whether an intruder observing the system, and knowing the model of the system, can determine for sure if the system is in a secret state. There are different notions of opacity in the literature. It is shown in [4] that initial, final, current-state, and language-based opacity can be transformed to one another with polynomial-time algorithms for verification purposes. Moreover, infinite-step opacity is a limiting case of $K$-step opacity. Thus, in this paper, we mainly address the verification of current-state opacity first, and then that of $K$-step opacity, which cannot be transformed to current-state opacity for verification purposes. We recall the formal definitions of these properties in the context of the framework of this paper.

Definition 6

A non-deterministic automaton $G$ with event set ${\Sigma}$ and set of secret states $Q^{S}$ is current-state opaque, with respect to $Q^{S}$ if and only if

[TABLE]

The system is current-state opaque if an intruder cannot determine whether the system is currently in a secret state or not.

Definition 7

A non-deterministic automaton $G$ with event set ${\Sigma}$ and set of secret states $Q^{S}$ is infinite-step opaque, with respect to $Q^{S}$

[TABLE]

The system is infinite-step opaque if an intruder cannot determine whether the system ever was in a secret state or not at any time in the past.

Definition 8

A non-deterministic automaton $G$ with event set ${\Sigma}$ and set of secret states $Q^{S}$ is $K$-step opaque, with respect to $Q^{S}$

[TABLE]

The system is $K$-step opaque if the entrance of the system into a secret state remains uncertain for an intruder after up to $K$ future observations. Hence, 0-step opacity is equivalent to current-state opacity, and when $K\stackrel{{\scriptstyle}}{{\rightarrow}}\infty$, then $K$-step opacity becomes infinite-step opacity [7].

It is shown in [16] that current-state opacity can be verified by building the standard observer automaton.

Proposition 1

[16*]** Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton with set of secret states $Q^{S}$. Let $det(G)=\langle{\Sigma},X_{obs},\stackrel{{\scriptstyle}}{{\rightarrow}}_{obs},X_{obs}^{\circ}\rangle$ be the current-state estimator of $G$. Then $G$ is current-state opaque with respect to $Q^{S}$ if and only if for all $s\in\mathcal{L}(G)$ it holds that $[det(G)\stackrel{{\scriptstyle s}}{{\rightarrow}}X\ \text{implies that}\ X\not\subseteq Q^{S}]$. *

The verification of infinite-step and $K$-step opacity is considered in [5] and [7], respectively, where these properties were first introduced. Recently, a new approach for the verification of infinite and $K$-step opacity was introduced, which relies on building the so-called two-way observer of the system [17]. We will leverage this latter approach in the development of our results. Again, we recall relevant definitions and results, restated in the context of our framework.

Definition 9

[17]** Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton and $G_{R}$ be the reversed automaton of $G$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$. The two-way observer of $G$ is the deterministic automaton obtained by:

[TABLE]

Proposition 2

[17]** Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton with set of secret states $Q^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H=\langle\Delta({\Sigma})\cup\Delta_{R}({\Sigma}),Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$ be the two-way observer of $G$. Then $G$ is infinite-step opaque with respect to $Q^{S}$ if and only if

[TABLE]

The system is infinite-step opaque if for all the reachable states of the two-way observer, the intersection of the first with the second components is not a subset of the secret states of the system or it is empty.

Proposition 3

[17]** Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton with set of secret states $Q^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, with ${\Sigma}_{H}=\Delta({\Sigma})\cup\Delta_{R}({\Sigma})$, be the two-way observer of $G$. Let $P_{\Delta}:{\Sigma}_{H}\stackrel{{\scriptstyle}}{{\rightarrow}}\Delta_{R}({\Sigma})$. Then $G$ is $K$-step opaque with respect to $Q^{S}$ if and only if, for any string $s\in\mathcal{L}(H)$ such that $Q^{\circ}_{H}\stackrel{{\scriptstyle s}}{{\rightarrow}}(h_{1},h_{2})$, we have that

[TABLE]

Example 1

Consider automaton $G_{1}$ in Fig. 1. Assume that the set of secret states is $Q^{S}=\{s_{1},s_{3}\}$; we have that $\Delta\colon\ \{\alpha,\beta\}\to\ \{(\alpha,\epsilon),(\beta,\epsilon)\}$ and $\Delta_{R}\colon\ \{\alpha,\beta\}\to\ \{(\epsilon,\alpha),(\epsilon,\beta)\}$. In the figure $det(G_{1})$ and $H_{1}$ are the current-state estimator and the two-way observer of $G_{1}$, respectively. In $H_{1}$ the states are:

• •

$A=(\{s_{0}\},\{s_{0},s_{1},s_{2},s_{3},s_{4},s_{5}\})$,

• •

$B=(\{s_{0}\},\{s_{0}\})$,

• •

$C=(\{s_{0}\},\{s_{1},s_{3}\})$,

• •

$D=(\{s_{1},s_{2},s_{3},s_{4}\},\{s_{0},s_{1},s_{2},,s_{3},s_{4},s_{5}\})$,

• •

$E=(\{s_{1},s_{2},s_{3},s_{4}\},\{s_{0}\})$,

• •

$F=(\{s_{1},s_{2},s_{3},s_{4}\},\{s_{1},s_{3}\})$,

• •

$I=(\{s_{5}\},\{s_{0},s_{1},s_{2},s_{3},s_{4},s_{5}\})$,

• •

$J=(\{s_{5}\},\{s_{0}\})$,

• •

$K=(\{s_{5}\},\{s_{1},s_{3}\})$.

The system is current-state opaque as the intruder cannot distinguish between $s_{0}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}s_{1}$ and $s_{0}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}s_{2}$. Automaton $det(G_{1})$ confirms that the system is current-state opaque since there is no state in $det(G_{1})$ which is subset of $Q^{S}$ (Prop. 1). However, the system is not infinite-step opaque, because after observing event $\beta$ the intruder will know that system was in $s_{1}$ and $s_{3}$. The two-way observer $H_{1}$ confirms this result as in the state $F$ we have $\{s_{1},s_{2},s_{3},s_{4}\}\cap\{s_{1},s_{3}\}=\{s_{1},s_{3}\}\subseteq Q^{S}$ (Prop. 2). The system is not $K=1$ step opaque either since $H_{1}\xrightarrow{(\epsilon,\beta)(\alpha,\epsilon)}F$ and $\{s_{1},s_{2},s_{3},s_{4}\}\cap\{s_{1},s_{3}\}=\{s_{1},s_{3}\}\subseteq Q^{S}$ but $P_{\Delta}((\epsilon,\beta)(\alpha,\epsilon))=(\epsilon,\beta)$ and $|P_{\Delta}((\epsilon,\beta)(\alpha,\epsilon))|\not>1$ (Prop. 3).

4 Compositional opacity verification

This section describes the general framework of transforming current-state opacity and $K$-step opacity to nonblocking verification. Since infinite-step opacity is a limiting case of $K$-step opacity, a specific treatment of this property is omitted hereafter; instead, we make relevant observations about it in our discussion; see Sect. 7. Note that current-state opacity is also a special case of $K$-step opacity. However, since verification of current-state opacity requires building the current state estimator and not the two-way observer, we address current-state opacity separately from $K$-step opacity.

The input to the algorithm is a modular nondeterministic system. A modular system is a collection of interacting components

[TABLE]

The compositional opacity verification algorithm is summarized in Fig. 2 and the steps are as follow:

1. (i)

At the first of the compositional opacity verification, the modular system (5) is abstracted, using opaque observation equivalence. Each automaton $G_{i}$ may be replaced by an abstracted version, $\tilde{G}_{i}$, with less states or transitions. 2. (ii)

Next, the current-state estimators, in the case of current-state opacity verification, or the two-way observers, in the case of $K$-step opacity verification, of the individual abstracted components are built, $H_{i}$ in Fig. 2. 3. (iii)

Next, the opacity verification problem is transformed to nonblocking verification problem. The states of the individual current-state estimators or the two-way observers that violate opacity are identified and transitions to blocking states from those states are added, resulting in $H_{i,\psi_{i}}$ in Fig. 2. 4. (iv)

Compositional nonblocking verification is used to verified opacity problem. In compositional nonblocking verification, the synchronous composition is computed gradually, abstracting each intermediate result again. Eventually, the procedure leads to a single automaton, denoted by $\tilde{H}$, which due to the abstraction process has less states and transitions compared to the original system. Once $\tilde{H}$ is found, it is used for nonblocking verification. The system is current-state opaque if and only if $\tilde{H}$ is nonblocking and it is $K$-step opaque if $\tilde{H}$ is nonblocking.

Our motivation for proceeding as above is that compositional nonblocking verification has been well studied and it has shown very promising results [11, 12].

The monolithic approach to verify opacity, first synchronizes all the component of the system and builds the monolithic current-state estimator or two-way observer of the system. As the number of the states of the synchronized product grows exponentially with the number of components, the complexity of building the CSE or the two-way observer of the whole system is $\mathcal{O}(2^{|X|^{n}})$. In contrast, the complexity of generating modular CSEs or two-way observers, instead of their monolithic counterparts, is $\mathcal{O}(2^{|X|})$, which is significantly smaller. In addition, the proposed approach in this paper not only avoid building synchronized product of the whole system, but it also abstracts the components and reduces the number of the states of each component before the construction of CSEs or two-way observers. Fig. 2 illustrates the steps of compositional opacity verification for the two cases of $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$. The subsequent sections formally develop this approach.

5 Compositional current-state opacity verification

This section describes compositional current-state opacity verification. First, Sect. 5.1 describes the abstraction methods that preserve current-state opacity. Next, Sect. 5.2 describes that individual current-state estimators can be built instead of the monolithic current-state estimator. Finally, Sect. 5.3 explains the transformation of current-state opacity verification to compositional nonblocking verification.

5.1 Opaque observation equivalence

At the first stage of compositional opacity verification, individual nondeterministic components are replaced by their abstracted opaque equivalent components, step (i) in Fig. 2.

Bisimulation equivalence and observation equivalence are two well-known abstraction methods [20] to abstract the state space of an automaton. Bisimulation considers states to be equivalent if they have outgoing transitions with the same events, including unobservable events, to equivalent states. Observation equivalence is more general than bisimulation as it ignores the unobservable events (namely, event $\tau$ in our set-up).

Definition 10

[20*]** Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton. An equivalence relation $\approx\ \subseteq Q\times Q$ is called an

• observation equivalence* on $G$, if the following holds for all $x_{1},x_{2}\in Q$ such that $x_{1}\approx x_{2}$: if $x_{1}\stackrel{{\scriptstyle s}}{{\Rightarrow}}y_{1}$ for some $s\in{\Sigma}^{*}$, then there exists $y_{2}\in Q$ such that $x_{2}\stackrel{{\scriptstyle s}}{{\Rightarrow}}y_{2}$, and $y_{1}\approx y_{2}$.*

In order to use observation equivalence for abstraction in our compositional opacity verification methodology, the set of secret states needs to be taken into account. For this purpose, a restricted version of observation equivalence called opaque observation equivalence is defined.

Definition 11

Let $G=\langle\Sigma_{\tau},\penalty 750Q^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}},\penalty 750Q^{\circ}\rangle$ be a non-deterministic automaton with set of secret states $Q^{S}\subseteq Q$ and set of non-secret states $Q^{NS}=Q\setminus Q^{S}$. An equivalence relation $\mathord{\sim}\subseteq Q\times Q$ is called an opaque observation equivalence on $G$ if the following holds for all $x_{1},x_{2}\in Q$ such that $x_{1}\sim x_{2}$:

1. (i)

if $x_{1}\stackrel{{\scriptstyle s}}{{\Rightarrow}}y_{1}$ for some $s\in{\Sigma}^{*}$, then there exists $y_{2}\in Q$ such that $x_{2}\stackrel{{\scriptstyle s}}{{\Rightarrow}}y_{2}$, and $y_{1}\sim y_{2}$, 2. (ii)

$x_{1}\in Q^{S}$* if and only if $x_{2}\in Q^{S}$.*

Opaque observation equivalence considers two states to be equivalent if they have the same secret property and from both of them equivalent states can be reached by the same sequences of events aside from the $\tau$ event.

We present our first result on the use of opaque observation equivalence in the verification of opacity. (In the sequel, for the sake of simplicity of notation, we will denote the event set of non-deterministic automata by ${\Sigma}$, with the understanding that some transitions may be labeled by $\tau$.)

Theorem 4

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\lor}$ for interaction, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is current-state opaque if and only if $\tilde{\mathcal{G}}$ is current-state opaque.

Proof:

Consider $T=G_{2}\mathbin{\parallel}G_{3}\mathbin{\parallel}\ldots\mathbin{\parallel}G_{n}=\langle{\Sigma}_{T},Q_{T},\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ}_{T}\rangle$. Then $Q^{S}_{T}=Q^{T}\setminus Q_{T}^{NS}$, where $Q_{T}^{NS}=Q^{NS}_{2}\times\ldots\times Q^{NS}_{n}$. Let $P_{G}:{\Sigma}_{T}\cup{\Sigma}_{G_{1}}\to{\Sigma}_{G_{1}}$ and $P_{T}:{\Sigma}_{T}\cup{\Sigma}_{G_{1}}\to{\Sigma}_{T}$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\lor}T$ is not current-state opaque then $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T$ is not current-state opaque either, and vice versa.

1. (i)

Assume that $G_{1}\mathbin{\parallel}_{\lor}T$ is not current-state opaque. Then there exists $(x_{1},x_{T})\in Q_{G_{1}}\times Q_{T}$ such that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$ and $x_{1}\in Q_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$, and there does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$. From $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$ it follows that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x_{1}$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$.

From there does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$, it follows that for all $x_{1}^{\prime}\in Q_{G_{1}}$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}_{1}$ it holds that $x^{\prime}_{1}\in Q_{1}^{S}$ or for all $x_{T}^{\prime}\in Q_{T}$ such that $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x^{\prime}_{T}$ it holds that $x^{\prime}_{T}\in Q_{T}^{S}$. Moreover, since $G_{1}$ and $\tilde{G_{1}}$ are opaque observation equivalent from $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x_{1}$ and based on Def. 11, it follows that $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{2}]$ such that $x_{1}\in[x_{2}]$. Now, consider three cases:

1. a)

$x_{T}\in Q_{T}^{S}$ and $x_{1}\in Q_{1}^{NS}$. Then from $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{2}]$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$, it follows that $\tilde{G_{1}}\mathbin{\parallel}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{2}],x_{T})$. State $([x_{2}],x_{T})$ is also considered secret as $x_{T}\in Q_{T}^{S}$. Since for all $x_{T}^{\prime}\in Q_{T}$ such that $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x^{\prime}_{T}$ it holds that $x^{\prime}_{T}\in Q_{T}^{S}$, then $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{2}],x^{\prime}_{T})$ such that $x^{\prime}_{T}\in Q_{T}^{NS}$ does not exist. Thus, $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T$ is not current-state opaque. 2. b)

$x_{1}\in Q_{1}^{S}$ and $x_{T}\in Q_{T}^{NS}$. Then from $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{2}]$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$, it follows that $\tilde{G}_{1}\mathbin{\parallel}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{2}],x_{T})$. As $x_{1}\in[x_{2}]$ based on Definition 11, it holds that for all $x\in[x_{2}]$, $x\in Q_{1}^{S}$ and $[x_{2}]\in\tilde{Q}_{1}^{S}$, which implies that $([x_{2}],x_{T})$ is a secret state. Since for all $x_{1}^{\prime}\in Q_{G_{1}}$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}_{1}$ it holds that $x^{\prime}_{1}\in Q_{1}^{S}$, based on Definition 11 it follows that for all $[x^{\prime}]\in\tilde{Q}_{G_{1}}$ such that $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x^{\prime}]$ it holds that $[x^{\prime}]\in\tilde{Q}^{S}_{1}$. Thus, $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}],x^{\prime}_{T})$ such that $[x^{\prime}]\in\tilde{Q}^{NS}_{1}$ does not exist, which means that $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T$ is not current-state opaque. 3. c)

$x_{T}\in Q_{T}^{S}$ and $x_{1}\in Q_{1}^{S}$. Then the proof follows from (i)a) and (i)b). 2. (ii)

Assume that $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T$ is not current-state opaque. Then there exists $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$ such that $[x_{1}]\in\tilde{Q}_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$ and there does not exists $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}_{G_{1}}\times Q_{T}$ such that $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ and $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$. From $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, it follows that $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{1}]$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$. From there does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$ such that $\tilde{G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$, it follows that for all $[x^{\prime}_{1}]\in\tilde{Q}_{G_{1}}$ such that $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x^{\prime}_{1}]$ it holds that $[x^{\prime}_{1}]\in\tilde{Q}_{1}^{S}$ or for all $x^{\prime}_{T}\in Q_{T}$ such that $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x^{\prime}_{T}$ it holds that $x^{\prime}_{T}\in Q_{T}^{S}$. Moreover, since $G_{1}$ and $\tilde{G_{1}}$ are opaque observation equivalent from $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{1}]$ and based on Definition 11, it follows that there exists $x\in[x_{1}]$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x$.

Again, consider three cases:

1. a)

$x_{T}\in Q_{T}^{S}$ and $[x_{1}]\in\tilde{Q}_{1}^{NS}$. The proof is similar to (i)a). 2. b)

$[x_{1}]\in\tilde{Q}_{1}^{S}$ and $x_{T}\in Q_{T}^{NS}$. Then as $[x_{1}]\in\tilde{Q}_{1}^{S}$ it holds that for all $x\in[x_{1}]$ also $x\in Q_{1}^{S}$. Thus, from $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$ it follows that there exists $G_{1}\mathbin{\parallel}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x,x_{T})$, where $(x,x_{T})$ is considered a secret state. Since for all $[x^{\prime}_{1}]\in\tilde{Q}_{G_{1}}$ such that $\tilde{G_{1}}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x^{\prime}_{1}]$ it holds that $[x^{\prime}_{1}]\in\tilde{Q}_{1}^{S}$, then by Definition 11 it holds that for all $x^{\prime}\in Q_{G_{1}}$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}$ it holds that $x^{\prime}\in Q_{1}^{S}$. This means that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime},x^{\prime}_{T})$ such that $x^{\prime}\in Q_{1}^{NS}$ does not hold, which implies that $G_{1}\mathbin{\parallel}_{\lor}T$ is not current-state opaque. 3. c)

$x_{T}\in Q_{T}^{S}$ and $[x_{1}]\in\tilde{Q}_{1}^{S}$. Then the proof follows from (ii)a) and (ii)b). $\blacksquare$

Theorem 4 illustrates that the components of a modular system that are interacting by $\mathbin{\parallel}_{\lor}$ can be abstracted using opaque observation equivalence while preserving the current-state opacity property. If $\mathbin{\parallel}_{\land}$ is used for interaction, a similar result holds and the following corollary can be proved.

Corollary 5

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\land}$ for interaction and with the set of secret states $Q^{S}=Q_{1}^{S}\times\ldots\times Q_{n}^{S}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is current-state opaque if and only if $\tilde{\mathcal{G}}$ is current-state opaque.

Proof:

Consider $G_{2}\mathbin{\parallel}\ldots\mathbin{\parallel}G_{n}=T=\langle{\Sigma}_{T},Q_{T},\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ}_{T}\rangle$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque either and vice versa. Let $P_{G}:{\Sigma}_{T}\cup{\Sigma}_{G_{1}}\to{\Sigma}_{G}$ and $P_{T}:{\Sigma}_{T}\cup{\Sigma}_{G_{1}}\to{\Sigma}_{T}$.

1. (i)

If $G_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque. Then there exists $(x_{1},x_{T})\in Q_{G_{1}}\times Q_{T}$ such that $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$ and $(x_{1},x_{T})\in Q_{1}^{S}\times Q_{T}^{S}$, and there does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q_{G_{1}}\times X_{T}$ such that $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$ and $x^{\prime}_{1}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$. This means, there does not exist $x^{\prime}_{1}\in Q^{NS}_{G}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}_{1}$ or $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x^{\prime}_{T}$. Now we need to show the two following cases:

1. a)

$\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{2}],x_{T})$ and $([x_{2}],x_{T})\in\tilde{Q}_{1}^{S}\times Q_{T}^{S}$. Since $G_{1}$ and $\tilde{G}_{1}$ are opaque observation equivalent from $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x_{1}$ and based on Definition 11 it follows that $\tilde{G}_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{2}]$ such that $x_{1}\in[x_{2}]$. From $\tilde{G}_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{2}]$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$ it follows that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{2}],x_{T})$. As $x_{1}\in[x_{2}]$ based on Definition 11 it holds that for all $x\in[x_{2}]$, $x\in Q_{1}^{S}$ and $[x_{2}]\in\tilde{Q}_{1}^{S}$. This means $([x_{2}],x_{T})\in\tilde{Q}_{1}^{S}\times Q_{T}^{S}$. 2. b)

There does not exist $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}],x^{\prime}_{T})$ such that $[x^{\prime}]\in\tilde{Q}_{1}^{NS}$ or $x^{\prime}_{T}\in Q_{T}^{NS}$. From there does not exist $x^{\prime}_{1}\in Q^{NS}_{G}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}_{1}$ or $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x^{\prime}_{T}$ and based on Definition 11 it follows that there does not exist $[x^{\prime}]\in\tilde{Q}^{NS}_{1}$ and $x_{1}^{\prime}\in[x^{\prime}]$ such that $\tilde{G}_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x^{\prime}]$ either. This implies there does not exist $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}],x^{\prime}_{T})$ such that $[x^{\prime}]\in\tilde{Q}^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$.

Therefore it can be concluded that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque. 2. (ii)

If $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque. Then there exists $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$ such that $([x_{1}],x_{T})\in\tilde{Q}_{1}^{S}\times Q_{T}^{S}$ and there does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}_{G_{1}}\times Q_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ and $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$. From $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$ it follows that $\tilde{G}_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{1}]$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$ and $[x_{1}]\in\tilde{Q}_{G}^{S}$ and $x_{T}\in Q_{T}^{S}$. Again we need to show the two following cases:

1. a)

$G_{1}\mathbin{\parallel}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x,x_{T})$, where $(x,x_{T})\in Q^{S}_{1}\times Q^{S}_{T}$. since $G_{1}$ and $\tilde{G}_{1}$ are opaque observation equivalent from $\tilde{G}_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}[x_{1}]$ and based on Definition 11 it follows that there exists $x\in[x_{1}]$ such that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x$. Then as $[x_{1}]\in\tilde{Q}_{1}^{S}$ it holds that for all $x\in[x_{1}]$ also $x\in Q_{1}^{S}$. Thus, from $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x$ and $T\stackrel{{\scriptstyle P_{T}(s)}}{{\Longrightarrow}}x_{T}$ it follows that $G_{1}\mathbin{\parallel}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x,x_{T})$, where $(x,x_{T})\in Q^{S}_{1}\times Q^{S}_{T}$. 2. b)

$G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime},x^{\prime}_{T})$ such that $x^{\prime}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ does not exist. From there does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}_{G_{1}}\times Q_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ and $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ and based on Definition 11 it holds that $G_{1}\stackrel{{\scriptstyle P_{G}(s)}}{{\Longrightarrow}}x^{\prime}$ such that $x^{\prime}\in Q^{NS}_{1}$ does not exist. This means $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime},x^{\prime}_{T})$ such that $x^{\prime}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ does not exist.

Therefore, it can be concluded that the $G_{1}\mathbin{\parallel}_{\land}T$ is not current-state opaque. $\blacksquare$

Example 2

Consider automaton $G_{1}$ in Fig. 1 with set of secret states $Q_{1}^{S}=\{s_{1},s_{3}\}$. Consider states $s_{2}$ and $s_{4}$. Both states are non-secret states, $s_{2},s_{4}\in Q^{NS}$, and they have the same future behavior since $s_{2}\stackrel{{\scriptstyle\tau}}{{\rightarrow}}s_{4}$ and $s_{4}\stackrel{{\scriptstyle\varepsilon}}{{\rightarrow}}s_{4}$. Thus, states $s_{2}$ and $s_{4}$ can be merged while preserving opaque observation equivalence. A similar argument holds for $s_{1},s_{3}$. Merging $s_{2}$ and $s_{4}$, and $s_{1}$ and $s_{3}$, results in $\tilde{G_{1}}$ with two less states compared to $G_{1}$; it is shown in Fig. 1.

5.2 Synchronous composition of CSEs

The idea of compositional opacity verification is to abstract the components and construct the current-state estimator (CSE) for each abstracted component and, next, transform opacity verification to compositional nonblocking verification. For this approach to work, it needs to be shown that current-state opacity is preserved by synchronization of individual CSEs, step (ii) in Fig. 2. In the following, Prop. 6 first shows that synchronization of CSEs produces an automaton that is isomorphic with the monolithic CSE of the original system, $det(\mathcal{G})$.111We could not find a proof of this result in the literature. Then, Theorem 7 and Corollary 8 show that the current-state opacity of a system can be verified by constructing the CSEs of individual components and then synchronizing them by using $\mathbin{\parallel}_{\lor}$ or $\mathbin{\parallel}_{\land}$, respectively. As $\mathbin{\parallel}_{\lor}$ is more general compared with $\mathbin{\parallel}_{\land}$, The following proposition has been presented and proved in Chapter 5 of [21], Proposition 5.5.

Proposition 6

[21]** Let $G_{1}=\langle{\Sigma}_{1},\penalty 750Q_{1}^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}_{1}},\penalty 750Q^{\circ}_{1}\rangle$ and $G_{2}=\langle{\Sigma}_{2},\penalty 750Q_{2}^{\vphantom{\circ}},\penalty 750\mathord{\mathord{\stackrel{{\scriptstyle}}{{\rightarrow}}}{}^{\vphantom{\circ}}_{2}},\penalty 750Q^{\circ}_{2}\rangle$ be two non-deterministic automata. Then $det(G_{1}\mathbin{\parallel}G_{2})$ is isomorphic to $det(G_{1})\mathbin{\parallel}det(G_{2})$.

Prop. 6 shows that the CSEs of the components of a system can be constructed individually.222If the system components synchronize also on common unobservable events, then Prop. 6 may not hold. The idea of this paper is to transform the opacity verification problem to compositional nonblocking verification problem. Since the input to compositional nonblocking verification is a set of automata, it is essential for the proposed algorithm to keep the modular structure of the system.

The following theorem shows that current-state opacity is preserved by synchronization of the individual CSEs.

Theorem 7

Let $\mathcal{G}=\{G_{1},\cdots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\lor}$ for interaction, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $det(G_{i})=\langle{\Sigma}_{i},X^{i}_{obs},\stackrel{{\scriptstyle}}{{\rightarrow}}_{i},X_{i}^{\circ}\rangle$ for $1\leq i\leq n$. Then $\mathcal{G}$ is current-state opaque if and only if $det(G_{1})\mathbin{\parallel}_{\lor}\ldots\mathbin{\parallel}_{\lor}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\ldots,X_{n})$ implies $X_{i}\not\subseteq Q_{i}^{S}$ for all $1\leq i\leq n$.

Proof:

Based on Prop. 6, it holds that $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ if and only $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\ldots,X_{n})$ and $(x_{1},\ldots,x_{n})\in X$ if and only if $(x_{1},\ldots,x_{n})\in X_{1}\times\cdots\times X_{n}$. If the system is current-state opaque then for all $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ it holds that $X\not\subseteq Q^{S}$. Since $\mathbin{\parallel}_{\lor}$ is used for composition, this means there exists $(x_{1},\ldots,x_{n})\in X$ such that $x_{i}\in Q^{NS}_{i}$ for all $1\leq i\leq n$. Based on Prop. 6 it holds that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\ldots,X_{n})$ and there exists $(x_{1},\ldots,x_{n})\in X_{1}\times\cdots\times X_{n}$ such that $x_{i}\in Q^{NS}_{i}$ for all $1\leq i\leq n$. This means that $X_{i}\not\subseteq Q^{S}_{i}$ for all $1\leq i\leq n$.

Similarly, assume that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\ldots,X_{n})$ and $X_{i}\not\subseteq Q_{i}^{S}$ for all $1\leq i\leq n$. Since $\mathbin{\parallel}_{\lor}$ is used for composition, this means there exists $(x_{1},\ldots,x_{n})\in X_{1}\times\cdots\times X_{n}$ such that $x_{i}\in Q^{NS}_{i}$ for all $1\leq i\leq n$. Based on Prop. 6 it holds that $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ and there exists $(x_{1},\ldots,x_{n})\in X$ such that $x_{i}\in Q^{NS}_{i}$ for all $1\leq i\leq n$, which implies $X\not\subseteq Q^{S}$. Thus, the system is current-state opaque. $\blacksquare$

Theorem 7 proves that a system is current state opaque if and only if no state of the modular current-state estimator lies entirely in the set of secret states. The set of secret states in Theorem 7 is defined based on $\mathbin{\parallel}_{\lor}$. The following corollary proves that a similar result also holds when $\mathbin{\parallel}_{\land}$ is used for synchronization.

Corollary 8

Let $\mathcal{G}=\{G_{1},\cdots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\land}$ and with set of secret states $Q^{S}=Q_{1}^{S}\times\cdots\times Q_{n}^{S}$ and $det(G_{i})=\langle{\Sigma}_{i},X^{i}_{obs},\stackrel{{\scriptstyle}}{{\rightarrow}}_{i},X_{i}^{\circ}\rangle$ for $1\leq i\leq n$. Then $\mathcal{G}$ is current-state opaque if and only if $det(G_{1})\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ implies $X_{1}\times\cdots\times X_{n}\not\subseteq Q_{1}^{S}\times\cdots\times Q_{n}^{S}$.

Proof:

Based on Prop. 6 it holds that $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ if and only $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and $(x_{1},\cdots,x_{n})\in X$ if and only if $(x_{1},\cdots,x_{n})\in X_{1}\times\cdots\times X_{n}$. If the system is current-state opaque then for all $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ it holds that $X\not\subseteq Q^{S}$, which means that there exists $(x_{1},\cdots,x_{n})\in X$ such that $(x_{1},\ldots,x_{n})\not\in Q^{S}_{1}\times\ldots\times Q^{S}_{n}$. Based on Prop. 6 it holds that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and there exists $(x_{1},\cdots,x_{n})\in X_{1}\times\cdots\times X_{n}$ such that $(x_{1},\ldots,x_{n})\not\in Q^{S}_{1}\times\ldots\times Q^{S}_{n}$. Thus, $X_{1}\times\cdots\times X_{n}\not\subseteq Q^{S}_{1}\times\ldots\times Q^{S}_{n}$.

Similarly assume $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and $X_{1}\times\cdots\times X_{n}\not\subseteq Q^{S}_{1}\times\ldots\times Q^{S}_{n}$. This means that there exists $(x_{1},\ldots,x_{n})\in X_{1}\times\cdots\times X_{n}$ such that $(x_{1},\ldots,x_{n})\not\in Q^{S}_{1}\times\ldots\times Q^{S}_{n}$. Based on Prop. 6 it holds that $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ and there exists $(x_{1},\cdots,x_{n})\in X$ such that $(x_{1},\ldots,x_{n})\not\in Q^{S}_{1}\times\ldots\times Q^{S}_{n}$, which implies $X\not\subset Q^{S}$. Thus, the system is current-state opaque. $\blacksquare$

Example 3

Assume we have the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where the set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}],[s_{2}]\}$ and $Q^{S}_{2}=\{t_{1}\}$. Automaton $\tilde{G}_{1}$ and $G_{2}$ are shown in Fig. 1 and Fig. 3, respectively. Fig. 3 also shows $D=det(\tilde{G}_{1}\mathbin{\parallel}G_{2})$ and $D^{\prime}=det(\tilde{G}_{1})\mathbin{\parallel}det(G_{2})$, where

• •

$D_{0}=\{(s_{0},t_{0})\}$, $D_{1}=\{([s_{1}],t_{1}),([s_{2}],t_{1})\}$ in $D$

• •

$D^{\prime}_{0}=(\{s_{0}\},\{t_{0}\})$, $D^{\prime}_{1}=(\{[s_{1}],[s_{2}]\},\{t_{1}\})$ in $D^{\prime}$.

It can be observed that $D$ and $D^{\prime}$ are isomorphic. If $\mathbin{\parallel}_{\lor}$ is used for synchronization, then $([s_{1}],t_{1})$ and $([s_{2}],t_{1})$ are considered secret states. This means that $D_{1}\subseteq Q^{S}$. Therefore, it can be concluded that $G_{1}\mathbin{\parallel}_{\lor}G_{2}$ is not current-state opaque. Moreover, $([s_{1}],t_{1})$ and $([s_{2}],t_{1})$ are also considered secret if $\mathbin{\parallel}_{\land}$ is used for interaction. Therefore, $G_{1}\mathbin{\parallel}_{\land}G_{2}$ is not current-state opaque.

5.3 Current-state opacity to nonblocking verification

So far, we have shown that the components of a modular system can be abstracted using opaque observation equivalence and the CSEs of individual abstracted components can be built. This section describes the transformation of compositional opacity verification to nonblocking verification, steps (iii) and (iv) in Fig. 2. These steps are done after creating the modular current-state estimators. The compositional approach is well-established for nonblocking verification [11, 12]. A variety of abstraction methods with efficient implementations that preserve the nonblocking property are introduced in [11, 12]. Thus, transforming current-state opacity to nonblocking verification makes it possible to use well-developed algorithms for nonblocking verification. To transform current-state opacity to nonblocking verification, the first step is to identify the states of individual current-state estimators that are violating opacity. These states are considered as $\psi$-states in Def. 3. From these states, transitions to blocking states are added. The system is current-state opaque if and only if the transformed system is nonblocking.

As explained in Sect. 3, the components of the system can interact either by $\mathbin{\parallel}_{\lor}$ or $\mathbin{\parallel}_{\land}$. Therefore, two different transformations are required to reflect this. In the following, Theorem 9 and Corollary 10 formally describe how to transform current-state opacity to nonblocking verification when $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$ are used, respectively.

Theorem 9

Let $\mathcal{G}=\{G_{1},\cdots,G_{n}\}$ be a non-deterministic system, with $\mathbin{\parallel}_{\lor}$ used for interaction, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $det(G_{i})=\langle{\Sigma}_{i},X_{obs}^{i},\stackrel{{\scriptstyle}}{{\rightarrow}}_{i},X_{i}^{\circ}\rangle$. Then $\mathcal{G}$ is not current-state opaque if and only if $det(G_{1})_{\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi_{n}}$ is blocking, where $X_{\psi_{i}}^{i}=\{X\in X_{obs}^{i}\ |\ X\subseteq Q_{i}^{S}\}$.

Proof:

First, assume that $\mathcal{G}$ is not current-state opaque. Based on Theorem 7 it holds that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ such that $X_{i}\subseteq Q_{i}^{S}$ for some $1\leq i\leq n$, which implies $X_{i}\in X_{\psi_{i}}^{i}$. Based on Lemma 24 in Appendix, $det(G_{1})_{\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi_{n}}$ is blocking.

Next, assume that $det(G_{1})_{\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi_{n}}$ is blocking. Then based on Lemma 24 in Appendix, it holds that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ such that $X_{i}\in X_{obs}^{i}$ and $X_{i}\in X_{\psi_{i}}^{i}$ for some $1\leq i\leq n$. This means that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ such that $X_{i}\subseteq Q_{i}^{S}$ for some $1\leq i\leq n$, which based on Theorem 7 implies that $\mathcal{G}$ is not current-state opaque. $\blacksquare$

The following example shows all the steps of compositional current-state opacity verification.

Example 4

Consider the system $\mathcal{G}=\{G_{1},G_{2}\}$, where $G_{1}$ is shown in Fig. 1 and $G_{2}$ is shown in Fig. 3. Assume that the set of secret states of $G_{1}$ and $G_{2}$ are $Q^{S}_{1}=\{s_{1},s_{2},s_{3},s_{4}\}$ and $Q_{2}^{S}=\{t_{1}\}$, respectively. At the first step of the compositional approach, step (i) in Fig 2, each automaton is abstracted using opaque observation equivalence. Thus, $G_{1}$ is replaced by $\tilde{G}_{1}$, shown in Fig. 1, and $G_{2}$ can not be abstracted. Automaton $\tilde{G}_{1}$ has set of secret states $\tilde{Q}^{S}_{1}=\{[s_{1}],[s_{2}]\}$. Next, $det(\tilde{G}_{1})$ and $det(G_{2})$ are constructed, step (ii) in Fig. 2. Fig. 3 shows $det(\tilde{G}_{1})$ and since $G_{2}$ is deterministic, $det(G_{2})=G_{2}$. The next step in the compositional approach is to transform opacity verification to nonblocking verification by building the $\psi$-automata of the individual components, step (iii) in Fig. 2. Assume that $\mathbin{\parallel}_{\lor}$ is used for interaction. As $\{[s_{1}],[s_{2}]\}\subseteq Q^{S}_{1}$ in $det(\tilde{G_{1}})$ and $\{t_{1}\}\subseteq Q^{S}_{2}$ in $det(G_{2})$, it follows that $X_{\psi_{1}}^{1}=\{\{[s_{1}],[s_{2}]\}\}$ and $X_{\psi_{2}}^{2}=\{\{t_{1}\}\}$. The $\psi$-automata of $det(\tilde{G}_{1})$ and $det(G_{2})$ are shown in Fig. 4 as $O_{1}$ and $O_{2}$, respectively. The transformed system is blocking as $O_{1}\mathbin{\parallel}O_{2}\xrightarrow{\alpha\psi_{1}}{\mathord{\perp}}$, step (iv) in Fig. 2. Thus, we can conclude that the original system is not current-state opaque when $\mathbin{\parallel}_{\lor}$ is used for interaction. Indeed, the system is not current-state opaque as if $\alpha$ occurs in the monolithic system, then $G_{1}\mathbin{\parallel}_{\lor}G_{2}$ goes to the secret states $(s_{1},t_{1})$ or $(s_{2},t_{1})$, from where there is no possible denial.

Corollary 10

Let $\mathcal{G}=\{G_{1},\cdots,G_{n}\}$ be a non-deterministic system, with $\mathbin{\parallel}_{\land}$ used for interaction, where the set of secret states is $Q^{S}=Q_{1}^{S}\times\cdots\times Q_{n}^{S}$. Let $det(G_{i})=\langle{\Sigma}_{i},X_{obs}^{i},\stackrel{{\scriptstyle}}{{\rightarrow}}_{i},X_{i}^{\circ}\rangle$. Then $\mathcal{G}$ is not current-state opaque if and only if $det(G_{1})_{\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi}$ is blocking, where $X_{\psi}^{i}=\{X\in X_{obs}^{i}\ |\ X\subseteq Q_{i}^{S}\}$.

Proof:

First assume $\mathcal{G}$ is not current-state opaque. Based on Definition 6 it holds that there exists $s\in{\Sigma}^{*}$ such that $det(\mathcal{G})\stackrel{{\scriptstyle s}}{{\rightarrow}}X$ and $X\subseteq Q^{S}$. Based on Prop. 6 $det(\mathcal{G})$ is isomorphic to $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})$. Thus, $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and $X_{1}\times\cdots\times X_{n}\subseteq Q_{1}^{S}\times\ldots\times Q_{n}^{S}$, which implies $X_{i}\subseteq Q_{i}^{S}$ for all $1\leq i\leq n$. Thus, it holds that $X_{1}\times\cdots\times X_{n}\subseteq X_{\psi}^{1}\times\cdots\times X_{\psi}^{n}$. Based on Lemma 25, $det(G_{1})_{\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi}$ is blocking.

Now assume $det(G_{1})_{\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})_{\psi}$ is blocking. Then based on Lemma 25 it holds that $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and $X_{1}\times\cdots\times X_{n}\subseteq X_{\psi}^{1}\times\cdots\times X_{\psi}^{n}$. This means $det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n})\stackrel{{\scriptstyle s}}{{\rightarrow}}(X_{1},\cdots,X_{n})$ and $X_{i}\subseteq Q_{i}^{S}$ for all $1\leq i\leq n$, which implies that $\mathcal{G}$ is not current-state opaque. $\blacksquare$

The main difference between Theorem 9 and Corollary 10 is in generating the $\psi$-automata of the individual components. When $\mathbin{\parallel}_{\lor}$ is used for composition, then the system is not current-state opaque if at least one state of the composed states is secret. To capture this feature, individual components $G_{i}$ have different $\psi_{i}$-transitions. This guarantees that if the transformed system is blocking, then there is a composed state in the original system with at least one secret state. In contrast, when $\mathbin{\parallel}_{\land}$ is used for interaction, a composed state is considered secret if all the states are secret. To assure this, in the transformed system all the components have the same $\psi$-transitions. Thus, the $\psi$-transitions happen if and only if they happen in all the components simultaneously.

Example 5

Consider again the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ is shown in Fig. 1 and $G_{2}$ is shown in Fig. 3. Assume that the set of secret states of $\tilde{G}_{1}$ and $G_{2}$ are $\tilde{Q}^{S}_{1}=\{[s_{1}],[s_{2}]\}$ and $Q_{2}^{S}=\{t_{1}\}$, respectively. Now, assume that $\mathbin{\parallel}_{\land}$ is used for interaction. Similarly to Example 4, we have that $X_{\psi}^{1}=\{\{[s_{1}],[s_{2}]\}\}$ and $X_{\psi}^{2}=\{\{t_{1}\}\}$. In contrast to Example 4, to generate the $\psi$-automata when $\mathbin{\parallel}_{\land}$ is used for interaction, all the transitions to ${\mathord{\perp}}$ are labeled by the same $\psi$ event. The $\psi$-automata of $det(\tilde{G}_{1})$ and $det(G_{2})$ are shown in Fig. 4 as $O^{\prime}_{1}$ and $O^{\prime}_{2}$, respectively. The $\psi$-system is blocking as $O^{\prime}_{1}\mathbin{\parallel}O^{\prime}_{2}\xrightarrow{\alpha\psi}{\mathord{\perp}}$. Thus, we can conclude that the original system is not current-state opaque when $\mathbin{\parallel}_{\land}$ is used for interaction.

6 Compositional infinite-step opacity verification

This section discusses the compositional approach for infinite-step opacity verification. In the compositional infinite-step opacity verification individual components are first abstracted. Next, the two-way observers [17] of components are generated and finally the infinite-step opacity verification is transformed to the compositional nonblocking verification. In the following, Section 6.1 explains how individual components can be abstracted before building the modular two-way observers. Next, Section 6.2 establishes a link between the modular two-way observers and the monolithic two-way observer. Section 6.3 shows the transformation of the infinite-step opacity verification to nonblocking verification when $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$ is used for interaction.

6.1 Opaque observation equivalence

As explained in Section 4, the first step of the compositional infinite-step opacity is to abstract the components using opaque observation equivalence. In the following Theorem 11 and Corollary 12 show that opaque observation equivalence preserves infinite-step opacity when $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$ are used for interaction, respectively. Theorem 11 and Corollary 12 are similar to Theorem 4 and Corollary 5 presented in Section 5.1, and accordingly, they have similar proofs.

Theorem 11

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\lor}$ for interaction, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is infinite-step opaque if and only if $\tilde{\mathcal{G}}$ is infinite-step opaque.

Proof:

Assume $T=G_{2}\mathbin{\parallel}_{\lor}\ldots\mathbin{\parallel}_{\lor}G_{n}$ with set of secret states $Q^{S}_{T}$ and set of non secret states $Q_{T}^{NS}=Q_{T}\setminus Q_{T}^{S}$. Then $Q^{S}_{T}=Q^{T}\setminus Q_{T}^{NS}$, where $Q_{T}^{NS}=Q^{NS}_{2}\times\ldots\times Q^{NS}_{n}$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque then $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque either and vice versa.

1. (i)

First assume that $G_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque. Then there exists $(x^{0}_{G},x^{0}_{T})\in Q^{\circ}_{G_{1}}\times Q^{\circ}_{T}$ and $st\in\mathcal{L}({G_{1}}\mathbin{\parallel}_{\lor}T,(x^{0}_{G},x^{0}_{T}))$ such that $(x^{0}_{G},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, and $x_{1}\in Q_{G_{1}}^{S}$ or $x_{T}\in Q_{T}^{S}$, and one of the following holds.

• •

For all $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$ then ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$.

Since ${G_{1}}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\sim{G_{1}}\mathbin{\parallel}_{\lor}T$. This means, if ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{G_{1}}\times Q^{NS}_{T}$ if and only if $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$. Thus, $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque either.

Now consider the case when $G_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque because $(x^{0}_{G},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, and $x_{1}\in Q_{G_{1}}^{S}$ or $x_{T}\in Q_{T}^{S}$ and there does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$. The proof for this part is the same as the proof for Theorem 4 in Section 5.1, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted. 2. (ii)

If $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque. Then there exists $([x_{G}^{0}],x_{T}^{0})\in\tilde{Q}^{\circ}_{G_{1}}\times Q_{T}^{\circ}$ and $st\in\mathcal{L}(\tilde{G}_{1}\mathbin{\parallel}_{\lor}T,([x^{0}_{G}],x^{0}_{T}))$ such that $([x^{0}_{G}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, and $[x_{1}]\in\tilde{Q}_{G_{1}}^{S}$ or $x_{T}\in Q_{T}^{S}$, and one of the following cases holds.

• •

For all $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ then $\tilde{G}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$.

Since ${G_{1}}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\sim G\mathbin{\parallel}_{\lor}T$. This means, if $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then ${G_{1}}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{G_{1}}\times Q^{NS}_{T}$ if and only if $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$. Thus, ${G_{1}}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque either.

Now consider the case when $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not infinite-step opaque because $([x^{0}_{G}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, and $[x_{1}]\in\tilde{Q}_{G_{1}}^{S}$ or $x_{T}\in Q_{T}^{S}$ and there does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$. Again the proof for this part is the same as the proof for Theorem 4 in Section 5.1, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted. $\blacksquare$

In the theorem $\sim_{inf}$ refers to infinite-step opaque equivalence definite in Section 5.

Corollary 12

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\land}$ for interaction and with the set of secret states $Q^{S}=Q_{1}^{S}\times\ldots\times Q_{n}^{S}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is infinite-step opaque if and only if $\tilde{\mathcal{G}}$ is infinite-step opaque.

Proof:

Assume $T=G_{2}\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}G_{n}$ with set of secret states $Q^{S}_{T}$ and set of non secret states $Q_{T}^{NS}=Q_{T}\setminus Q_{T}^{S}$. Then $Q^{S}_{T}=Q^{T}\setminus Q_{T}^{NS}$, where $Q_{T}^{S}=Q^{S}_{2}\times\ldots\times Q^{S}_{n}$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque either and vice versa.

1. (i)

First assume that $G_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque. Then there exists $(x^{0}_{G},x^{0}_{T})\in Q^{\circ}_{G_{1}}\times Q^{\circ}_{T}$ and $st\in\mathcal{L}(G_{1}\mathbin{\parallel}_{\land}T,(x^{0}_{G},x^{0}_{T}))$ such that $(x^{0}_{G},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, and $(x_{1},x_{T})\in Q_{G_{1}}^{S}\times Q_{T}^{S}$, and one of the following holds.

• •

For all $(x^{\prime}_{1},x^{\prime}_{T})$ such that $x^{\prime}_{1}\in Q^{NS}_{G_{1}}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ and ${G_{1}}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$ then ${G_{1}}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $x^{\prime}_{1}\in Q^{NS}_{G_{1}}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$.

Since ${G_{1}}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\sim G_{1}\mathbin{\parallel}_{\land}T$. This means, if $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $x^{\prime}_{1}\in Q^{NS}_{G_{1}}$ if and only if $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{G_{1}}$. Thus, $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque either.

Now consider the case, where $(x_{1},x_{T})\in Q_{G_{1}}\times Q_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$ and $(x_{1},x_{T})\in Q_{G_{1}}^{S}\times Q_{T}^{S}$, and there does not exist $x^{\prime}_{1}\in Q^{NS}_{G_{1}}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that ${G_{1}}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$. The proof for this part is the same as the proof for Corollary 5, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted.

Therefore, it can be concluded that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque. 2. (ii)

If $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque. Then there exists $([x_{G}^{0}],x_{T}^{0})\in\tilde{Q}^{\circ}_{G_{1}}\times Q_{T}^{\circ}$ and $st\in\mathcal{L}(\tilde{G}_{1}\mathbin{\parallel}_{\land}T,([x^{0}_{G}],x^{0}_{T}))$ such that $([x^{0}_{G}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, and $([x_{1}],x_{T})\in\tilde{Q}_{G_{1}}^{S}\times Q_{T}^{S}$, and one of the following cases holds.

• •

For all $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}_{G_{1}}\times Q_{T}$ such that $[x^{\prime}_{1}]\in\tilde{Q}^{NS}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ and $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$.

Since $G\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\sim G_{1}\mathbin{\parallel}_{\land}T$. This means, if $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $x^{\prime}_{1}\in Q^{NS}_{G_{1}}$ if and only if $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{G_{1}}\times Q^{NS}$. Thus, $G_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque either.

Now consider the case where, $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not infinite-step opaque because there exists $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$ such that $([x_{1}],x_{T})\in\tilde{Q}_{G_{1}}^{S}\times Q_{T}^{S}$ and $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\not\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ such that $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{G_{1}}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$. Again the proof for this part is the same as the proof for Corollary 5, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted.

Therefore, it can be concluded that the $G\mathbin{\parallel}_{\land}T$ is not infinite-step opaque. $\blacksquare$

6.2 Synchronous composition of two-way observers

It has been shown in [17] that a two-way observer can be used to verify infinite-step opacity. In order to monolithically verify the infinite-step opacity of a modular system the monolithic representation of whole system is generated first. Next, the two-way observer of the system is constructed, see Definition 9. This approach requires generating two observer automata for two potentially large components, which maybe intractable. The compositional approach on the other hand, avoids constructing the monolithic two-way observer of the system. Instead, the two-way observers of the components are built individually. However, the monolithic two-way observer of the system is a subautomaton of the composed individual two-way observers. This is shown in Proposition 13.

Proposition 13

Let $G_{1}$ and $G_{2}$ be two non-deterministic automata. Let $G_{i,R}$ be the reversed automaton of $G_{i}$ for $i=1,2$ and let $G_{R}$ be the reversed automaton of $G_{1}\mathbin{\parallel}G_{2}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$. Let $H_{i}=\Delta(det(G_{i}))\mathbin{\parallel}\Delta_{R}(det(G_{i,R}))$ for $i=1,2$ and $H=\Delta(det(G_{1}\mathbin{\parallel}G_{2}))\mathbin{\parallel}\Delta_{R}(det(G_{R}))$. Then $H\sqsubseteq H_{1}\mathbin{\parallel}H_{2}$, which means that if $H\stackrel{{\scriptstyle s}}{{\rightarrow}}(X,X_{R})\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}(Y,Y_{R})$ in $H$ then $H_{1}\mathbin{\parallel}H_{2}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),(X^{2},X^{2}_{R}))\stackrel{{\scriptstyle\sigma}}{{\rightarrow}}((Y^{1},Y^{1}_{R}),(Y^{2},Y^{2}_{R}))$ in $H_{1}\mathbin{\parallel}H_{2}$ such that $X_{R}\subset X^{1}_{R}\times X^{2}_{R}$ and $Y_{R}\subseteq Y^{1}_{R}\times Y^{2}_{R}$.

Proof:

Based on Lemma 26 in Appendix, it holds that $\Delta(det(G_{1}))\mathbin{\parallel}\Delta(det(G_{2}))=\Delta(det(G_{1})\mathbin{\parallel}det(G_{2}))$, and based on Prop. 6, $\Delta(det(G_{1})\mathbin{\parallel}det(G_{2}))$ and $\Delta(det(G_{1}\mathbin{\parallel}G_{2}))$ are isomorphic. Thus, it is enough to show that $\Delta_{R}(det(G_{R}))\sqsubseteq\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\Delta_{R}(det(G_{2,R}))$. Moreover, based on Lemma 26, it holds that $\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\Delta_{R}(det(G_{2,R}))=\Delta_{R}(det(G_{1,R})\mathbin{\parallel}det(G_{2,R}))$. Thus, it is enough to show that $det(G_{R})\sqsubseteq det(G_{1,R})\mathbin{\parallel}det(G_{2,R})$.

It is shown by induction on $n\geq 0$ that $X^{0}\stackrel{{\scriptstyle\sigma_{1}}}{{\rightarrow}}X^{1}\stackrel{{\scriptstyle\sigma_{2}}}{{\rightarrow}}\ldots\stackrel{{\scriptstyle\sigma_{n}}}{{\rightarrow}}X_{n}$ in $det(G_{R})$ if $(X^{0}_{1},X^{0}_{2})\stackrel{{\scriptstyle\sigma_{1}}}{{\rightarrow}}(X_{1}^{1},X_{2}^{1})\stackrel{{\scriptstyle\sigma_{2}}}{{\rightarrow}}\ldots\stackrel{{\scriptstyle\sigma_{n}}}{{\rightarrow}}(X_{1}^{n},X_{2}^{n})$ in $det(G_{1,R})\mathbin{\parallel}det(G_{2,R})$ such that $(x_{1},x_{2})\in X^{j}$ if $(x_{1},x_{2})\in X^{j}_{1}\times X^{j}_{2}$.

Base case: $n=0$. Let $X_{R}^{\circ}$ be the initial state of $det(G_{R})$ and $X_{i,R}^{\circ}$ be the initial state of $det(G_{i,R})$ for $i=1,2$. If $(x_{1},x_{2})\in X_{R}^{\circ}$, then as all the states of $G_{R}$ are considered as initial states it holds that $(x_{1},x_{2})$ is a reachable state, which means that $G_{1}\mathbin{\parallel}G_{2}\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{2})$. Based on Def. 2, it holds that $G_{i}\stackrel{{\scriptstyle P_{i}(s)}}{{\Longrightarrow}}x_{i}$ in $G_{i}$ for $i=1,2$. Based on the definition of the reversed automaton, all the states of $G_{i,R}$ for $i=1,2$ are considered as initial states, which implies that $x_{i}\in Q^{\circ}_{{i,R}}$ for $i=1,2$, . Thus, $(x_{1},x_{2})\in Q^{\circ}_{{1,R}}\times Q^{\circ}_{{2,R}}$, which means that $(x_{1},x_{2})\in X_{1,R}^{\circ}\times X_{2,R}^{\circ}$.

Inductive step: Assume that the claim holds for some $n\geq 0$, i.e, $X_{R}^{\circ}=X^{0}\xrightarrow{\sigma_{1}\sigma_{2}\ldots\sigma_{n}}X^{n}=X$ in $det(G_{R})$ if $(X_{1,R}^{\circ},X_{2,R}^{\circ})=(X_{1}^{0},X_{2}^{0})\xrightarrow{\sigma_{1}\sigma_{2}\ldots\sigma_{n}}(X^{n}_{1},X^{n}_{2})=(X_{1},X_{2})$ in $det(G_{1,R})\mathbin{\parallel}det(G_{2,R})$, and $(x_{1},x_{2})\in X^{k}$ if $(x_{1},x_{2})\in X^{k}_{1}\times X^{k}_{2}$ for all $0\leq k<n$. It must be shown that if $X=X^{n}\xrightarrow{\sigma_{n+1}}Y$ in $det(G_{R})$, then $(X_{1},X_{2})=(X^{n}_{1},X^{n}_{2})\xrightarrow{\sigma_{n+1}}(Y_{1},Y_{2})$ in $det(G_{1,R})\mathbin{\parallel}det(G_{2,R})$, and if $(x_{1},x_{2})\in X$, then $(x_{1},x_{2})\in X_{1}\times X_{2}$.

Let $det(G_{R})\xrightarrow{\sigma_{1}\ldots\sigma_{n}}X^{n}=X\xrightarrow{\sigma_{n+1}}Y$ in $det(G_{R})$ and $(x_{1},x_{2})\in X$. Then based on $UR(x)$ it follows that $(x_{1},x_{2})=(x_{1}^{1},x_{2}^{1})\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}(x_{1}^{r},x_{2}^{t})\xrightarrow{\sigma_{n+1}}(y_{1},y_{2})$ in $G_{R}$. Since $(y_{1},y_{2})$ is a reachable state in $G_{R}$, it holds that there exists $s\in({\Sigma}_{1}\cup{\Sigma}_{2})^{*}$ such that $G_{1}\mathbin{\parallel}G_{2}\stackrel{{\scriptstyle s}}{{\Rightarrow}}(y_{1},y_{2})\xrightarrow{\sigma_{n+1}}(x_{1}^{r},x_{2}^{t})\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}(x_{1}^{1},x_{2}^{1})$. Based on Def. 2, it holds that $G_{1}\stackrel{{\scriptstyle P_{1}(s)}}{{\Longrightarrow}}y_{1}\xrightarrow{P_{1}(\sigma_{n+1})}x_{1}^{r}\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}x_{1}^{1}$ in $G_{1}$ and $G_{2}\stackrel{{\scriptstyle P_{2}(s)}}{{\Longrightarrow}}y_{2}\xrightarrow{P_{2}(\sigma_{n+1})}x_{2}^{t}\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}x_{2}^{1}$ in $G_{2}$. This means that $x_{1}^{1}\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}x_{1}^{r}\xrightarrow{P_{1}(\sigma_{n+1})}y_{1}$ in $G_{1,R}$ and $x_{2}^{1}\stackrel{{\scriptstyle\tau}}{{\Rightarrow}}x_{2}^{t}\xrightarrow{P_{2}(\sigma_{n+1})}y_{2}$ in $G_{2,R}$. Then based on $UR(x)$ and the inductive hypothesis, it holds that $det(G_{1,R})\xrightarrow{P_{1}(\sigma_{1}\sigma_{2}\ldots\sigma_{n})}X_{1}\xrightarrow{P_{1}(\sigma_{n+1})}Y_{1}$ and $det(G_{2,R})\xrightarrow{P_{2}(\sigma_{1}\sigma_{2}\ldots\sigma_{n})}X_{2}\xrightarrow{P_{2}(\sigma_{n+1})}Y_{2}$. Moreover, based on $UR(x)$ it holds that $x_{1}\in X_{1}$ and $x_{2}\in X_{2}$. Then based on Def. 2 it holds that $det(G_{1,R})\mathbin{\parallel}det(G_{2,R})\xrightarrow{\sigma_{1}\sigma_{2}\ldots\sigma_{n}}(X_{1},X_{2})\xrightarrow{\sigma_{n+1}}(Y_{1},Y_{2})$. Thus, $(X_{1},X_{2})\xrightarrow{\sigma_{n+1}}(Y_{1},Y_{2})$ in $det(G_{1,R})\mathbin{\parallel}det(G_{2,R})$ and $(x_{1},x_{2})\in X_{1}\times X_{2}$. $\blacksquare$

Proposition 13 only establishes that the monolithic two-way observer of a modular system is a subautomaton of the synchronous product of the individual two-way observers but in contrast to Proposition 6 the isomorphism does not hold in general. The reason is when the monolithic representation of the system is built some combinations of states become unreachable, or some transitions become disabled. However, those unreachable states may become reachable when individual reverse automata are composed. This happens because in the reversed automaton all the states are considered as initial state and consequently reachable states. This over approximation may cause some unreachable states that are violating the infinite-step opacity to become reachable. Therefore, the verification results may return incorrect violation of infinite-step opacity. This is shown in Example 6.

Theorem 14

*Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a nondeterministic system with $\mathbin{\parallel}_{\lor}$ for interaction, where each automaton has the set of secret states $Q_{i}^{S}$. Then the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$. If *

[TABLE]

then $\mathcal{G}$ is infinite-step opaque.

Proof:

First, based on Proposition 6, Proposition 13 and Lemma 26 it holds that $H=\Delta(det(\mathcal{G}))\mathbin{\parallel}\Delta_{R}(det(\mathcal{G}_{R}))\sqsubseteq[\Delta(det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}]$.

Assume that

[TABLE]

Since $\mathbin{\parallel}_{\lor}$ is used for interaction, from $(X^{i}\cap X^{i}_{R})\not\subseteq Q_{i}^{S}$ or $(X^{i}\cap X_{R}^{i})=\emptyset$ for all $1\leq i\leq n$ it follows that $((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))\not\subseteq Q^{S}$ or $((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))=\emptyset$. Therefore, equation (7) can be rewritten as

[TABLE]

Based on Prop. 13 if $H\stackrel{{\scriptstyle s}}{{\rightarrow}}(X,X_{R})$ it holds that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\ldots,(X^{n},X_{R}^{n}))$ and $X_{R}\subseteq X^{1}_{R}\times\ldots\times X_{R}^{n}$ and based on Prop. 6 it holds that $X=X^{1}\times\ldots\times X^{n}$. This implies $(X\cap X_{R})\subseteq(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})$.

Therefore, equation (6.2) can be rewritten as

[TABLE]

Thus, the system is infinite-step opaque. $\blacksquare$

Example 6

Consider the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ and $G_{2}$ are shown in Figure 1 and Figure 3 respectively. The set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$ and $G_{2}$ is $Q^{S}_{2}=\emptyset$. Assume $\mathbin{\parallel}_{\lor}$ is used for interaction. The two-way observer of $\tilde{G_{1}}$ is $\tilde{H}_{1}$ and the two-way observer of $G_{2}$ is $H_{2}$. Automaton $\tilde{H}_{1}$ is similar to $H_{1}$ shown in Figure 1, where

• •

$A=(\{s_{0}\},\{s_{0},[s_{1}],[s_{2}],s_{5}\})$,

• •

$B=(\{s_{0}\},\{s_{0}\})$,

• •

$C=(\{s_{0}\},\{[s_{1}]\})$,

• •

$D=(\{[s_{1}],[s_{2}]\},\{s_{0},[s_{1}],[s_{2}],s_{5}\})$,

• •

$E=(\{[s_{1}],[s_{2}]\},\{s_{0}\})$,

• •

$F=(\{[s_{1}],[s_{2}]\},\{[s_{1}]\})$,

• •

$I=(\{s_{5}\},\{s_{0},[s_{1}],[s_{2}],s_{5}\})$,

• •

$J=(\{s_{5}\},\{s_{0}\})$,

• •

$K=(\{s_{5}\},\{[s_{1}]\})$.

Figure 5 shows $H_{2}$, where

• •

$A^{\prime}=(\{t_{0}\},\{t_{0},t_{1}\})$,

• •

$B^{\prime}=(\{t_{1}\},\{t_{0},t_{1}\})$,

• •

$C^{\prime}=(\{t_{0}\},\{t_{1}\})$,

• •

$D^{\prime}=(\{t_{1}\},\{t_{1}\})$,

• •

$E^{\prime}=(\{t_{0}\},\{t_{0}\})$,

• •

$F^{\prime}=(\{t_{1}\},\{t_{0}\})$.

The monolithic approach to verify infinite-step opacity of the system is to build $\mathcal{G}=\tilde{G}_{1}\mathbin{\parallel}_{\lor}G_{2}$ and then build the two-way observer of the system $\mathcal{G}$, which is shown in Figure 5 as $H$. In the automaton $H$ the states are:

• •

$W_{1}=((\{(s_{0},t_{0})\},\{(s_{0},t_{0}),([s_{1}],t_{1}),([s_{2}],t_{1})\})$,

• •

$W_{2}=(\{([s_{1}],t_{1}),([s_{2}],t_{1})\},\{(s_{0},t_{0}),([s_{1}],t_{1})$* $,([s_{2}],t_{1})\})$,*

• •

$W_{3}=(\{(s_{0},t_{0})\},\{(s_{0},t_{0})\})$,

• •

$W_{4}=(\{([s_{1}],t_{1}),([s_{2}],t_{1})\},\{(s_{0},t_{0})\})$,

• •

$W_{5}=((\{(s_{0},t_{0})\},\{([s_{1}],t_{1}),([s_{2}],t_{1})\})$,

• •

$W_{6}=(\{([s_{1}],t_{1}),([s_{2}],t_{1})\},\{([s_{1}],t_{1}),([s_{2}],t_{1})\})$,

Let $W_{i}=(q_{i},p_{i})$ for automaton $H$. As it can be seen, $q_{i}\cap p_{i}=\{(s_{0},t_{0})\}\not\subseteq Q^{S}$ when $i=1,3$, and $q_{i}\cap p_{i}=\emptyset$ when $i=4,5$, and $q_{i}\cap p_{i}=\{([s_{1}],t_{1}),([s_{2}],t_{1})\}\not\subseteq Q^{S}$ when $i=2,6$. Therefore, the system is infinite-step opaque. The modular two-way observer of the system is $H_{1}\mathbin{\parallel}H_{2}$ shown in Figure 5. The condition of Theorem 14 does not hold for the state $(F,F^{\prime})$ in $H_{1}\mathbin{\parallel}H_{2}$ since for the state $F$ in $H_{1}$ we have $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$. Therefore, from $H_{1}\mathbin{\parallel}H_{2}$ it can not be concluded that the system is infinite-step opaque.

Corollary 15

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}G_{n}$ be a nondeterministic system, with the set of secret states $Q_{\mathcal{G}}^{S}=Q_{1}^{S}\times\cdots\times Q_{n}^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$.

*If *

[TABLE]

then $\mathcal{G}$ is infinite-step opaque.

Proof:

First, based on Proposition 6, Proposition 13 and Lemma 26 it holds that $H=\Delta(det(\mathcal{G}))\mathbin{\parallel}\Delta_{R}(det(\mathcal{G}_{R}))\sqsubseteq[\Delta(det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}]$.

Assume that

[TABLE]

Since $\mathbin{\parallel}_{\land}$ is used for interaction, from there exist $(X^{i},X_{R}^{i})$ such that $(X^{i}\cap X^{i}_{R})\not\subseteq Q_{i}^{S}$ or $(X^{i}\cap X_{R}^{i})=\emptyset$ it follows that $((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))\not\subseteq Q^{S}$ or $((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))=\emptyset$. Therefore, equation (6.2) can be rewritten as

[TABLE]

Based on Prop. 13 if $H\stackrel{{\scriptstyle s}}{{\rightarrow}}(X,X_{R})$ it holds that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\ldots,(X^{n},X_{R}^{n}))$ and $X_{R}\subseteq X^{1}_{R}\times\ldots\times X_{R}^{n}$ and based on Prop. 6 it holds that $X=X^{1}\times\ldots\times X^{n}$. This implies $(X\cap X_{R})\subseteq(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})$. Therefore, equation (6.2) can be rewritten as

[TABLE]

Thus, the system is infinite-step opaque. $\blacksquare$

Example 7

Consider again the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ and $G_{2}$ are shown in Figure 1 and Figure 3 respectively. The set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$ and $G_{2}$ is $Q^{S}_{2}=\emptyset$. Now, assume $\mathbin{\parallel}_{\land}$ is used for interaction. The problematic state $(F,F^{\prime})$ in $H_{1}\mathbin{\parallel}H_{2}$ is no longer violating the condition of Corollary 15 since for $F^{\prime}$ we have $(\{t_{0}\}\cap\{t_{1}\})=\emptyset$. Therefore, the condition of Corollary 15 holds for all the state of $H_{1}\mathbin{\parallel}H_{2}$. Thus, by analyzing the states of $H_{1}\mathbin{\parallel}H_{2}$, it can be concluded that the system is infinite-step opaque.

6.3 Infinite-step opacity to nonblocking verification

The main idea of this paper is to transform the opacity verification problem to nonblocking verification and use the existing verification algorithms. To do so, the $\psi$-automata of the two-way observers of the system components need to be generated. In the following, Theorem 16 and Corollary 17 show how $\psi$-automaton can be generated when $\mathbin{\parallel}_{\lor}$ and $\mathbin{\parallel}_{\land}$ are used for interaction, respectively.

Theorem 16

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\lor}\ldots\mathbin{\parallel}_{\lor}G_{n}$ be a nondeterministic system, with the set of non-secret states $Q_{\mathcal{G}}^{NS}=Q_{1}^{NS}\times\cdots\times Q_{n}^{NS}$ and the set of secret states $Q^{S}=Q\setminus Q^{NS}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$. If $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}$ is noblocking, where $X_{\psi,i}^{i}=\{(X^{i},X^{i}_{R})\in X_{H_{i}}\ |\ (X^{i}\cap X^{i}_{R})\subseteq Q_{i}^{S}\}$, then the system $\mathcal{G}$ is infinite-step opaque.

Proof:

Assume $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}$ is nonblocking. As all the states of $H_{i,\psi_{i}}$ for all $1\leq i\leq n$ except ${\mathord{\perp}}$ are marked this means there does not exist $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\cdots,(X^{n},X^{n}_{R}))\stackrel{{\scriptstyle\psi_{i}}}{{\rightarrow}}{\mathord{\perp}}$, which implies $(X^{i},X^{i}_{R})\not\in X_{\psi}^{i}$ for all $1\leq i\leq n$. Thus, for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ it holds that $\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\cdots,(X^{n},X^{n}_{R}))$, where $(X^{i}\cap X^{i}_{R})\not\subseteq Q_{i}^{S}$ or $X^{i}\cap X^{i}_{R}=\emptyset$ for all $1\leq i\leq n$. Therefore, based on Theorem 14 the system is infinite-step opaque. $\blacksquare$

To generate $\psi$-automata of individual two-way observers, at the states of the two-way observers in which infinite-step opacity is violated the $\psi_{i}$-transition to blocking states are added. This transforms verification of infinite-step opacity to nonblocking problem. If the results of the verification is nonblocking then the system is infinite-step opaque. However, if the results is blocking the verification software tools like Supremica [18] will return a counter example. By the help of the counter example it is possible to verify if the blocking is caused due to the over approximation. If this is the case, the problematic state can be removed and the system can be verified again, otherwise it can be concluded that the system is not infinite-step opaque.

Example 8

Consider the system $\mathcal{G}=\{G_{1},G_{2}\}$, where $G_{1}$ and $G_{2}$ are shown in Figure 1 and Figure 3 respectively. The set of secret states of $G_{1}$ is $Q^{S}_{1}=\{s_{1},s_{3}\}$ and $G_{2}$ is $Q^{S}_{2}=\emptyset$. Assume $\mathbin{\parallel}_{\lor}$ is used for interaction. At the first step of the compositional approach individual components are abstracted using opaque observation equivalence. This results in the abstracted system $\tilde{\mathcal{G}}=\{\tilde{G}_{1},G_{2}\}$ with $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$. $\tilde{G}_{1}$ is shown in Figure 1. After that, the two-way observers of the abstracted components are generated. As explained in Example 6 the two-way observer of $\tilde{G_{1}}$ is $\tilde{H}_{1}$ and the two-way observer of $G_{2}$ is $H_{2}$ shown Figures 1 and 5. Next, the infinite-step opacity verification is transformed to nonblocking verification by generating $\psi_{i}$-automaton for each $H_{i}$. For the two-way observer $H_{1}$ we have $X_{\psi_{1}}^{1}=\{F\}$ since for the state $F$ it holds that $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$. For the two-way observer $H_{2}$ we have $X_{\psi_{2}}^{2}=\emptyset$. Figure 6 shows the $H_{1,\psi_{1}}$. The system $H_{1,\psi_{1}}\mathbin{\parallel}H_{2,\psi_{2}}$ is blocking since $H_{1,\psi_{1}}\mathbin{\parallel}H_{2,\psi_{2}}\xrightarrow{(\alpha,\epsilon)(\epsilon,\beta)}(F,F^{\prime})\stackrel{{\scriptstyle\psi_{1}}}{{\rightarrow}}{\mathord{\perp}}$. Thus, no conclusion can be drawn about the infinite-step opacity of the system. The problem of over approximation is caused by the reverse automata of the two-way observer. From $\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\Delta(det(G_{2}))\mathbin{\parallel}\Delta_{R}(det(G_{2,R}))\xrightarrow{(\alpha,\epsilon)(\epsilon,\beta)}(F,F^{\prime})=((\{[s_{1}],[s_{2}]\},\{[s_{1}]\}),(\{t_{1}\},\{t_{0}\}))$ it follows that $\Delta_{R}(G_{1,R})\mathbin{\parallel}\Delta_{R}(G_{2,R})\xrightarrow{(\epsilon,\beta)}(\{[s_{1}]\},\{t_{0}\})$. Thus, to verify if this is a valid violation of opacity, it needs to be analyzed if state $([s_{1}],t_{0})$ is a reachable state in $G_{1}\mathbin{\parallel}G_{2}$. Since $G_{1}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}[s_{1}]$ and $G_{2}\not\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}t_{0}$ it can be concluded that $([s_{1}],t_{0})$ is not a reachable state in $G_{1}\mathbin{\parallel}G_{2}$. Thus, it can be concluded that the violation is due to the over approximation. Thus, the system is finite-step opaque.

Corollary 17

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}G_{n}$ be a nondeterministic system, with the set of secret states $Q_{\mathcal{G}}^{S}=Q_{1}^{S}\times\cdots\times Q_{n}^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$. If $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}$ is nonblocking, where $X_{\psi,i}^{i}=\{(X^{i},X^{i}_{R})\in X_{H_{i}}\ |\ (X^{i}\cap X^{i}_{R})\subseteq Q_{i}^{S}\}$, then the system $\mathcal{G}$ is infinite-step opaque.

Proof:

Assume $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}$ is nonblocking. As all the sates of $H_{i}$ for all $1\leq i\leq n$ are marked this means there does not exist $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X_{1},Y_{1}),\cdots,(X_{n},Y_{n}))\stackrel{{\scriptstyle\psi}}{{\rightarrow}}{\mathord{\perp}}$, which implies there exists $(X_{i},Y_{i})$ such that $(X_{i},Y_{i})\not\in X_{\psi}^{i}$. Thus, for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ it holds that $\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\cdots,(X^{n},X^{n}_{R}))$, where $(X^{i}\cap X^{i}_{R})\not\subseteq Q_{i}^{S}$ or $(X^{i}\cap X^{i}_{R})=\emptyset$ for some $1\leq i\leq n$. Based on Corollary 15 it holds that the system is infinite-step opaque. $\blacksquare$

7 Compositional $K$-step opacity verification

This section discusses the compositional approach for $K$-step opacity verification. Since infinite-step opacity is a special case of $K$-step opacity, in this section we mainly focus on $K$-step opacity and we discuss throughout how the results can be extended to handle infinite-step opacity verification. As in the case of current-state opacity, the first step of compositional $K$-step opacity verification is to abstract the individual components. This is described in Sect. 7.1. Next, Sect. 7.2 presents the construction of two-way observers of individual components and Sect. 7.3 shows how $K$-step opacity verification can be transformed to nonblocking verification.

7.1 Opaque observation equivalence

The idea of $K$-step opacity is that the intruder cannot determine if the secret state was reached within $K$-step prior to the current state. As opaque observation equivalence only merges states with the same secrecy property and the same future behavior, $K$-step opacity is preserved by opaque observation equivalence, step (i) in Fig. 2. This is shown in Theorem 18.

Theorem 18

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\lor}$ for interaction, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q^{NS}_{1}\times\ldots\times Q^{NS}_{n}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is $K$-step opaque if and only if $\tilde{\mathcal{G}}$ is $K$-step opaque.

Proof:

Consider $G_{2}\mathbin{\parallel}\ldots\mathbin{\parallel}G_{n}=T=\langle{\Sigma}_{T},Q_{T},\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ}_{T}\rangle$ with the set of secret states $Q^{S}_{T}=Q^{S}_{2}\times\ldots\times Q^{T}_{n}$ and non secret states $Q_{T}^{NS}=Q_{T}\setminus Q_{T}^{S}$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque then $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque either and vice versa.

1. (i)

First assume that $G_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque. Then there exists $(x^{0}_{G_{1}},x^{0}_{T})\in Q^{\circ}_{G_{1}}\times Q^{\circ}_{T}$ and $st\in\mathcal{L}(G_{1}\mathbin{\parallel}_{\lor}T,(x^{0}_{G_{1}},x^{0}_{T}))$ such that $(x^{0}_{G_{1}},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, and $x_{1}\in Q_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$ and $|t|\leq K$, and one of the following holds.

• •

For all $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$ then $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$.

Since $G_{1}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\sim G_{1}\mathbin{\parallel}_{\lor}T$. This means, if $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ if and only if $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$. Thus, $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque either.

Now consider the case where $G_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque because $(x^{0}_{G},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, and $x_{1}\in Q_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$ and there does not exist $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$. The proof for this part is the same as the proof for Theorem 4 in Sect. 5.1, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted. 2. (ii)

If $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque. Then there exists $([x_{G_{1}}^{0}],x_{T}^{0})\in\tilde{Q}^{\circ}_{G_{1}}\times Q_{T}^{\circ}$ and $st\in\mathcal{L}(\tilde{G}_{1}\mathbin{\parallel}_{\lor}T,([x^{0}_{G_{1}}],x^{0}_{T}))$ such that $([x^{0}_{G_{1}}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, and $[x_{1}]\in\tilde{Q}_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$ and $|t|\leq K$, and one of the following cases holds.

• •

For all $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ then $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$.

Since $G_{1}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\sim G_{1}\mathbin{\parallel}_{\lor}T$. This means, if $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $G_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $(x^{\prime}_{1},x^{\prime}_{T})\in Q^{NS}_{1}\times Q^{NS}_{T}$ if and only if $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$. Thus, $G_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque either.

Now consider the case when $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T$ is not $K$-step opaque because $([x^{0}_{G_{1}}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, and $[x_{1}]\in\tilde{Q}_{1}^{S}$ or $x_{T}\in Q_{T}^{S}$ and there does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\lor}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$. The proof for this part is the same as the proof for Theorem 4 in Sect. 5.1, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted. $\blacksquare$

Theorem 18 shows that if $x\stackrel{{\scriptstyle s}}{{\Rightarrow}}$ in $G$, then $[x]\stackrel{{\scriptstyle s}}{{\Rightarrow}}$ in $\tilde{G}$. As opaque observation equivalence only merges states with the same future behavior, the lengths of the strings remain consistent after abstraction. Therefore, $K$-step opacity is preserved by opaque observation equivalence.

Corollary 19

Let $\mathcal{G}=\{G_{1},\ldots,G_{n}\}$ be a non-deterministic system with $\mathbin{\parallel}_{\land}$ for interaction and with the set of secret states $Q^{S}=Q_{1}^{S}\times\ldots\times Q_{n}^{S}$. Let $\sim$ be an opaque observation equivalence on $G_{1}$ such that $\tilde{\mathcal{G}}=\{\tilde{G_{1}},G_{2},\ldots,G_{n}\}$. Then $\mathcal{G}$ is $K$-step opaque if and only if $\tilde{\mathcal{G}}$ is $K$-step opaque.

Proof:

Consider $G_{2}\mathbin{\parallel}\ldots\mathbin{\parallel}G_{n}=T=\langle{\Sigma}_{T},Q_{T},\stackrel{{\scriptstyle}}{{\rightarrow}},Q^{\circ}_{T}\rangle$. It suffices to show that if $G_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque either and vice versa.

1. (i)

First assume that $G_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque. Then there exists $(x^{0}_{G_{1}},x^{0}_{T})\in Q^{\circ}_{G_{1}}\times Q^{\circ}_{T}$ and $st\in\mathcal{L}(G_{1}\mathbin{\parallel}_{\land}T,(x^{0}_{G_{1}},x^{0}_{T}))$ such that $(x^{0}_{G_{1}},x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$, $(x_{1},x_{T})\in Q_{1}^{S}\times Q_{T}^{S}$ and $|t|\leq K$, and one of the following holds.

• •

For all $(x^{\prime}_{1},x^{\prime}_{T})$ such that $x^{\prime}_{1}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ and $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$ then $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $x^{\prime}_{1}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$.

Since $G_{1}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\sim G_{1}\mathbin{\parallel}_{\land}T$. This means, if $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $x^{\prime}_{1}\in Q^{NS}_{1}$ if and only if $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{1}$. Thus, $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque either.

Now consider the case, where $(x_{1},x_{T})\in Q_{G_{1}}\times Q_{T}$ such that $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x_{1},x_{T})$ and $(x_{1},x_{T})\in Q_{1}^{S}\times Q_{T}^{S}$, and there does not exist $x^{\prime}_{1}\in Q^{NS}_{1}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ such that $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})$. The proof for this part is the same as the proof for Corollary 5, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted.

Therefore, it can be concluded that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque. 2. (ii)

If $\tilde{G}_{1}\mathbin{\parallel}_{\land}T$ is not $K$-step opaque. Then there exists $([x_{G_{1}}^{0}],x_{T}^{0})\in\tilde{Q}^{\circ}_{G_{1}}\times Q_{T}^{\circ}$ and $st\in\mathcal{L}(\tilde{G}_{1}\mathbin{\parallel}_{\land}T,([x^{0}_{G}],x^{0}_{T}))$ such that $([x^{0}_{G}],x^{0}_{T})\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x_{1}],x_{T})$, $([x_{1}],x_{T})\in\tilde{Q}_{G_{1}}^{S}\times Q_{T}^{S}$ and $|t|\leq K$, and one of the following cases holds.

• •

For all $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}_{G_{1}}\times Q_{T}$ such that $[x^{\prime}_{1}]\in\tilde{Q}^{NS}$ or $x^{\prime}_{T}\in Q^{NS}_{T}$ and $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$ then $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$.

• •

There does not exist $([x^{\prime}_{1}],x^{\prime}_{T})\in\tilde{Q}^{NS}_{1}\times Q^{NS}_{T}$ such that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})$.

Since $G_{1}\sim\tilde{G}_{1}$ it holds that $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\sim G_{1}\mathbin{\parallel}_{\lor}T$. This means, if $\tilde{G}_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}([x^{\prime}_{1}],x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$ then $G_{1}\mathbin{\parallel}_{\land}T\stackrel{{\scriptstyle s}}{{\Rightarrow}}(x^{\prime}_{1},x^{\prime}_{T})\not\stackrel{{\scriptstyle t}}{{\Rightarrow}}$, where $x^{\prime}_{1}\in[x_{1}^{\prime}]$ and $x^{\prime}_{1}\in Q^{NS}_{1}$ if and only if $[x^{\prime}_{1}]\in\tilde{Q}^{NS}_{1}$. Thus, $G\mathbin{\parallel}_{\land}T$ is not $K$-step opaque either.

Again the proof for this part is the same as the proof for Corollary 5, proof of opaque observation equivalence preserves current-state opacity, and consequently omitted.

Therefore, it can be concluded that the $G\mathbin{\parallel}_{\land}T$ is not $K$-step opaque. $\blacksquare$

7.2 Synchronization of two-way observers

To verify $K$-step opacity similar to infinite-step opacity the two-way observers of the system components need to be generated. As explained in Section 6.2 synchronization of the two-way observers of individual components provides an over approximation of the state space of the monolithic two-way observer of the system. Thus, if the verification of the over approximated two-way observer results in $K$-step opacity it can be concluded that the original system is also $K$-step opaque. However, if the result shows violation of the $K$-step opacity it needs to be investigated to confirm that the violation is not the result of reaching an unreachable state due to over approximation.

Theorem 20

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\lor}\ldots\mathbin{\parallel}_{\lor}G_{n}$ be a non-deterministic system, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q\setminus Q^{NS}$, where $Q^{NS}=Q_{1}^{NS}\times\ldots\times Q_{n}^{NS}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ and let $H=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}$. Let $P_{\Delta}:{\Sigma}_{H}\stackrel{{\scriptstyle}}{{\rightarrow}}\Delta_{R}({\Sigma})$. If for any string $s\in\mathcal{L}(H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n})$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\ldots,(X^{n},X_{R}^{n}))$ we have

[TABLE]

then the system $\mathcal{G}$ is $K$-step opaque.

Proof:

First, based on Proposition 6, Proposition 13 and Lemma 26 it holds that $\Delta(det(\mathcal{G}))\mathbin{\parallel}\Delta_{R}(det(\mathcal{G}_{R}))\sqsubseteq[\Delta(det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}]$.

Assume that for any string $s\in\mathcal{L}(H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n})$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X_{1},Y_{1}),\ldots,(X_{n},Y_{n}))$ we have

[TABLE]

Since $\mathbin{\parallel}_{\lor}$ is used for interaction, from $[\exists(X^{i}\cap X_{R}^{i})\ :\ (X^{i}\cap X_{R}^{i})\subseteq Q_{i}^{S}\land\ (X^{i}\cap X_{R}^{i})\not=\emptyset]$ it holds that $[((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))\subseteq Q^{S}\land((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))\not=\emptyset]$. Since $((X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R}))=((X^{1}\times\ldots\times X^{n})\cap(X^{1}_{R}\times\ldots\times X^{n}_{R}))$ equation 7.2 can be rewritten as

[TABLE]

Based on Prop. 13 if $H\stackrel{{\scriptstyle s}}{{\rightarrow}}(X,X_{R})$ it holds that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\ldots,(X^{n},X_{R}^{n}))$ and $X_{R}\subseteq X^{1}_{R}\times\ldots\times X_{R}^{n}$ and based on Prop. 6 it holds that $X=X^{1}\times\ldots\times X^{n}$. This implies $(X\cap X_{R})\subseteq(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})$. Thus, there are two possibilities for $(X\cap X_{R})$:

• •

If $(X\cap X_{R})=\emptyset$ then it can be concluded that the system is $K$-step opaque.

• •

If $(X\cap X_{R})\not=\emptyset$ then as $((X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n}))\subseteq Q^{S}$ and $(X\cap X_{R})\subseteq((X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n}))$ it follows that $(X\cap X_{R})\subseteq Q^{S}$. Thus, we have

[TABLE]

which means the system is $K$-step opaque. $\blacksquare$

Theorem 20 establishes a sufficient condition for $K$-step opacity verification when $\mathbin{\parallel}_{\lor}$ is used for synchronization. Essentially, the theorem looks at all reachable states of the modular two-way observer, which contain states in which the (non-empty) intersection of the two components lies entirely in the set of secret states. If such states are reached after up to $K$ observations, then the system is $K$-step opaque.

Example 9

Consider the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ and $G_{2}$ are shown in Fig. 1 and Fig. 3, respectively. The set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$ and that of $G_{2}$ is $Q^{S}_{2}=\emptyset$. The modular two-way observer of the system is $\{H_{1},H_{2}\}$ and the monolithic two-way observer of the system is $H$, shown in Fig. 5. Assume $\mathbin{\parallel}_{\lor}$ is used for interaction and 1-step opacity needs to be verified. Let $W_{i}=(q_{i},p_{i})$ for automaton $H$. As it can be seen, $q_{i}\cap p_{i}=\{(s_{0},t_{0})\}\not\subseteq Q^{S}$ when $i=1,3$, and $q_{i}\cap p_{i}=\emptyset$ when $i=4,5$, and $q_{i}\cap p_{i}=\{([s_{1}],t_{1}),([s_{2}],t_{1})\}\not\subseteq Q^{S}$ when $i=2,6$. Therefore, the system is 1-step opaque and in fact infinite-step opaque. However, the condition of Theorem 20 does not hold for the state $(F,F^{\prime})$ since $H_{1}\mathbin{\parallel}H_{2}\xrightarrow{(\alpha,\epsilon)(\epsilon,\beta)}(F,F^{\prime})$ and for state $F$ in $H_{1}$ we have that $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$ but $|P_{\Delta}((\alpha,\epsilon)(\epsilon,\beta))|=1\not>1$. Therefore, from $H_{1}\mathbin{\parallel}H_{2}$, it cannot be concluded that the system is 1-step opaque.

Corollary 21 provides a similar result as Theorem 20 when interaction is done using $\mathbin{\parallel}_{\land}$.

Corollary 21

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}G_{n}$ be a non-deterministic system, where each automaton has set of secret states $Q_{i}^{S}$. Hence, the set of secret states of the system is $Q^{S}=Q_{1}^{S}\times\ldots\times Q_{n}^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ and let $H=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}$. Let $P_{\Delta}:{\Sigma}_{H}\stackrel{{\scriptstyle}}{{\rightarrow}}\Delta_{R}({\Sigma})$. If for any string $s\in\mathcal{L}(H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n})$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X_{1},Y_{1}),\ldots,(X_{n},Y_{n}))$ we have

[TABLE]

then the system $\mathcal{G}$ is $K$-step opaque.

Proof:

First, based on Prop. 6, Prop. 13 and Lemma 26 it holds that $\Delta(det(\mathcal{G}))\mathbin{\parallel}\Delta_{R}(det(\mathcal{G}_{R}))\sqsubseteq[\Delta(det(G_{1})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R})\mathbin{\parallel}\ldots\mathbin{\parallel}det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n,R}))=\Delta(det(G_{1}))\mathbin{\parallel}\Delta_{R}(det(G_{1,R}))\mathbin{\parallel}\ldots\mathbin{\parallel}\Delta(det(G_{n}))\mathbin{\parallel}\Delta_{R}(det(G_{n,R}))=H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}]$. Assume that for any string $s\in\mathcal{L}(H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n})$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X_{1},Y_{1}),\ldots,(X_{n},Y_{n}))$

[TABLE]

Since $\mathbin{\parallel}_{\land}$ is used for interaction, from $(X^{i}\cap X^{i}_{R})\subseteq Q_{i}^{S}$ and $(X^{i}\cap X_{R}^{i})\not=\emptyset$ for all $1\leq i\leq n$ it holds that $(X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R})\subseteq Q^{S}$ and $(X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R})\not=\emptyset$. Since $(X^{1}\cap X^{1}_{R})\times\ldots\times(X^{n}\cap X^{n}_{R})=(X^{1}\times\ldots\times X^{n})\cap(X^{1}_{R}\times\ldots\times X^{n}_{R})$ equation 7.2 can be rewritten as $[(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X^{n}_{R})\subseteq Q^{S}\land\ (X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X^{n}_{R})\not=\emptyset]\Rightarrow|P_{\Delta}(s)|>K$.

Based on Prop. 13 if $H\stackrel{{\scriptstyle s}}{{\rightarrow}}(X,X_{R})$ it holds that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X^{1}_{R}),\ldots,(X^{n},X_{R}^{n}))$ and $X_{R}\subseteq X^{1}_{R}\times\ldots\times X_{R}^{n}$ and based on Prop. 6 it holds that $X=X^{1}\times\ldots\times X^{n}$. This implies $(X\cap X_{R})\subseteq(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})$. Thus, there are two possibilities for $(X\cap X_{R})$:

• •

If $(X\cap X_{R})=\emptyset$ then it can be concluded that the system is $K$-step opaque.

• •

If $(X\cap X_{R})\not=\emptyset$ then from $(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})\subseteq Q^{S}$ and $(X\cap X_{R})\subseteq(X^{1}\times\ldots\times X^{n})\cap(X_{R}^{1}\times\ldots\times X_{R}^{n})$ it follows that $(X\cap X_{R})\subseteq Q^{S}$. Thus, we have

[TABLE]

which means the system is $K$-step opaque. $\blacksquare$

Example 10

Consider the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ and $G_{2}$ are shown in Fig. 1 and Fig. 3, respectively. The set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$ and that of $G_{2}$ is $Q^{S}_{2}=\emptyset$. The modular two-way observer of the system is $\{H_{1},H_{2}\}$ and the monolithic two-way observer of the system is $H$, shown in Fig. 5. Assume $\mathbin{\parallel}_{\land}$ is used for interaction and 1-step opacity needs to be verified. 333Since $Q^{S}_{2}=\emptyset$ and $\mathbin{\parallel}_{\land}$ is used for interaction the system is trivially infinite-step opaque and also 1-step opaque. However, it is used to explain the condition of Corollary 21. The condition of Corollary 21 holds for all states of $H_{1}\mathbin{\parallel}H_{2}$ including state $(F,F^{\prime})$. Even though for state $F$ in $H_{1}$ we have that $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$ but since for $F^{\prime}$ we have ${t_{1}}\cap{t_{0}}=\emptyset$, state $(F,F^{\prime})$ does not violate the condition of Corollary 21. Therefore, in contrast to Example 9 from $H_{1}\mathbin{\parallel}H_{2}$, it can be concluded that the system is 1-step opaque.

7.3 $K$-step opacity to nonblocking verification

The main idea of this paper is to transform opacity verification to nonblocking verification and use existing nonblocking verification algorithms. To transform $K$-step opacity verification to nonblocking verification, the $\psi$-automata of the two-way observers need to be built. First, the states of the two-way observers that violate $K$-step opacity are identified and from them transitions to blocking states are added, step (iii) and (iv) in Fig. 2.

Theorem 22

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\lor}\ldots\mathbin{\parallel}_{\lor}G_{n}$ be a non-deterministic system, with set of non-secret states $Q_{\mathcal{G}}^{NS}=Q_{1}^{NS}\times\cdots\times Q_{n}^{NS}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$. Let $P_{i,\Delta}:\Sigma_{H_{i}}\to\Delta_{R}({\Sigma}_{i})$. If $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}$ is nonblocking then $\mathcal{G}$ is $k$-step opaque, where $X_{\psi_{i}}^{i}=\{\ H_{i}\stackrel{{\scriptstyle s}}{{\rightarrow}}(X^{i},X_{R}^{i})\ |\ (X^{i}\cap X_{R}^{i})\subseteq Q_{i}^{S}\land\ (X^{i}\cap X_{R}^{i})\not=\emptyset\ \land|P_{i,\Delta}(s)|\leq K\}$.

Proof:

If $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}$ is nonblocking it means that for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1,\psi_{1}}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi_{n}}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\ldots,(X^{n},X_{R}^{n}))$ there does not exist $\psi_{i}$ such that $((X^{1},X_{R}^{1}),\ldots,(X_{n},X_{R}^{n}))\not\stackrel{{\scriptstyle\psi_{i}}}{{\rightarrow}}{\mathord{\perp}}$. This means $(X^{i},X_{R}^{i})\not\in X_{\psi_{i}}^{i}$ for all $1\leq i\leq n$. If $(X^{i},X_{R}^{i})\not\in X_{\psi_{i}}^{i}$, there are two possibilities:

• •

$(X^{i}\cap X_{R}^{i})\not\subseteq Q^{S}_{i}$ for all $1\leq i\leq n$. This means for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\ldots,(X^{n},X_{R}^{n}))$ it holds that $(X^{i}\cap X_{R}^{i})\not\subseteq Q^{S}_{i}$ for all $1\leq i\leq n$. This means there does not exist $(X^{i}\cap X_{R}^{i})$ such that $(X^{i}\cap X_{R}^{i})\subseteq Q^{S}_{i}$ and $(X^{i}\cap X_{R}^{i})=\emptyset$. Thus, based on Theorem 20 it holds that the system is $K$-step opaque.

• •

$[(X^{i}\cap X_{R}^{i})\subseteq Q^{S}_{i}\land(X^{i}\cap X_{R}^{i})\not=\emptyset]\Rightarrow|P_{i,\Delta}(P_{i}(s))|>K$ for all $1\leq i\leq n$. Since $|P_{\Delta}(s)|\geq|P_{i,\Delta}(P_{i}(s))|$ and $|P_{i,\Delta}(P_{i}(s))|>K$ it holds that $|P_{\Delta}(s)|>K$. This means if there exists $(X^{i},X_{R}^{i})$ such that $(X^{i}\cap X_{R}^{i})\subseteq Q^{S}_{i}$ and $(X^{i},X_{R}^{i})\not=\emptyset$ then $|P_{\Delta}(s)|>K$. Thus, based on Theorem 20 it follows that the system $\mathcal{G}$ is $K$-step opaque. $\blacksquare$

Theorem 22 establishes that when the transformed system is nonblocking, we can conclude that the original system is $K$-step opaque. However, if the result of nonblocking verification is negative (blocking), then the system could still be $K$-step opaque. This problem arises for two reasons. First, it can be caused by the over-approximation of the state space of the two-way observer, as was explained in Sect. 7.2. Second, it may also be caused by over-approximation of $X_{\psi_{i}}^{i}$. The latter may happen because $X_{\psi_{i}}^{i}$ can contain states that are not fulfilling the condition on the length of strings, $|P_{\Delta}(s)|>K$, in Def. 3. However, the length of the strings are unknown before the synchronization and synchronization may add to the length of $s$, causing fulfillment of the condition.

The following example illustrates all the steps of modular $K$-step verification.

Example 11

Consider the system $\mathcal{G}=\{G_{1},G_{2}\}$, where $G_{1}$ and $G_{2}$ are shown in Fig. 1 and Fig. 3, respectively. The set of secret states of $G_{1}$ is $Q^{S}_{1}=\{s_{1},s_{3}\}$ and that of $G_{2}$ is $Q^{S}_{2}=\emptyset$. Assume $\mathbin{\parallel}_{\lor}$ is used for interaction and 1-step opacity needs be verified. At the first step of the compositional approach, individual components are abstracted using opaque observation equivalence, step (i) in Fig. 2. This results in the abstracted system $\tilde{\mathcal{G}}=\{\tilde{G}_{1},G_{2}\}$ with $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$. $\tilde{G}_{1}$ is shown in Fig. 1. Next, the two-way observers of the abstracted components are generated, step (ii) in Fig. 2. As explained in Example 6, the two-way observer of $\tilde{G_{1}}$ is $\tilde{H}_{1}$ and the two-way observer of $G_{2}$ is $H_{2}$; shown in Figs 1 and 5. Next, 1-step opacity verification is transformed to nonblocking verification by generating the $\psi_{i}$-automaton for each $H_{i}$, step (iii) in Fig. 2. For the two-way observer $H_{1}$ we have that $X_{\psi_{1}}^{1}=\{F\}$, since for the state $F$ it holds that $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$ and $|P_{1,\Delta}((\alpha,\epsilon)(\epsilon,\beta))|=1$. For the two-way observer $H_{2}$ we have that $X_{\psi_{2}}^{2}=\emptyset$. Fig. 6 shows $H_{1,\psi_{1}}$. The system $H_{1,\psi_{1}}\mathbin{\parallel}H_{2,\psi_{2}}$ is blocking since $H_{1,\psi_{1}}\mathbin{\parallel}H_{2,\psi_{2}}\xrightarrow{(\alpha,\epsilon)(\epsilon,\beta)}(F,F^{\prime})\stackrel{{\scriptstyle\psi_{1}}}{{\rightarrow}}{\mathord{\perp}}$. Thus, no conclusion can be drawn about the 1-step opacity of the system, step (iv) in Fig. 2.

However, as explained in Example 6 state $(F,F^{\prime})$ is reachable due to over approximation. Thus, it can be concluded that the system is 1-step opaque.

Finally, Corollary 23 shows how $K$-step opacity can be verified when $\mathbin{\parallel}_{\land}$ is used for interaction.

Corollary 23

Let $\mathcal{G}=G_{1}\mathbin{\parallel}_{\land}\ldots\mathbin{\parallel}_{\land}G_{n}$ be a non-deterministic system, with set of secret states $Q_{\mathcal{G}}^{S}=Q_{1}^{S}\times\cdots\times Q_{n}^{S}$. Let $\Delta\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}{\Sigma}\times\{\epsilon\}$ and $\Delta_{R}\colon{\Sigma}\stackrel{{\scriptstyle}}{{\rightarrow}}\{\epsilon\}\times{\Sigma}$ and let $H_{i}=\langle{\Sigma}_{H},Q_{H},\stackrel{{\scriptstyle}}{{\rightarrow}}_{H},Q^{\circ}_{H}\rangle$, where ${\Sigma}_{H_{i}}=\Delta({\Sigma}_{i})\cup\Delta_{R}({\Sigma}_{i})$, be the two-way observer of $G_{i}$ for $1\leq i\leq n$. Let $P_{i,\Delta}:\Sigma_{H_{i}}\to\Delta_{R}({\Sigma}_{i})$. If $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}$ is nonblocking then $\mathcal{G}$ is $K$-step opaque, where where $X_{\psi}^{i}=\{\ H_{i}\stackrel{{\scriptstyle s}}{{\rightarrow}}(X^{i},X_{R}^{i})\ |\ (X^{i}\cap X_{R}^{i})\subseteq Q_{i}^{S}\land\ (X^{i}\cap X_{R}^{i})\not=\emptyset\ \land|P_{i,\Delta}(s)|\leq K\}$.

Proof:

If $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}$ is nonblocking it means that for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1,\psi}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n,\psi}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\ldots,(X^{n},X_{R}^{n}))\not\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$. This means there exists $(X^{i},X_{R}^{i})$ such that $(X^{i},X_{R}^{i})\not\in X_{\psi}^{i}$. If $(X^{i},X_{R}^{i})\not\in X_{\psi}^{i}$ then there are two following possibilities.

1. (i)

$(X^{i}\cap X_{R}^{i})\not\subseteq Q^{S}_{i}$. This means for all $s\in(\Delta({\Sigma})\cup\Delta_{R}({\Sigma}))^{*}$ such that $H_{1}\mathbin{\parallel}\ldots\mathbin{\parallel}H_{n}\stackrel{{\scriptstyle s}}{{\rightarrow}}((X^{1},X_{R}^{1}),\ldots,(X^{n},X_{R}^{n}))$ it holds that there exists $(X^{i},X_{R}^{i})$ such that $(X^{i}\cap X_{R}^{i})\not\subseteq Q^{S}_{i}$, which based on Corollary 21 it holds that the system is $K$-step opaque. 2. (ii)

$[(X^{i}\cap X_{R}^{i})\subseteq Q^{S}_{i}\land(X^{i}\cap X_{R}^{i})\not=\emptyset]\Rightarrow|P_{i,\Delta}(P_{i}(s))|>K$. Since $|P_{\Delta}(s)|\geq|P_{i,\Delta}(P_{i}(s))|$ and $|P_{i,\Delta}(P_{i}(s))|>K$ it holds that $|P_{\Delta}(s)|>K$. This means if $[(X^{j}\cap X_{R}^{j})\subseteq Q^{S}_{j}\land(X^{j}\cap X_{R}^{j})\not=\emptyset]$ for all $1\leq j\leq n$ then $|P_{\Delta}(s)|>K$. Thus, based on Corollary 21 it follows that the system $\mathcal{G}$ is $K$-step opaque. $\blacksquare$

Example 12

Consider the system $\mathcal{G}=\{\tilde{G}_{1},G_{2}\}$, where $\tilde{G}_{1}$ and $G_{2}$ are shown in Fig. 1 and Fig. 3, respectively. The set of secret states of $\tilde{G}_{1}$ is $\tilde{Q}^{S}_{1}=\{[s_{1}]\}$ and that of $G_{2}$ is $Q^{S}_{2}=\emptyset$. Assume that $\mathbin{\parallel}_{\land}$ is used for interaction and that 1-step opacity needs to be verified. The two-way observer of $\tilde{G_{1}}$ is $\tilde{H}_{1}$ and the two-way observer of $G_{2}$ is $H_{2}$. Automaton $\tilde{H}_{1}$ is shown in Fig. 1 as $H_{1}$ and $H_{2}$ is shown in Fig. 5. To transform 1-step opacity verification to nonblocking verification, the $\psi$-automaton for each $H_{i}$ needs to be generated. For the two-way observer $\tilde{H}_{1}$ we have that $\tilde{H}_{1}\xrightarrow{(\epsilon,\beta),(\alpha,\epsilon)}F=\{[s_{1}],[s_{2}]\},\{[s_{1}]\}$ and $\{[s_{1}],[s_{2}]\}\cap\{[s_{1}]\}\subseteq Q^{S}_{1}$ and $|P_{1,\Delta}((\epsilon,\beta),(\alpha,\epsilon))|=1$. Thus, $X_{\psi}^{1}=\{F\}$ and for the two-way observer $H_{2}$ we have that $X_{\psi}^{2}=\emptyset$. Automaton $H_{1,\psi}$ is similar to $H_{1,\psi_{1}}$ shown in Fig. 6, but the transition $F\stackrel{{\scriptstyle\psi_{1}}}{{\rightarrow}}{\mathord{\perp}}$ is instead replaced by $F\stackrel{{\scriptstyle\psi}}{{\rightarrow}}{\mathord{\perp}}$. The system $H_{1,\psi}\mathbin{\parallel}H_{2,\psi}$ is trivially nonblocking. Thus, we can conclude that the system is 1-step opaque.

8 Experimental Results

In this section, compositional current-state opacity verification is tested on a scalable example. The example consists of two players, $A$ and $B$, that are moving in a house. To enter each room of the house the players need to use the corresponding key. One of the rooms is a “two-person rule” room, which means that to open that room the presence of the two players is required. Fig. 7 shows the model of the players.

In the model of the players, event $u_{i,j}$ means that player $i$ has unlocked room $j$. Player $A$ starts at room $R_{1}$, from which the player can go to room $R_{2}$. Room $R_{3}$ is the two-person rule room and event $u_{3}$ is a shared event between the two players. This shows that both players can enter room $R_{3}$ only if they are at room $R_{2}$ simultaneously. After entering room $R_{3}$, player $A$ can either unobservably go to room $R_{4}$, which is a secret room for player $A$, and then return to room $R_{3}$, or it can go to room $R_{5}$. From room $R_{5}$, player $A$ can return to the initial room $R_{1}$. Player $B$ can start either at room $R_{1}$ or $R_{2}$. From room $R_{3}$, player $B$ can go back to the initial room $R_{1}$ or it can go to room $R_{5}$ and from there go back to the initial room $R_{1}$. However, room $R_{5}$ is a secret room for $B$. The example can be scaled up by adding serially connected houses or increasing the number of players.

We have used Supremica [18] to test the scalability of our compositional methodology for current-state opacity verification on the above example. The model is scaled up by adding up to 2,000 players or having up to 2,000 serially connected houses (using $||_{\lor}$). All tests were run on a standard laptop using a quad core CPU at 2.6 GHz. Our methodology does not use any prior knowledge about the system. Table 1 shows the results of the experiments. For each model, the table shows the number of automata (Aut.) and whether the system is current-state opaque (Opaque). The table also shows the runtime for calculating opaque observation equivalence, the runtime for constructing the current-state estimator of all the components, and finally the runtime for nonblocking verification. Even though the compositional approach has no prior knowledge about the system, the models can be verified in few seconds or minutes.

9 Conclusion

We introduced a novel methodology for verification of current-state and $K$-step opacity in modular discrete event systems. The methodology supports compositional reasoning using the notion of opaque observation equivalence that we defined, which guarantees that current-state and $K$-step opacity are preserved properties. After abstracting the components, the opacity verification problem is then transformed to a nonblocking verification problem. This makes it possible to use existing compositional methods for nonblocking verification of modular systems. Under our methodology, the system is current-state opaque if and only if the transformed system is nonblocking. In addition, it can be concluded that the system is infinite-step opaque or $K$-step opaque if the transformed system is nonblocking. Our experimental results suggest that the compositional approach that we have presented can lead to significant computational gains over a monolithic approach.

It would be of interest to study in the future how compositional approaches could be used to enforce opacity for a non-opaque system, either via supervisory control or via the use of output edit functions.