Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach

Zhang, Kuize; Yin, Xiang und Zamani, Majid (2019): Opacity of Nondeterministic Transition Systems: A (Bi)Simulation Relation Approach. In: IEEE Transactions on Automatic Control, Bd. 64, Nr. 12: S. 5116-5123

Abstract

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.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0018-9286
• Sprache: Englisch