Verification of initial-state opacity in Petri nets

SEATZU, CARLA;GIUA, ALESSANDRO
2015-01-01

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).
2015
Petri nets;discrete event systems;formal verification;observers;reachability analysis;BRG;DES;Petri net system;basis reachability graph;discrete event systems;external observer;initial-state opacity;initial-state opaque;intruder;labeled Petri nets;secret;system evolution;verification;Automata;Complexity theory;Explosions;Fault diagnosis;Observers;Petri nets;Yttrium
Files in This Item:
File Size Format  
15cdc_b_draft.pdf

Solo gestori archivio

Type: versione post-print
Size 682.7 kB
Format Adobe PDF
& nbsp; View / Open   Request a copy
682.7 kB Adobe PDF & nbsp; View / Open   Request a copy

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Questionnaire and social

Share on:
Impostazioni cookie