Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4999899 | Automatica | 2017 | 6 Pages |
Abstract
A system is said to be opaque if an intruder that observes its evolution through a mask cannot infer that the system's evolution belongs to a given secret behavior. Opacity verification is the problem of determining whether the system is opaque with respect to a given secret or not. In this paper we address the decidability of the opacity verification problem. Using reduction approaches, we show that verification of initial-state, current-state, and language opacity is undecidable in labeled Petri nets.
Related Topics
Physical Sciences and Engineering
Engineering
Control and Systems Engineering
Authors
Yin Tong, Zhiwu Li, Carla Seatzu, Alessandro Giua,