Opacity of nondeterministic transition systems: A (bi)simulation relation approach
Logic in Computer Science
2018-09-14 v2 Optimization and Control
Abstract
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.
Cite
@article{arxiv.1802.03321,
title = {Opacity of nondeterministic transition systems: A (bi)simulation relation approach},
author = {Kuize Zhang and Xiang Yin and Majid Zamani},
journal= {arXiv preprint arXiv:1802.03321},
year = {2018}
}
Comments
21 pages, partially presented at IEEE CDC 2017