随机布尔可满足性问题的广义Craig插值及其在概率状态可达性和区域稳定性中的应用
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability
摘要：
随机布尔可满足性（SSAT）问题是由Papadimitriou在1985年通过随机量化给命题可满足性增加一个不确定性的概率模型时提出的。SSAT有许多应用，其中概率有界模型检验（PBMC）的符号表示的马尔可夫决策过程。本文确定了克雷格插值的SSAT框架的概念，并开发了一个算法，计算这样的插值的基础上的分辨率演算SSAT。作为一个潜在的应用领域，这个新的概念克雷格插值，我们解决概率系统的符号分析。我们首先调查使用插值的概率状态可达性分析，把证伪过程采用PBMC概率安全属性的验证技术。此外，我们提出了一种基于插值的方法来概率区域稳定性，能够验证在某些区域内稳定的概率足够大。
英文摘要：
The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpolation, we address the symbolic analysis of probabilistic systems. We first investigate the use of interpolation in probabilistic state reachability analysis, turning the falsification procedure employing PBMC into a verification technique for probabilistic safety properties. We furthermore propose an interpolation-based approach to probabilistic region stability, being able to verify that the probability of stabilizing within some region is sufficiently large.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
