Infinite-step opacity of nondeterministic finite transition systems: A bisimulation relation approach

It is known that the problem of verifying the infinite-step opacity of nondeterministic finite transition systems (NFTSs)is PSPACE-hard. In this paper, we investigate whether it is possible to use classical bisimulation relation to come up with abstract NFTSs and verify the infinite-step opacity of original NFTSs over their abstractions. First, we show that generally bisimulation relation does not preserve infinitestep opacity. Second, by adding some additional conditions to bisimulation relation, we prove that a stronger version of bisimulation relation, called here opacity-preserving bisimulation relation, preserves infinite-step opacity. Therefore, if one can find an abstract NFTS for a large NFTS under an opacity-preserving bisimulation relation, then the infinite-step opacity of the original NFTS can be verified by investigating that over the abstract NFTS. Finally, we show that under some mild assumptions, the quotient relation between an NFTS and its quotient system becomes opacity-preserving bisimulation relation which provides a scheme for constructing opacity-preserving abstractions of large- scale NFTSs. We show the effectiveness of the results using several examples throughout the paper.