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.
|Titolo:||Decidability of opacity verification problems in labeled Petri net systems|
|Autori interni:||SEATZU, CARLA|
|Data di pubblicazione:||2017|
|Tipologia:||1.1 Articolo in rivista|