2018/02/09 by Kuize Zhang, Xiang Yin, Zhang, Kuize +3 · 2 citations
Computer Science · Decision Sciences · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Optimization and Control (math.OC) #Simulation Techniques and Applications
paper · pdf · doi:10.48550/arxiv.1802.03321
openalex publication_date 2018/02/09 · openalex created_date 2018/02/23 · openalex updated_date 2026/07/28
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.