Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
复制标题
DOI：
10.1109/tac.2019.2908726
复制
发表时间：
2018-02
影响因子：
6.8
通讯作者：
Kuize Zhang;Xiang Yin;Majid Zamani
中科院分区：
文献类型：
--
作者：
Kuize Zhang;Xiang Yin;Majid Zamani
本文从初始状态不透明度、当前状态不透明度、$K$步不透明度和无限步不透明度的角度，提出了几种不确定性过渡系统（nts）的不透明度保持（bi）模拟关系。我们还展示了如何利用商结构来计算这种关系。因此，尽管无限NTS的不透明性验证问题通常是不可判定的，但如果能找到无限NTS与有限NTS之间的不透明性保持关系，则无限NTS的（缺乏）不透明性可以很容易地在有限NTS上进行验证，这是可判定的。
In this paper, we propose several opacity-preserving (bi)simulation relations for nondeterministic transition systems (NTSs) in terms of initial-state opacity, current-state opacity, $K$-step opacity, and infinite-step opacity. We also show how one can leverage quotient constructions to compute such relations. As a result, although the opacity verification problem for infinite NTSs is generally undecidable, if one can find such an opacity-preserving relation from an infinite NTS to a finite one, the (lack of) opacity of the infinite NTS can be easily verified over the finite one, which is decidable.