期刊
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 64, 期 12, 页码 5116-5123出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2019.2908726
关键词
(Bi)simulation relation; nondeterministic transition system; opacity
资金
- German Research Foundation [ZA 873/1-1]
- National Natural Science Foundation of China [61803259, 61833012, 61603109]
- Natural Science Foundation of Heilongjiang Province of China [LC2016023]
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据