Reduced-complexity verification for initial-state opacity in modular discrete event systems
Ημερομηνία
2010ISBN
978-3-902661-79-1Source
IFAC Proceedings Volumes (IFAC-PapersOnline)IFAC Proceedings Volumes (IFAC-PapersOnline)
Volume
10Pages
78-83Google Scholar check
Keyword(s):
Metadata
Εμφάνιση πλήρους εγγραφήςΕπιτομή
In this paper, we propose and analyze reduced-complexity methodologies for verifying initial-state opacity in modular discrete event systems. Initial-state opacity requires that the membership of the system initial state to a given set of secret states S remains opaque (uncertain) to an intruder who has complete knowledge of the system model and observes system activity through some natural projection map. In the modular setting we consider, the given system is modeled as a composition (synchronous product) of M modules -G1,G 2,., GM} where each module Gi is a non-deterministic finite automaton with Ni states with the set of secret states S is of the form S = {(x1, x2,., xM)|x i ε Si}, where Si is the set of secret states for module Gi. Assuming that the pairwise shared events are pairwise observable and that the intruder observes events that are observable in at least one module, we provide a modular algorithm for verifying initial-state opacity with O(MNM-12N2) state and time complexity, where N = maxi Ni. This is a considerable reduction compared to the O(2(NM)2 ) state and time complexity of the centralized verification method, which verifies initial-state opacity by considering the composed system as a monolithic system.