基于双向观测器的随机离散事件系统的不透明性

Opacity Verification in Stochastic Discrete Event Systems Using Two-way Observers

本文针对随机系统模型,研究随机离散事件系统的不透明性。首先对随机无穷步不透明性和随机K步不透明性进行形式化。通过构造一个基于双向观测器的验证器,得到一个运用双向观测器验证系统随机无穷步不透明性和随机K步不透明性的充分必要条件。最后提出一个基于双向观测器的随机无穷步不透明性和随机K步不透明性验证算法。

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.