基于噪声划分的通用随机系统形式化抽象

验证具有复杂噪声分布的安全关键随机系统的性能是困难的。我们引入一种通用流程，用于对具有非标准（例如非仿射、非对称、非单峰）噪声分布的非线性随机系统进行有限抽象以用于验证。该方法通过对噪声域进行有限划分，借助转移概率区间构造系统的区间马尔可夫链（IMC）抽象。噪声划分允许一类通用的分布与结构，包括乘性和混合模型，并兼容已知系统与数据驱动系统。针对关于噪声单调的系统，给出了最优转移界所需的划分，并为仿射和乘性结构提供了显式划分。由于抽象过程的可靠性，在 IMC 上的验证可针对时序逻辑规范给出随机系统的保证。此外，我们提出了一种无需精化的新算法，可改善验证结果。针对具有非高斯噪声的线性和非线性系统（含一个数据驱动示例）的案例研究，展示了该方法在不过度保守情况下的通用性与有效性。