ProbReach：随机混合系统的已验证概率 Delta-可达性
计算机科学中的逻辑
2015-03-06 v3 系统与控制
摘要
我们介绍了 ProbReach，这是一种用于验证随机混合系统概率可达性的工具，即计算系统到达状态空间不安全区域的概率。具体而言，ProbReach 将计算一个任意小的区间，并保证该区间包含所需的概率。即使是线性混合系统，标准（非概率）可达性也是不可判定的。在 ProbReach 中，我们采用了较弱的 delta-可达性概念，其中不安全区域由用户定义的参数 (delta) 进行过近似。这种选择会导致误报，但也使得 virtually 任何混合系统的可达性问题变得可判定。在 ProbReach 中，我们实现了一种适用于随机行为由随机初始条件给出的混合系统的概率版 delta-可达性。本文介绍了 ProbReach 的功能，概述了其并行实现，并展示了涉及高度非线性混合系统的多个基准测试的结果。
引用
@article{arxiv.1410.8060,
title = {ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems},
author = {Fedor Shmarov and Paolo Zuliani},
journal= {arXiv preprint arXiv:1410.8060},
year = {2015}
}
备注
HSCC 2015