Verification of infinite-step and K-step opacity Using Petri Nets
Systems and Control
2019-09-12 v1 Systems and Control
Abstract
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.
Cite
@article{arxiv.1909.05138,
title = {Verification of infinite-step and K-step opacity Using Petri Nets},
author = {Hao Lan and Yin Tong and Jin Guo and Carla Seatzu},
journal= {arXiv preprint arXiv:1909.05138},
year = {2019}
}
Comments
8 pages, 5 figures. arXiv admin note: text overlap with arXiv:1908.09604, arXiv:1903.07827, arXiv:1903.09298