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

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. (C) 2018 Elsevier Ltd. All rights reserved.