连续时间随机系统有限时约束占有时间的定量验证
系统与控制
2026-04-22 v1 系统与控制
摘要
本文关注连续时间随机系统（由随机微分方程 SADEs 描述）在有限时段内受约束占有时间的定量验证问题。不同于传统可达性分析仅关注单事件属性（如进入目标集），许多自主任务（包括监视、无线充电和化学混合）要求系统在保持严格安全约束的前提下，在目标区域内累积规定的时长。我们提出了障碍证书框架，用于计算该类累积规格在有限时窗内被满足的概率的严格上、下界。通过引入一个在系统到达安全集边界时冻结的停机过程，我们推导出三类证书：一种用于上界，两种用于下界。本文通过使用半正定规划实现的数值示例验证了所提方法的有效性。
引用
@article{arxiv.2604.19014,
title = {Quantitative Verification of Finite-Time Constrained Occupation Measures for Continuous-time Stochastic Systems},
author = {Bai Xue and C. -H. Luke Ong},
journal= {arXiv preprint arXiv:2604.19014},
year = {2026}
}