Show simple item record

dc.contributor.authorSaboori, A.en
dc.contributor.authorHadjicostis, Christoforos N.en
dc.creatorSaboori, A.en
dc.creatorHadjicostis, Christoforos N.en
dc.description.abstractIn this paper, we formulate and analyze methodologies for verifying the notion of initial-state opacity in discrete event systems that are modeled as non-deterministic finite automata with partial observation on their transitions. A system is initial-state opaque if the membership of its true initial state to a set of secret states remains opaque (i.e., uncertain) to an intruder who observes system activity through some projection map. Initial-state opacity can be used to characterize security requirements in a variety of applications, including tracking problems in sensor networks. In order to model and analyze the intruder capabilities regarding initial-state opacity, we first address the initial-state estimation problem in a non-deterministic finite automaton via the construction of an initial-state estimator. We analyze the properties and complexity of the initial-state estimator, and show how the complexity of the verification method can be greatly reduced in the special case when the set of secret states is invariant. We also establish that the verification of initial-state opacity is a PSPACE-complete problem. © 2013 Elsevier Inc. All rights reserved.en
dc.sourceInformation Sciencesen
dc.subjectDiscrete event simulationen
dc.subjectDiscrete event systemen
dc.subjectAutomata theoryen
dc.subjectState estimationen
dc.subjectSensor networksen
dc.subjectInitial stateen
dc.subjectSecurity applicationen
dc.subjectNondeterministic finite automatonen
dc.subjectPspace-complete problemsen
dc.subjectPartial observationen
dc.subjectSecurity requirementsen
dc.subjectVerification methoden
dc.subjectFormal methods in securityen
dc.subjectFormal methods in security analysisen
dc.subjectInitial state estimationen
dc.subjectInitial state estimatoren
dc.subjectTracking in sensor networken
dc.titleVerification of initial-state opacity in security applications of discrete event systemsen
dc.description.issueJournal Articleen
dc.description.endingpage132Πολυτεχνική Σχολή / Faculty of EngineeringΤμήμα Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών / Department of Electrical and Computer Engineering
dc.contributor.orcidHadjicostis, Christoforos N. [0000-0002-1706-708X]

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record