Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach

Bohan Cui, Jianing Zhao, Yu Chen, Alessandro Abate, Marta Kwiatkowska, Xiang Yin

Abstract

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.

Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach

Abstract

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.

Paper Structure

This paper contains 13 sections, 6 theorems, 38 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Partially Observable Stochastic Systems
  4. Observational Equivalence and State Estimates
  5. A Unified Formulation of Observational Properties
  6. Observational Properties
  7. Detectability
  8. Opacity
  9. A Unified Formulation of Observational Properties
  10. Instantiations of the Unified Formulation
  11. Certificates for Observational Properties
  12. Case Studies
  13. Conclusion

Key Result

Proposition 1

Let $\mathcal{M}$ be a POSS, $\epsilon \in \mathbb{R}_{\geq 0}$ denote the measurement precision, $\lambda \in \mathbb{R}_{\geq 0}$ denote the state detection tolerance, and $p \in (0,1]$ denote the required detection probability. Then $\blacktriangleleft$$\blacktriangleleft$

Figures (1)

  • Figure E1: The value of the certificate $\mathbf{V}$ at time instant $t=0$.

Theorems & Definitions (19)

  • Definition 1: $\epsilon$-Approximate Observational Equivalence
  • Definition 2: State Estimates
  • Definition 3: Approximate Detectability
  • Definition 4: Approximate Opacity
  • Remark 1
  • Proposition 1
  • proof
  • Proposition 2
  • Definition 5: Verification Structure
  • Theorem 1
  • ...and 9 more