# Opacity of nondeterministic transition systems: A (bi)simulation relation approach

arXiv: https://arxiv.org/abs/1802.03321 · HTML: https://mlsanity.com/paper/1802.03321/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Feb 2018.

## Built on by (most cited first, 2 of 2)

- [Hyper Strategy Logic](https://mlsanity.com/paper/2403.13741/) (2024)
- [Decentralized Planning Using Probabilistic Hyperproperties](https://mlsanity.com/paper/2502.13621/) (2025)

## Abstract (arXiv)

In this paper, we propose several opacity-preserving (bi)simulation relations for general nondeterministic transition systems (NTS) in terms of initial-state opacity, current-state opacity, K-step opacity, and infinite-step opacity. We also show how one can leverage quotient construction to compute such relations. In addition, we use a two-way observer method to verify opacity of nondeterministic finite transition systems (NFTSs). As a result, although the verification of opacity for infinite NTSs is generally undecidable, if one can find such an opacity-preserving relation from an infinite NTS to an NFTS, the (lack of) opacity of the NTS can be easily verified over the NFTS which is decidable.