UNICA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Cagliari dal mese di luglio 2015.
EnglishA Petri net system is said to be initial-state opaque if its initial state remains opaque to an external observer (called an intruder). In other words, the intruder is never able to ascertain that the initial state belongs to a given set of states (called a secret) based on its observation of the system's evolution. This paper addresses the problem of verifying initial-state opacity in discrete event systems (DES) modeled by labeled Petri nets. An efficient approach to verifying initial-state opacity is proposed based on the notion of basis reachability graph (BRG).
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
| Titolo: | Verification of initial-state opacity in Petri nets |
| Autori: | |
| Data di pubblicazione: | 2015 |
| Abstract: | A Petri net system is said to be initial-state opaque if its initial state remains opaque to an external observer (called an intruder). In other words, the intruder is never able to ascertain that the initial state belongs to a given set of states (called a secret) based on its observation of the system's evolution. This paper addresses the problem of verifying initial-state opacity in discrete event systems (DES) modeled by labeled Petri nets. An efficient approach to verifying initial-state opacity is proposed based on the notion of basis reachability graph (BRG). |
| Handle: | http://hdl.handle.net/11584/178030 |
| Tipologia: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Copyright © 2020