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

TL;DR

This paper presents a unified probabilistic verification framework for stochastic systems using observational properties, automata, and barrier certificates to provide guarantees without discretizing the state space.

Contribution

It introduces a novel approach combining HyperLTL-based properties, reachability analysis, and stochastic barrier certificates for probabilistic verification.

Findings

Framework effectively verifies observational properties in stochastic systems.

Barrier certificates provide probabilistic guarantees without state-space discretization.

Case study demonstrates practical applicability of the 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.