Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach
This work addresses verification challenges in state estimation and security for stochastic systems, representing an incremental advance by unifying prior concepts.
The paper tackles the probabilistic formal verification of stochastic dynamical systems by introducing observational properties, which unify existing notions and are reduced to reachability analysis, with effectiveness demonstrated through a case study.
In this paper, we investigate the probabilistic formal verification of stochastic dynamical systems over continuous state spaces. Motivated by problems in state estimation and information-flow security, we introduce the notion of observational properties, which characterize the inferences an external observer can draw from system outputs. These properties are formulated as probabilistic hyperproperties based on HyperLTL over finite traces, yielding a unified framework that subsumes several existing notions studied separately in the literature. We reduce the verification problem to reachability analysis over an augmented structure that integrates the system dynamics with an automaton representation of the specification. Building on this construction, we develop stochastic barrier certificates that provide probabilistic guarantees for property satisfaction while avoiding explicit state-space discretization. The effectiveness of the proposed framework is demonstrated through a case study.