随机系统中一类观测性质的证书合成：统一方法
系统与控制
2026-04-07 v1 系统与控制
摘要
本文研究了连续状态空间上随机动力系统的概率形式验证。受状态估计和信息流安全问题的启发，我们引入了观测性质的概念，用于刻画外部观察者从系统输出中可以推断出的信息。这些性质被表述为基于有限迹上 HyperLTL 的概率超性质，从而得到一个统一框架，涵盖了文献中若干单独研究的已有概念。我们将验证问题归约为在增广结构上的可达性分析，该结构将系统动力学与规范的自动机表示相结合。基于这一构造，我们发展了随机障碍证书，为性质满足提供概率保证，同时避免了显式的状态空间离散化。所提出框架的有效性通过一个案例研究得到了验证。
引用
@article{arxiv.2604.04067,
title = {Certificates Synthesis for A Class of Observational Properties in Stochastic Systems: A Unified Approach},
author = {Bohan Cui and Jianing Zhao and Yu Chen and Alessandro Abate and Marta Kwiatkowska and Xiang Yin},
journal= {arXiv preprint arXiv:2604.04067},
year = {2026}
}