Logo Logo
Switch Language to German
Zhang, Kuize; Yin, Xiang; Zamani, Majid (2019): Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach. In: IEEE Transactions on Automatic Control, Vol. 64, No. 12: pp. 5116-5123
Full text not available from 'Open Access LMU'.


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.