摘要：AbstractOpacity is an important information secure property. A system is said to be infinite-step opaque if the intruder is never able to ascertain that the system is or has been in a secret state at some time, based on its observation of the system evolution. This work aims to verify infinite-step opacity of discrete event systems modeled with labeled Petri nets. Based on the notion of basis reachability graph, a new structure called basis two-way observer is proposed to check infinite-step opacity of a bounded system, which is shown to be more efficient than the standard method based on the reachability graph.
