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

【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.更多还原