广东工业大学学报  2023, Vol. 40Issue (3): 32-37.  DOI: 10.12052/gdutxb.210169.
0

引用本文 

亓国照, 刘富春, 崔洪刚. 基于双向观测器的随机离散事件系统的不透明性[J]. 广东工业大学学报, 2023, 40(3): 32-37. DOI: 10.12052/gdutxb.210169.
Qi Guo-zhao, Liu Fu-chun, Cui Hong-gang. Opacity Verification in Stochastic Discrete Event Systems Using Two-way Observers[J]. JOURNAL OF GUANGDONG UNIVERSITY OF TECHNOLOGY, 2023, 40(3): 32-37. DOI: 10.12052/gdutxb.210169.

基金项目:

国家自然科学基金资助项目(61672722);广东省自然科学基金资助项目(2023A1515012783)

作者简介:

亓国照(1997–),男,硕士研究生,主要研究方向为控制理论与控制工程、算法分析与设计。

通信作者

刘富春(1971–),男,教授,博士,主要研究方向为控制理论与控制工程、数理逻辑与模糊系统,E-mail:liufch@gdut.edu.cn

文章历史

收稿日期:2021-11-05
基于双向观测器的随机离散事件系统的不透明性
亓国照, 刘富春, 崔洪刚    
广东工业大学 计算机学院,广东 广州 510006
摘要: 本文针对随机系统模型,研究随机离散事件系统的不透明性。首先对随机无穷步不透明性和随机K步不透明性进行形式化。通过构造一个基于双向观测器的验证器,得到一个运用双向观测器验证系统随机无穷步不透明性和随机K步不透明性的充分必要条件。最后提出一个基于双向观测器的随机无穷步不透明性和随机K步不透明性验证算法。
关键词: 随机离散事件系统    双向观测器    无穷步不透明    K步不透明性    
Opacity Verification in Stochastic Discrete Event Systems Using Two-way Observers
Qi Guo-zhao, Liu Fu-chun, Cui Hong-gang    
School of Computer Science and Technology, Guangdong University of Technology, Guangzhou 510006, China
Abstract: The opacity of stochastic discrete event system is studied for stochastic system models. Firstly, the notions of stochastic infinite-step opacity and stochastic K-step opacity are formalized. By constructing a validator based on a two-way observer, a necessary and sufficient condition is obtained to verify the stochastic infinite-step opacity and stochastic K-step opacity of systems by using the validator of two-way observer. Finally, the verification algorithm for stochastic infinite-step opacity and stochastic K-step opacity based on two-way observer is proposed.
Key words: stochastic discrete event system    two-way observer    infinite-step opacity    K-step opacity    

离散事件系统是由离散事件按照一定的运行规则相互作用而导致状态演化的一类动态系统,在军事国防、交通控制、计算机集成制造系统、电子通讯网络、机器人技术等领域都有成功应用[1-5]。近年来,离散事件系统的不透明性(opacity)研究引起了国内外众多学者的广泛关注。离散事件系统的不透明性在数字签名、信息认证、数据加密等信息安全机制中有着重要应用[6-9]

文献[10-12]研究系统的不透明性验证,并提出了多种不同类型的不透明性。文献[10]使用监督控制的方法确保系统不透明性。文献[13]中K步不透明性首先被提出。K步不透明性用来验证入侵者能否确定系统在特定时刻之后的K个状态是否存在秘密状态。文献[14]提出,当K趋于无穷时,K步不透明度变为无穷步不透明度。文献[14]提出了一种改进的方法,使用了一种称为双向观测器的结构。文献[15]在随机离散事件系统中研究无穷步不透明性和K步不透明性,并提出随机无穷步不透明性和随机K步不透明性。

本文继续文献[14-15]的工作,将文献[14]提出的双向观测器引入至随机离散事件系统,提出一种基于双向观测器的随机无穷步不透明性和随机K步不透明性验证方法。首先对随机无穷步不透明性和随机K步不透明性进行形式化定义。然后运用文献[15]中的方法,构造 $ ({G},{p}) $ 的反向自动机 $ {{G}}_{{R}} $ ,进而得到 $ ({G},{p}) $ 的双向观测器。通过 $ ({G},{p}) $ 的双向观测器得到含有秘密状态的映射集,再以 $ ({G},{p}) $ 含有秘密状态的映射集构建验证器,得到一个基于双向观测器验证系统随机无穷步不透明性和随机K步不透明性的充分必要条件。最后提出一个基于双向观测器的随机无穷步不透明性和随机K步不透明性验证算法。

1 系统模型

经典离散事件系统表示为式(1)的不确定自动机[1]

$ G=\left({X},{\varSigma },{\delta },{{X}}_{0}\right) $ (1)

式中: $ {X} $ 为状态集, $ {\varSigma } $ 为事件集, $ {\delta }:{X}\times {\varSigma }\to {2}^{{X}} $ 是状态转移函数, $ {{X}}_{0}\subseteq {X} $ 为初始状态集。用 $ {{\varSigma }}^{{*}} $ 表示 $ {\varSigma } $ 中元素的所有有限长度字符串的集合,包括空串 $ {\epsilon } $ 。语句 $ {L}{\subseteq {\varSigma }}^{{*}} $ 是有限长度字符串 $ {{\varSigma }}^{{*}} $ 的子集。通常, $ {\varSigma } $ 可划分为两个集合:可观测事件集合 $ {{\varSigma }}_{{{\rm{obs}}}} $ 和不可观测事件集合 $ {{\varSigma }}_{{{\rm{uo}}}} $ 。并且 $ {{\varSigma }}_{{{\rm{obs}}}}\cap {{\varSigma }}_{{{\rm{uo}}}}={\phi }\wedge {{\varSigma }}_{{{\rm{obs}}}}\cup {{\varSigma }}_{{{\rm{uo}}}}={\varSigma } $ 。自然映射 $ {P}: {{\varSigma }}^{{*}}\to {{\varSigma }}_{{{\rm{obs}}}}^{{*}} $ 可以递归定义为: $ {P}\left({t}{s}\right) ={P}\left({t}\right) {P}\left({s}\right) ,{t}\in {\varSigma }, {s}\in {{\varSigma }}^{{*}} $ 。当 $ {t}\in {{\varSigma }}_{{{\rm{obs}}}} $ 时, $ {P}\left({t}\right) ={t} $ ;当 $ {t}\in {{\varSigma }}_{{{\rm{uo}}}}\cup \left\{{\epsilon }\right\} $ 时, $ {P}\left({t}\right) ={\epsilon } $

而随机离散事件系统[2]是在经典离散事件系统的基础上附加一个概率结构,通常用一个随机有穷自动机 $ ({G},{p}) $ 表示,其中 $ {G}=({X},{\varSigma },{\delta },{{X}}_{0}) $ 是一个经典离散事件系统, $ {p}:{X}\times {\varSigma }\to \left[{0,1}\right] $ 是概率转移函数。特别地,用 $ {p}({\sigma }|{x}) $ 来表示事件 $ {\sigma } $ 在状态 $ {x} $ 发生的概率,它满足:(1) $ \forall {x}\in {X}:{{\varSigma }}_{{\sigma }\in {\varSigma }}{p}\left({\sigma }\right|{x}) =1 $ ;(2) $ \forall {x}\in {X},\forall {\sigma }\in {\varSigma }: {p}\left({\sigma }\right|{x}) > 0 \Leftrightarrow {\delta }({x},{\sigma }) ! $

给定状态集 $ {q}\in {2}^{{X}} $ ,用 $ {{\rm{UR}}}\left({q}\right) $ 来表示可从 $ {q} $ 中的某个状态不可观测地到达的状态集,即

$ {\rm{UR}}\left({q}\right) =\left\{{x}\in {X}:\exists {{x}}'\in {q},\exists {s}\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{{{\rm{s}}}}\text{.}{{{\rm{t}}}}\text{.}{\delta }\left({{x}}',{s}\right) ={x}\right\}$ (2)

$ {{\rm{Next}}}({q},{\sigma }) $ 表示当可观测事件 $ {\sigma }\in {{\varSigma }}_{{{\rm{obs}}}} $ 发生时可以立即达到的状态集,即

$ {\rm{Next}}\left({q},{\sigma }\right) =\left\{\begin{array}{c}x\in X:\exists {{x}}'\in q,\\ \exists s\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{{{\rm{s}}}}{.}{{{\rm{t}}}}{.}\delta \left({{x}}',{s}\right) =x\end{array}\right\} $ (3)

假设 $ {\alpha }\in {P}({L}\left({G}\right) ) $ 是一个可观测映射。用 $ {\widehat{{X}}}_{{G}}({\alpha }) $ 表示映射 $ {\alpha } $ 发生时的当前状态估计,其定义为

$ {\widehat{{X}}}_{{G}}({\alpha })=\left\{\begin{array}{c}x\in X:\exists s\in L\left({G}\right) ,\exists {{x}}'\in q,\\ P\left({s}\right) =\alpha ,x=\delta \left({{x}}',{s}\right) \end{array}\right\}$ (4)

当执行 $ {\beta }\le {\alpha } $ (即 $ {\beta }{为}{\alpha }{的}{前}{缀}{集}{合} $ ) 时,定义在已知可观映射 $ {\alpha } $ 的条件下 $ {\beta } $ 的延迟状态估计为

$ {\widehat{{X}}}_{{G}}({\beta }|{\alpha })=\left\{\begin{array}{c}x\in X:\exists st\in L\left({G}\right) ,\exists {{x}}'\in q,\\ P\left({s}\right) =\beta ,P\left({s}{t}\right) =\alpha ,x=\delta \left({{x}}',{s}\right) \end{array}\right\} $ (5)

直观上, $ {\widehat{{X}}}_{{G}}({\beta }|{\alpha }) $ 在观测 $ {\alpha } $ 的瞬间之前估计系统 $ \left|{\alpha }\right|-\left|{\beta }\right| $ 的状态。显然,有 $ {\widehat{{X}}}_{{G}}({\alpha }|{\alpha }) $ = $ {\widehat{{X}}}_{{G}}({\alpha }) $

给定 $ {\alpha }\in {{\varSigma }}_{{o}}^{{*}} $ 是观测到的事件串。操作 $ {{\varTheta }:{\varSigma }}_{{{\rm{o}}}}^{{*}}\to {2}^{{X}\times {X}} $ 其定义如下。

$ \varTheta \left({\alpha }\right) =\left\{\begin{array}{c}\left({x},{{x}}'\right) \in X\times X:\exists s\in {{\varSigma }}^{{*}},\\ P\left({s}\right) =\alpha ,{{x}}'=\delta \left({x},{s}\right) \end{array}\right\}$ (6)

给定 $ {\overline{{r}}}_{1},{\overline{{r}}}_{2}{\in 2}^{{X}\times {X}} $ 为两个状态对集合。操作 $\circ :{2}^{{X}\times {X}}\times {2}^{{X}\times {X}}\to {2}^{{X}\times {X}}$ ,其定义为

$ {\overline{{r}}}_{1}\circ {\overline{{r}}}_{2}=\left\{\begin{array}{c}\left({{x}}_{1},{{x}}_{3}\right) \in X\times X:\exists {{x}}_{2}\in X,\\ \left({{x}}_{1},{{x}}_{2}\right) \in {\overline{{r}}}_{1},\left({{x}}_{2},{{x}}_{3}\right) \in {\overline{{r}}}_{2}\end{array}\right\} $ (7)

给定 $ {{r}\in 2}^{{X}},$ 操作 $ \odot :{2}^{{X}}\to {2}^{{X}\times {X}} $ 定义为

$ \odot \left({r}\right) =\left\{\left({x},{{x}}'\right) \in {r}\times {X}:\exists {s}\in {{\varSigma }}_{{{\rm{uo}}}}^{{*}},{\delta }\left({x},{s}\right) ={{x}}'\right\} $ (8)
2 随机K步不透明性和随机无穷步不透明性

在实际应用中违反无穷步(或K步)不透明性的概率极其微小则可以忽略不计。定量评价无穷步(或K步)不透明性,还需考虑系统转移的概率。因此提出随机无穷步(或K步)不透明性定义。

定义1  给定一个随机离散事件系统 $ ({G},{p}) $ 和秘密状态集为 $ {{X}}_{{s}} $ 及阈值 $ {\theta } < 1 $ 。记

$ {{L}}_{{{\rm{IF}}}}^{{P}}=\{{s}\in {{L}}_{{{\rm{IF}}}}:\forall {t} < {s},{t}\notin {{L}}_{{{\rm{IF}}}}\} $

如果 $ {{\varSigma }}_{{s}\in {{L}}_{{{\rm{IF}}}}^{{P}}}{p}{r}({s}) < {\theta } $ ,则称 $ ({G},{p}) $ 具有随机无穷步不透明性。

直观上, $ {{L}}_{{{\rm{IF}}}}^{{P}} $ 表示满足“任意 $ {s} $ 的前缀 $ {t} $ ,使得 $ {t} $ 满足无穷步不透明性(即 $ {t}\notin {{L}}_{{{\rm{IF}}}} $ )”的所有语句 $ {s} $ 的集合(即最小不满足无穷步不透明性的语言),从而 $ {{\varSigma }}_{{s}\in {{L}}_{{{\rm{IF}}}}^{{P}}}{p}{r}({s}) < {\theta } $ 表示入侵者始终无法确定系统是否到达秘密状态的概率不小于 $ 1-{\theta } $

定义2  给定一个随机离散事件系统 $ ({G},{p}) $ 和秘密状态集为 $ {{X}}_{{s}} $ 及阈值 $ {\theta } < 1 $ 。记

$ {{L}}_{{{{KS}}}}^{{P}}=\{{s}\in {{L}}_{{{{KS}}}}:\forall {t} < {s},{t}\notin {{L}}_{{{{KS}}}}\} $

如果 $ {{\varSigma }}_{{s}\in {{L}}_{{{{KS}}}}^{{P}}}{p}{r}({s}) < {\theta } $ ,则称 $ ({G},{p}) $ 具有随机K步不透明性。

直观上, $ {{L}}_{{{{KS}}}}^{{P}} $ 表示满足“任意 $ {s} $ 的前缀 $ {t} $ ,使得 $ {t} $ 满足K步不透明性(即 $ {t}\notin {{L}}_{{{{KS}}}} $ )”的所有语句 $ {s} $ 的集合(即最小不满足K步不透明性的语言),从而 $ {{\varSigma }}_{{s}\in {{L}}_{{{{KS}}}}^{{P}}}{p}{r}({s}) < {\theta } $ 表示入侵者在K步状态转移内不能确定系统是否到达秘密状态的概率不小于 $ 1-{\theta } $

3 验证随机无穷步不透明性

基于双向观测器 $ {{{\rm{Obs}}}}_{{{\rm{t}}}{{\rm{w}}}}({G}) $ [14]验证随机无穷步不透明性。

定理1  给定一个随机离散事件系统 $ ({G},{p}) $ ,可观事件集为 $ {{\varSigma }}_{{{\rm{o}}}} $ ,秘密状态集为 $ {{X}}_{{s}} $ 。给定 $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})=({{Q}}_{{{\rm{tw}}}}, {{\varSigma }}_{{{\rm{tw}}}},{{f}}_{{{\rm{tw}}}},{{q}}_{{{\rm{tw}}},0}) $ $ ({G},{p}) $ 的双向观测器,记

$ {{L}}_{{{\rm{IFS}}}}=\{{s}\in {L}\left({G}\right) :\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) , $
$ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}},{{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{q}}_{1},{{q}}_{2}\right) , $
$ {{{q}}_{1}\cap {{q}}_{2}\ne {\phi }\wedge {q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}}\} $

随机离散事件系统 $ ({G},{p}) $ 具有无穷步不透明性,当且仅当 $ {{L}}_{{{\rm{IFS}}}}={\phi } $

证明  (充分性)设 $ \exists \left({{q}}_{1},{{q}}_{2}\right) \in {{q}}_{{{\rm{t}}}{{\rm{w}}}} $ ,使 $ {{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ 并且 $ {{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}} $ 。设 $ {s}\in {L}\left({G}\right) $ ,则 $ \exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) $ 使得 $ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}} $ [14]。已知 $ {{q}}_{1}={{f}}_{{{\rm{obs}}}}({{x}}_{0},{{\tau }}_{1}\left({t}\right) ) $ $ {{q}}_{2}= {{f}}_{{{\rm{obs}}},{R}} ({X},{{\tau }}_{2}\left({t}\right) ) $ ,那么

$ \begin{split} {\widehat{{X}}}_{\left|{{\tau }}_{1}\left({t}\right) \right|}({{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}})=&{{f}}_{{{\rm{obs}}}}({{x}}_{0},{{\tau }}_{1}\left({t}\right) )\cap {{f}}_{{{\rm{obs}}},{R}}({X},{{\tau }}_{2}\left({t}\right) )=\\ &{{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}} ^{[14]}。\end{split} $

$ ({G},{p}) $ 具有无穷步不透明性当且仅当 ${\widehat{{X}}}_{\left|{{\tau }}_{1}\left({t}\right) \right|}({{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}}) \nsubseteq {{X}}_{{s}}$ [14]。即 $ ({G},{p}) $ 具有无穷步不透明性时, $ {{L}}_{{{\rm{IFS}}}}={\phi } $

(必要性)设 $ {{L}}_{{{\rm{IFS}}}}\ne {\phi } $ ,则 $ {\widehat{{X}}}_{\left|{{s}}_{1}\right|}({{s}}_{1}{{s}}_{2})\subseteq {{X}}_{{s}} $ $ \exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) $ 使得 $ {{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ $ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}} $ [14]。另外,

$ {{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{f}}_{{{\rm{obs}}}}({{x}}_{0},{{\tau }}_{1}\left({t}\right) ),{{f}}_{{{\rm{obs}}},{R}}({X},{{\tau }}_{2}\left({t}\right) )\right) $

从而

${\widehat{{X}}}_{\left|{{s}}_{1}\right|}( {{s}}_{1}{{s}}_{2} ) = {{f}}_{{{\rm{obs}}}}( {{x}}_{0},{{s}}_{1} ) \cap {{f}}_{{{\rm{obs}}},{R}}({X},{\left({{s}}_{2}\right) }_{{R}} )$ = ${{q}}_{1} \cap {{q}}_{2} \subseteq {{X}}_{{s}} {{s}}_{1}{{s}}_{2} \in {P}\left({L}\left({G}\right) \right) $ ,则 $ {\widehat{{X}}}_{\left|{{s}}_{1}\right|}({{s}}_{1}{{s}}_{2})={{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ 。即当 $ {{L}}_{{{\rm{IFS}}}}={\phi } $ 时, $ ({G},{p}) $ 具有无穷步不透明性。定理1得证。

通过 $ {{L}}_{{{\rm{IFS}}}} $ 构建验证器 $ {{V}}_{{G}} $ [15]。记

$ {{L}}_{{{\rm{IFS}}}}=\{{s}\in {{L}}_{{{\rm{IF}}}}:\exists {\alpha }\le {p}\left({s}\right) {{\rm{s}}}.{{\rm{t}}}.{\widehat{{X}}}_{{G}}({\alpha }|{p}\left({s}\right) )\subseteq {{X}}_{{s}}\} $

对于任何 $ {\rho }\in {2}^{{X}\times {X}} $ ,定义

$ {{l}}_{1}({\rho })=\left\{{x}\in {X}:{\exists {x}}'\in {X}{{\rm{s}}}.{{\rm{t}}}.\left({x},{{x}}'\right) \in {\rho }\right\} $ (9)

作为 $ {\rho } $ 的第一个分量中的状态集。对于任何 ${R}\in {2}^{{2}^{{X}\times {X}}}$ ,定义

$ {{l}}_{1}({R})=\left\{{{l}}_{1}({\rho })\in {2}^{{X}}:{\rho }\in {{R}}\right\} $ (10)

确定是否 $ \exists {s}\in {{L}}_{{{\rm{IF}}}} $ ,就要确定 ${{Q}}_{{{\rm{IF}}}}=\{\left({x},{R}\right) \in {Q}:\exists {\rho }\in {R}\,{ }{{\rm{s}}}.{{\rm{t}}}.{{l}}_{1}({\rho })\subseteq {{X}}_{{s}}\}$ 是否为空。记

$ {{L}}_{{{\rm{IF}}}}^{{P}}=\{{s}\in {{L}}_{{{\rm{IFS}}}}:[{f}({{q}}_{0},{s}) \in {{Q}}_{{{\rm{IF}}}}]\wedge [\forall {t} < {s}:{f}({{q}}_{0},{s}) \notin {{Q}}_{{{\rm{IF}}}}\left]\right\} $

计算 $ {{\varSigma }}_{{s}\in {{L}}_{{{\rm{LF}}}}^{{P}}}{p}({s}) $ ,首先定义 $ {{V}}_{{G}}=\left({Q},{\varSigma },{f},{{q}}_{0}\right) $ [15]。然后定义马尔可夫链 $ \left({M}{C}\right) {{\boldsymbol{M}}}=(\overline{{Q}},{{p}}_{{M}},{{\pi }}_{0}) $ ,其中 $ {{\boldsymbol{M}}} $ 状态空间与 $ {{V}}_{{G}} $ 状态空间相同,转移概率函数 $ {{p}}_{{M}} $ : $ \overline{{Q}}\times \overline{{Q}}\to \left[{0,1}\right] $ 其定义为:对于任意 ${q}=\left({x},{R}\right),{{q}}'={ }({{x}}',{{R}}') \in \overline{{Q}}$ ,

${{p}}_{{M}}\left({{q}}'|{q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\nolimits _{{\sigma }\in {\varSigma }:{f}\left({q},{\sigma }\right) ={{q}}'}{p}\left({\sigma }|{x}\right) ,&q\notin {{Q}}_{{{\rm{IF}}}}\\ 1,&q\in {{Q}}_{{{\rm{IF}}}}\\ 0,&其他\end{array}} \right. $ (11)

$ {{\pi }}_{0}:\overline{{Q}}\to \left[{0,1}\right] $ 为初始状态分布,有 $ {{\pi }}_{0}\left({{q}}_{0}\right) { }={ }1 $ $ \forall {q}\ne {{q}}_{0}:{{\pi }}_{0}\left({q}\right) { }={ }0 $ 。对于 $ {{\boldsymbol{M}}} $ ,系统处于 $ {{Q}}_{{{\rm{IF}}}}\cap {Q} $ 中的一种状态,则永远停留在其中。 ${{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{I}}}{{\rm{F}}}}\right) =\varSigma _{{q}\in \overline{{Q}}}{{\pi }}_{0}\left({q}\right) \mathbb{{P}}\left({q}\right)$ ,其中 $ \mathbb{P}:\overline{{Q}}\to {\mathbb{R}}_{0}^{+} $ 为式(12)的最小非负数解向量。

$ P\left({q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\limits _{{{q}}'\in \overline{{Q}}}{{p}}_{{M}}\left({{q}}'|{q}\right) \mathbb{P}\left({{q}}'\right) ,& q\notin {{Q}}_{{{\rm{IF}}}}\\ 1,& q\in {{Q}}_{{{\rm{IF}}}}\end{array}} \right.$ (12)

$ {{\boldsymbol{M}}} $ 通过回溯原离散事件系统的概率转移来构造,所以有 $ {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) ={{\varSigma }}_{{s}\in {{L}}_{{{\rm{LF}}}}^{{P}}}{p}({s}) $

定理2[15]  给定一个随机离散事件系统 $ ({G},{p}) $ ,可观事件集为 $ {{\varSigma }}_{{{\rm{o}}}} $ ,秘密状态集为 $ {{X}}_{{s}} $ ,验证器为 $ {{V}}_{{G}} $ ${{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})=({{Q}}_{{{\rm{tw}}}},{{\varSigma }}_{{{\rm{tw}}}},{{f}}_{{{\rm{tw}}}},{{q}}_{{{\rm{tw}}},0})$ 为系统 $ ({G},{p}) $ 的双向观测器。随机离散事件系统 $ ({G},{p}) $ 具有随机无穷步不透明性当且仅当 $ {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) < {\theta } $

4 验证随机K步不透明性

基于双向观测器 $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G}) $ [14]验证随机K步不透明性。

定理3  给定一个随机离散事件系统 $ \left({G},{p}\right) $ ,可观事件集为 $ {{\varSigma }}_{{{\rm{o}}}} $ ,秘密状态集为 $ {{X}}_{{s}} $ 。给定 ${{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})=\left({{Q}}_{{{\rm{tw}}}}, {{\varSigma }}_{{{\rm{tw}}}},{{q}}_{{{\rm{tw}}},0}\right)$ $ \left({G},{p}\right) $ 的双向观测器,记

$ {{L}}_{{{{KSS}}}}=\{{s}\in {L}\left({G}\right) :\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) $
$ {{\rm{s}}}.{{\rm{t}}}.{P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}},{{f}}_{{{\rm{tw}}}}\left({{q}}_{{{\rm{tw}}},0},{t}\right) =\left({{q}}_{1},{{q}}_{2}\right) $
$ {|{\tau }}_{2}\left({t}\right) |\le {K},{{q}}_{1}\cap {{q}}_{2}\ne {\phi }\wedge {{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}}\} $

如果随机离散事件系统 $ ({G},{p}) $ 具有随机K步不透明性,当且仅当 $ {{L}}_{{{{KSS}}}}={\phi } $

证明  (充分性)设 $ \left({G},{p}\right) $ 具有K步不透明性,则 $ \exists \left({{q}}_{1},{{q}}_{2}\right) \in {{q}}_{{{\rm{tw}}}} $ ,使 $ {{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ $ {{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}} $

$ {s}\in {L}\left({G}\right) ,\exists {t}\in {L}\left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) :$
$ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}},{|{\tau }}_{2}\left({t}\right) |\le {K} $

另有

$ {{q}}_{1}\cap {{q}}_{2}={\widehat{{X}}}_{\left|{{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}}\right|-\left|{\left({{\tau }}_{2}\right({t}\left) \right) }_{{R}}\right|}({{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}})\subseteq {{X}}_{{s}} $

$ ({G},{p}) $ 具有无穷步不透明性当且仅当 $ {{q}}_{1}\cap {{q}}_{2}\ne {\phi }\wedge {{q}}_{1}\cap {{q}}_{2}\subseteq {{X}}_{{s}},{|{\tau }}_{2}\left({t}\right) | > {K} $ [14]。即 $ ({G},{p}) $ 具有K步不透明性时, $ {{L}}_{{{{KSS}}}}={\phi } $

(必要性)设 $ {{L}}_{{{{KSS}}}}\ne {\phi } $ ,则 $ {\widehat{{X}}}_{\left|{{s}}_{1}\right|}({{s}}_{1}{{s}}_{2})\subseteq {{X}}_{{s}} $ $ \exists {t}\in {L} \left({{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})\right) $ 使得 $ {{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ ,并且 $ {P}\left({s}\right) ={{\tau }}_{1}\left({t}\right) {\left({{\tau }}_{2}\left({t}\right) \right) }_{{R}}, {|{\tau }}_{2}\left({t}\right) |\le {K} $ [14]。则有

$ {{q}}_{1}\cap {{q}}_{2}={{f}}_{{{\rm{obs}}}}({{x}}_{0},{{s}}_{1})\cap {{f}}_{{{\rm{obs}}},{R}}({X},{\left({{s}}_{2}\right) }_{{R}}) ={\widehat{{X}}}_{\left|{{s}}_{1}{{s}}_{2}\right|-\left|{{s}}_{2}\right|}({{s}}_{1}{{s}}_{2})\subseteq {{X}}_{{s}} $

$ {|{s}}_{2}|={|{\tau }}_{2}\left({t}\right) |\le {K} $ $ {{s}}_{1}{{s}}_{2}\in {P}\left({L}\left({G}\right) \right) $ ,则 $ {\widehat{{X}}}_{\left|{{s}}_{1}{{s}}_{2}\right|-\left|{{s}}_{2}\right|} ({{s}}_{1}{{s}}_{2})= {{q}}_{1}\cap {{q}}_{2}\ne {\phi } $ 。即当 $ {{L}}_{{{{KSS}}}}={\phi } $ $ ({G},{p}) $ 具有K步不透明性。定理3得证。

$ {{L}}_{{{{KSS}}}}=\{{s}\in {{L}}_{{{{KS}}}}:\exists {\alpha }\le {p}\left({s}\right) $
$ {{\rm{s}}}.{{\rm{t}}}.\left|{p}\left({s}\right) /{\alpha }\right|\le {K}{ },{\widehat{{X}}}_{{G}}({\alpha }|{p}\left({s}\right) )\subseteq {{X}}_{{s}}\} $

为了确定是否 $ {s}\in {{L}}_{{{{KS}}}}^{{P}} $ ,记

$ \begin{split} {{Q}}_{{{{KS}}}}=&\left\{\right({x},{r},{{\rho }}_{1},\cdots,{{\rho }}_{{K}}) \in {{Q}}_{{K}}:[{{\rm{UR}}}\left({x}\right) \subseteq {{X}}_{{s}}]\vee \\ &[\exists {i}=1,\cdots ,{K}:{\phi }\ne {{l}}_{1}\left({{\rho }}_{{i}}\right) \subseteq {{X}}_{{s}}\left]\right\} 。\end{split} $

记:

$ {{L}}_{{{{KS}}}}^{{P}} = \left\{{s} \in {{L}}_{{{{KSS}}}}:\left[{{f}}_{{K}}\left({{q}}_{0},{s}\right) \in {{Q}}_{{{{KS}}}}\right] \wedge \left[\forall {t} < {s}:{{f}}_{{K}}\left({{q}}_{0},{s}\right) \notin {{Q}}_{{{{KS}}}}\right]\right\} $

计算 $ {{\varSigma }}_{{s}\in {{L}}_{{{{KS}}}}^{{P}}}{p}({s}) $ ,首先定义 $ {{V}}_{{G}}^{{K}}=\left({{Q}}_{{K}},{\varSigma },{{f}}_{{K}},{{q}}_{0,{K}}\right) $ 接着定义马尔可夫链 $ \left({M}{C}\right) {{{\boldsymbol{M}}}}_{{K}}=(\overline{{{Q}}_{{K}}},{{p}}_{{M},{K}},{{\pi }}_{0,{K}}) $ ,其中 $ \left({M}{C}\right) {{{\boldsymbol{M}}}}_{{K}} $ 状态空间与 $ {{V}}_{{G}}^{{K}} $ 状态空间相同,转移概率函数 $ {{p}}_{{M}} $ : $ \overline{{{Q}}_{{K}}}\times \overline{{{Q}}_{{K}}}\to \left[{0,1}\right] $ 其定义为:对于任意 $ {Q}{ }=({x},{r}, {{\rho }}_{1},\cdots,{{\rho }}_{{K}}) $ , $ {{Q}}'=({{x}}',{{r}}',{{\rho }}_{1}',\cdots,{{\rho }}_{{K}}') \in \overline{{{Q}}_{{K}}} $

${{p}}_{{{M}}_{{K}}}\left({{q}}'|{q}\right) =\left\{ {\begin{array}{*{20}{l}}\displaystyle\sum\limits _{{\sigma }\in {\varSigma }:{{f}}_{{K}}\left({q},{\sigma }\right) ={{q}}'}{p}\left({\sigma }|{x}\right) ,&{q}\notin {{Q}}_{{{{KS}}}}\\ 1,&q={{q}}'\in {{Q}}_{{{{KS}}}}\\ 0,&其他\end{array}} \right.$ (13)

$ {{\pi }}_{0}:\overline{{Q}}\to \left[{0,1}\right] $ 是初始状态分布,有 $ {{\pi }}_{0}\left({{q}}_{0}\right) { }={ }1 $ $ \forall {q}\ne {{q}}_{0}:{{\pi }}_{0}\left({q}\right) { }={ }0 $ 。对于 $ {{{\boldsymbol{M}}}}_{{K}} $ ,系统一旦到达 $ {{Q}}_{{{{KS}}}}\cap {Q} $ 中的一种状态将永远处于其中。用 $ {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) $ 表示。

定理4[15]  给定一个随机离散事件系统 $ ({G},{p}) $ ,可观事件集为 $ {{\varSigma }}_{{{\rm{o}}}} $ ,秘密状态集为 $ {{X}}_{{s}} $ ,验证器为 $ {{V}}_{{G}} $ ,正整数K $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G})=({{Q}}_{{{\rm{tw}}}},{{\varSigma }}_{{{\rm{tw}}}},{{f}}_{{{\rm{tw}}}},{{q}}_{{{\rm{tw}}},0}) $ 为系统 $ ({G},{p}) $ 的双向观测器。随机离散事件系统 $ ({G},{p}) $ 具有随机 $ {K} $ 步不透明性当且仅当 $ {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{K}{S}}\right) < {\theta } $

5 系统不透明性算法

在给定阈值 $ {\theta } $ 的情况下,检查 $ ({G},{p}) $ 是否具有随机无穷步不透明性和随机 $ {K} $ 步不透明性。基于上文的研究结果,提出以下算法。

算法1  输入: $ {({G},{p}) =({Q},{\varSigma },{f},{{q}}_{0})} $ ,可观事件集为 $ { {{\varSigma }}_{{{\rm{o}}}} }$ ,秘密状态集为 $ { {{X}}_{{s}}} $ ,随机无穷步不透明性阈值 $ { {{\theta }}_{{{\rm{IF}}}} }$ ,正整数K,随机K步不透明性阈值 $ { {{\theta }}_{{{{KS}}}}} $

输出:系统 $ { ({G},{p}) }$ 具有随机无穷步不透明性—— $ { {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) < {{\theta }}_{{I}{F}} }$

系统 $ { ({G},{p}) }$ 不具有随机无穷步不透明性—— $ {{{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) > {{\theta }}_{{I}{F}} }$

系统 $ { ({G},{p})} $ 具有随机K步不透明性—— $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) < {{\theta }}_{{{{KS}}}} }$

系统 $ { ({G},{p}) }$ 不具有随机K步不透明性—— $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) > {{\theta }}_{{{{KS}}}} }$

步骤:(1) 求得 $ { ({G},{p}) }$ $ { {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G}) }$

(2) 求 $ {({G},{p})} $ 中含有秘密状态且满足无穷步不透明性的语言 $ { {{L}}_{{{\rm{IFS}}}}} $ 和满足K步不透明性的语言 $ {{{L}}_{{{{KSS}}}}} $

(3) 求 $ { {{V}}_{{G}}} $ $ {{{V}}_{{G}}^{{K}} }$

(4) 分别构建 $ { {{V}}_{{G}} }$ $ {{{V}}_{{G}}^{{K}} }$ 的马尔可夫链 $ {{{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{I}}}{{\rm{F}}}}\right) }$ $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{K}{S}}\right)} $

(5) 计算 $ { {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right)} $ $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right)} $

(6) 如果 $ { {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) < {{\theta }}_{{{\rm{IF}}}} }$ ,输出=系统 $ { ({G},{p}) }$ 具有随机无穷步不透明性;

如果 $ { {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) > {{\theta }}_{{{\rm{IF}}}} }$ ,输出=系统 $ { ({G},{p}) }$ 不具有随机无穷步不透明性;

如果 $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) < {{\theta }}_{{{{KS}}}}} $ ,输出=系统 $ { ({G},{p}) }$ 具有随机K步不透明性;

如果 $ { {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) > {{\theta }}_{{{{KS}}}} }$ ,输出=系统 $ { ({G},{p}) }$ 不具有随机K步不透明性。

算法复杂度分析:对于随机无穷步不透明性的验证,首先构造验证器 $ {{V}}_{{G}} $ 和马尔可夫链 $ ({{\rm{MC}}}){{\boldsymbol{M}}} $ 。其中 $ {{V}}_{{G}} $ 最多包含 $ \left|{X}\right|\times {2}^{{2}^{\left|{X}\right|\times \left|{X}\right|}} $ 个状态。得到 $ {{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{\rm{IF}}}}\right) $ ,求解线性方程组需要 $ {O}\left({{n}}_{{{\rm{max}}}}^{3}\right) $ 。最坏情况复杂度大小在 $ ({G},{p}) $ 的上呈双指数增长。对随机 $ {K} $ 步不透明性的验证,构造验证器 $ {{V}}_{{G}}^{{K}} $ 和马尔可夫链 $ ({{\rm{MC}}}){{{\boldsymbol{M}}}}_{{K}} $ 最多需要 $ \left|{X}\right|\times {2}^{{K}\times \left|{X}\right|\times \left|{X}\right|} $ 个状态, $ {O}({{n}}_{{{\rm{max}}}}^{3}) $ 求解线性方程。即最坏情况复杂度的大小在 $ {{V}}_{{G}} $ $ {{V}}_{{G}}^{{K}} $ 上都是指数级别。

例1  在访问服务器时,用户权限存在两种:超级用户权限和普通用户权限。用户在登入服务器后,首先要获取相应的权限。拥有超级用户权限或者普通账户权限的账号都可以访问服务器。服务器的账户系统非常严格,普通用户在做系统级别的更改时会受到用户权限的限制。用户登录服务器默认拥有普通用户权限。拥有超级用户权限的用户可以以普通用户的身份访问服务器,还可以执行普通用户无法进行的系统操作。同时,拥有超级用户权限的用户还可以授权其他用户为超级用户。超级用户权限为系统最高权限,不受安全系统限制。为防止入侵者获得超级用户权限,将“超级用户权限登入”看作是一个秘密状态。对于一个已设计的服务器系统,能否通过比较随机离散事件系统具有随机K步不透明性的阈值 $ {\theta } $ 与系统安全期望值,提前得到系统是否安全以便采取相应预防措施。

给定事件a为用户获取访问系统权限,事件b为超级用户权限转换成普通用户权限,事件c为访问系统。考虑如图1(a)所示用户访问服务器系统,其中状态1表示未登录用户,状态2表示用户以普通用户权限登入,状态3表示用户以超级用户权限登入,状态4为用户访问服务器系统。其中状态3被表示为秘密状态。当入侵者在入侵系统后可以确定用户是以超级用户权限登入(秘密状态)时,表明系统不具备随机 $ {K} $ 步不透明性。用字母ABCDEFH标识不同的状态集。将用户访问系统的事件看作随机离散事件系统的事件转移,投影为 $ {P}:{{\varSigma }}^{{*}} \to {{\varSigma }}_{{{\rm{o}}}}^{{*}} $ ,其中 $ {{\varSigma }}_{{{\rm{o}}}}=\left\{{a},{b},{c}\right\} $ $ {{X}}_{{s}}=\left\{3\right\} $ 为秘密状态。

图 1 系统 $ {G} $ 其中的可观事件 $ {{\varSigma }}_{{{\rm{obs}}}}=\{{a},{b},{c}\} $ 和秘密状态 $ {{X}}_{{s}}=\left\{3\right\} $ Figure 1 System $ {G} $ with $ {{\varSigma }}_{{{\rm{obs}}}}=\{{a},{b},{c}\} $ $ {{X}}_{{s}}=\left\{3\right\} $

步骤1:求 $ ({G},{p}) $ $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G}) $ ,如图2所示。

图 2 $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G}) $ Figure 2 $ {{{\rm{Obs}}}}_{{{\rm{tw}}}}({G}) $

步骤2:求得 $ ({G},{p}) $ 中含有秘密状态且满足K步不透明性的语言 ${{L}}_{{{KSS}}}=\{{a}{c},{a}{b}{c}\}。$

步骤3:求 $ {{V}}_{{G}}^{{K}} $ ,如图3(a)所示。

图 3 一个随机 $ {K} $ 步不透明性的例子,其中 $ {K}=1 $ Figure 3 An example of almost K-step opacity, where K =1

步骤4:构建 $ {{V}}_{{G}}^{{K}} $ 的马尔可夫链 $ {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) $ ,如图3(b)所示。

步骤5:计算 $ {{p}}_{{{M}}_{{K}}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) $

$ \left\{ \begin{array}{l} {\boldsymbol{P}}\left({{M}}_{1}\right) =0.9 {\boldsymbol{P}}\left({{M}}_{2}\right) +0.1 {\boldsymbol{P}}\left({{M}}_{3}\right) \\ {\boldsymbol{P}}\left({{M}}_{2}\right) ={\boldsymbol{P}}\left({{M}}_{4}\right) \\ {\boldsymbol{P}}\left({{M}}_{3}\right) =0.1{\boldsymbol{P}}\left({{M}}_{5}\right) +0.9{\boldsymbol{P}}\left({{M}}_{4}\right) \end{array} \right.$

由于 $ \boldsymbol{P}\left({{M}}_{2}\right) $ $ \boldsymbol{P}\left({{M}}_{4}\right) $ 是一个自由项,所以上述方程的解不唯一。设 $ \boldsymbol{P}\left({{M}}_{2}\right) =\boldsymbol{P}\left({{M}}_{4}\right) ={ }0 $ ,而 $ \boldsymbol{P}\left({{M}}_{5}\right) =1 $ ,则 $\boldsymbol{P}=\left[0.090\;0.101\right]$ 。因此 ${{\varSigma }}_{{s}\in {{L}}_{{{{KS}}}}^{{P}}}{p}({s})={{p}}_{{M}}^{{{\rm{abs}}}}\left({{Q}}_{{{{KS}}}}\right) =$ ${{\pi }}_{0}\left({{M}}_{1}\right) \times \boldsymbol{P}\left({{M}}_{1}\right) ={ }0.09 $ 。当系统安全期望值大于0.09时,此系统为随机1步不透明性。即入侵者无法在用户访问系统时确定用户是否是以超级用户权限登入。在设计这样的服务器时,可以通过算法1来判断所设计的系统是否安全。一旦所设计的系统不安全,则可以为保障拥有超级用户权限的用户不被发现而采取相应的控制手段(如提高普通用户权限使用频率、降低超级用户权限使用频率等),以规避超级用户权限被盗用的发生。

6 结论

本文研究了基于状态的可观映射下随机离散事件系统是否具有随机无穷步不透明性和随机 $ {K} $ 步不透明性问题。将双向观测器引入随机离散事件系统不透明性研究,构造随机无穷步不透明性和随机 $ {K} $ 步不透明性的验证器,提出算法以验证系统是否具有随机无穷步不透明性和随机 $ {K} $ 步不透明性。

参考文献
[1]
SAMPATH M, SENGUPTA R, LAFORTUNE S, et al. Diagnosability of discrete-event systems[J]. IEEE Transactions on Automatic Control, 1995, 40(9): 1555-1575. DOI: 10.1109/9.412626.
[2]
THORSLEY D, TENEKETZIS D. Diagnosability of stochastic discrete-event systems[J]. IEEE Transactions on Automatic Control, 2005, 50(4): 476-492. DOI: 10.1109/TAC.2005.844722.
[3]
QIU W, KUMAR R. Decentralized failure diagnosis of discrete event systems[J]. IEEE Transaction on Systems, Man, and Cybernetics-part A:Systems and Humans, 2006, 36(2): 384-395. DOI: 10.1109/TSMCA.2005.853503.
[4]
LIU F C, QIU D. Safe diagnosability of stochastic discrete event systems[J]. IEEE Transaction on Automatic Control, 2008, 53(5): 1291-1296. DOI: 10.1109/TAC.2008.921035.
[5]
ZAYTOON J, LAFORTUNE S. Overview of fault diagnosis methods for discrete event systems[J]. Annual Reviews in Control, 2013, 37(2): 308-320. DOI: 10.1016/j.arcontrol.2013.09.009.
[6]
JACOB R, LESAGE J, FAURE J. Overview of discrete event systems opacity: models, validation, and quantification[J]. Annual Reviews in Control, 2015, 48(7): 174-181.
[7]
ZHANG B, SHU S, LIN F. Maximum information release while ensuring opacity in discrete Event systems[J]. IEEE Transactions on Automation Science & Engineering, 2015, 12(3): 1067-1079.
[8]
BÉRARD B, CHATTERJEE K, SZNAJDER N. Probabilistic opacity for Markov decision processes[J]. Information Processing Letters, 2015, 115(1): 52-59. DOI: 10.1016/j.ipl.2014.09.001.
[9]
HADJICOSTIS C N, KEROGLOU C. Opacity formulations and verification in discrete event systems[C]// Proceedings of the 2014 IEEE Emerging Technology and Factory Automation (ETFA) , Barcelona: IEEE, 2014, 1-12.
[10]
ANOOSHIRAVAN S A, HADJICOSTIS C N. Verification of initial state opacity in security applications of discrete event systems[J]. Information Sciences, 2013, 246(14): 115-132.
[11]
DUBREIL J, DARONDEAU P, MARCHAND H. Opacity enforcing control synthesis[C]// 2008 9th International Workshop on Discrete Event Systems, Gothenburg: IEEE, 2008, 28-35.
[12]
SABOORI A, HADJICOSTIS C N. Opacity-enforcing supervisory strategies for secure discrete event systems[C]// 2008 47th IEEE Conference on Decision and Control, Cancun: IEEE, 2008, 889-894.
[13]
SABOORI A, HADJICOSTIS C N. Verification of K-step opacity and analysis of its complexity[C]// Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, Shanghai: IEEE, 2009, 205-210.
[14]
YIN X, LAFORTUNE S. A new approach for the verification of infinite-step and K-step opacity using two-way observers [J]. Automatica, 2017, 80: 162-171. DOI: 10.1016/j.automatica.2017.02.037.
[15]
XIANG L, LI Z, WANG W, et al. Infinite-step opacity and K-step opacity of stochastic discrete-event systems [J]. Automatica, 2019, 99: 276-274.