2019/09/09 by Lan, Hao, Tong, Yin, Guo, Jin +1
#FOS: Electrical engineering #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · doi:10.48550/arxiv.1909.05138
This paper addresses the problem of infinite-step opacity and K-step opacity of discrete event systems modeled with Petri nets. A Petri net system is said to be infinite-step/K-step opaque if all its secret states remains opaque to an intruder for any instant within infinite/K steps. In other words, the intruder is never able to ascertain that the system used to be in a secrete state within infinite/K steps based on its observation of the systems evolution. Based on the notion of basis reachability and the twoway observer, an efficient approach to verify infinite-step opacity and K-step opacity is proposed.