Automaton

Physics

Undecidable problem

Mathematics

Opacity

Algorithm

Optics

Automata theory

Decidability

Nondeterministic finite automaton

Nondeterministic algorithm

Computer science

Theoretical computer science

IEEE Transactions on Automatic Control

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.

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