随机布尔可满足性问题的广义 Craig 插值及其在概率状态可达性与区域稳定性中的应用
计算机科学中的逻辑
2015-07-01 v2
摘要
随机布尔可满足性问题（SSAT）由 Papadimitriou 于 1985 年通过将随机化量词引入命题可满足性以添加不确定性概率模型而提出。SSAT 具有诸多应用，其中包括符号化表示的马尔可夫决策过程的概率有界模型检测（PBMC）。本文为 SSAT 框架识别了 Craig 插值的概念，并基于 SSAT 的归结演算开发了一种计算此类插值的算法。作为这一新颖 Craig 插值概念的潜在应用领域，我们探讨了概率系统的符号分析。我们首先研究了插值在概率状态可达性分析中的应用，将采用 PBMC 的证伪过程转化为针对概率安全性质的验证技术。此外，我们提出了一种基于插值的概率区域稳定性方法，能够验证在某一区域内稳定的概率足够大。
引用
@article{arxiv.1206.4444,
title = {Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability},
author = {Tino Teige and Martin Fränzle},
journal= {arXiv preprint arXiv:1206.4444},
year = {2015}
}