Infinite-step opacity and K-step opacity of stochastic discrete-event systems

Abstract Opacity is an important information-flow property that arises in security and privacy analysis of cyber–physical systems. Among many different notions of opacity, K -step opacity requires that the intruder can never determine unambiguously that the system was at a secret state for any specific instant within K steps prior to that particular instant. This notion becomes infinity-step opacity when K goes to infinity. Existing works on the analysis of infinite-step opacity and K -step opacity only provide a binary characterization, i.e., a system is either opaque or non-opaque. To analyze infinite-step and K -step opacity more quantitatively, in this paper, we investigate the verification of infinite-step and K -step opacity in the context of stochastic discrete-event systems. A new notion of opacity, called almost infinite-step opacity (respectively, almost K -step opacity), is proposed to capture whether or not the probability of violating infinite-step opacity (respectively, K -step opacity) is smaller than a given threshold. We also provide effective algorithms for the verification of almost infinite-step opacity and almost K -step opacity.