Initial state opacity in stochastic DES

A non-deterministic finite automaton is initial-state opaque if the membership of its true initial state to a given set of secret states S remains opaque (i.e., uncertain) to an intruder who observes system activity through some natural projection map. By establishing that the verification of initial state opacity is equivalent to the language containment problem, earlier work has established that the verification of initial state opacity is a PSPACE-complete problem. In this paper, motivated by the desire to incorporate probabilistic (likelihood) information, we extend the notion of initial state opacity to stochastic discrete event systems. Specifically, we consider systems that can be modeled as probabilistic finite automata, and introduce and analyze the notions of almost initial state opacity and step-based almost initial state opacity, both of which hinge on the a priori probability that the given system generate behavior that violates initial-state opacity. We also discuss how almost initial state opacity and step-based almost initial state opacity can be verified, and analyze the complexity of the proposed verification methods.