Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.04067 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914447503654912 |
|---|---|
| author | Cui, Bohan Zhao, Jianing Chen, Yu Abate, Alessandro Kwiatkowska, Marta Yin, Xiang |
| author_facet | Cui, Bohan Zhao, Jianing Chen, Yu Abate, Alessandro Kwiatkowska, Marta Yin, Xiang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_04067 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach Cui, Bohan Zhao, Jianing Chen, Yu Abate, Alessandro Kwiatkowska, Marta Yin, Xiang Systems and Control 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. |
| title | Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2604.04067 |