Reduced-Complexity Verification for Initial-State Opacity in Modular Discrete Event Systems

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, G2, …, 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)|xi 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.