Online Verification and Enforcement of Sequential <italic>K</italic>-Opacity in Extended Probabilistic Automata

Abstract

In the context of extended probabilistic automata, this study focuses on an information flow property, called opacity, of discrete event systems. The achievement of this research is the formulation and in-depth analysis of what is termed sequential k-opacity. This metric, through its detailed assessment, marks an explicit and visible advancement beyond the existing paradigms for measuring system opacity. It introduces an improved method for analyzing the probability of event sequences leading to confidential states within a system. An approach of such a comprehensive nature is essential for a detailed analysis of opacity in systems typified by deterministic and stochastic elements. Furthermore, this work incorporates a numerical case study that provides a baseline for further investigations in practical applications, thereby validating the proposed framework’s usefulness. The research progresses to explore novel approaches to the reinforcement and persistence of system opacity within extended probabilistic automata. Among these approaches, the strategic use of fake events is critical as it is a fundamental tool for enhancing system security and secrecy, which plays an important role in protecting sensitive and secret data by effectively hiding the real status of the system from outside inspection.

Keywords

• Discrete event system
• extended probabilistic automaton
• sequential k-opacity
• system opacity