Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
复制标题
DOI：
10.1007/978-3-540-78929-1_13
复制
发表时间：
2008-04
影响因子：
3.9
通讯作者：
M. Fränzle;H. Hermanns;Tino Teige
中科院分区：
文献类型：
--
作者：
M. Fränzle;H. Hermanns;Tino Teige
混合动力系统的概率行为的分析是出了名的困难。为了使这种系统的机械化分析，我们扩展了算术可满足性模理论求解（SMT）的推理能力，通过全面处理随机（a.k.a.随机）量化的混合布尔算术约束系统内的离散变量。这为概率混合自动机的完全符号分析提供了技术基础。推广基于SMT的混合自动机的有界模型检查[2，11]，随机SMT允许直接和完全符号化的分析概率混合自动机的概率有界可达性问题，而无需通过中间有限状态抽象来近似。
The analysis of hybrid systems exhibiting probabilistic behaviour is notoriously difficult. To enable mechanised analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theory solving (SMT) by a comprehensive treatment of randomized (a.k.a. stochastic) quantification over discrete variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a fully symbolic analysis of probabilistic hybrid automata. Generalizing SMT-based bounded model-checking of hybrid automata [2,11], stochastic SMT permits the direct and fully symbolic analysis of probabilistic bounded reachability problems of probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.