화학공학소재연구정보센터
IEEE Transactions on Automatic Control, Vol.64, No.12, 5116-5123, 2019
Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach
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.