Verification and Refutation of Probabilistic Specifications via Games
Verification and Refutation of Probabilistic Specifications via Games
复制标题
通过游戏验证和反驳概率规范
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Huth
中科院分区：
文献类型：
--
作者：
M. Kattenbelt;M. Huth
我们开发了一个基于抽象的框架
检查马尔可夫决策过程（MDP）的概率规范，使用
随机两人游戏抽象（即“游戏”），
Kwiatkowska等人作为基金会。
我们为这些游戏抽象定义了一个抽象前序，
使我们能够为每个MDP识别许多新的游戏抽象-
范围从紧凑和不精确到复杂和精确。
这增加了以精度换取效率的能力
是可伸缩软件模型关键
检查，因为精确的抽象在构造中是昂贵的。
实践
此外，我们还建立了一个四值概率计算树
逻辑（PCTL）游戏抽象语义。
前序和PCTL语义一起构成了一个强大的验证，
MDP的任意PCTL属性的反驳框架。
We develop an abstraction-based framework
to check probabilistic specifications of Markov Decision Processes (MDPs) using
the stochastic two-player game abstractions (ie ``games') developed by
Kwiatkowska et al. as a foundation.
We define an abstraction preorder for these game abstractions which
enables us to identify many new game abstractions for each MDP ---
ranging from compact and imprecise to complex and precise.
This added ability to trade precision for efficiency
is crucial for scalable software model
checking, as precise abstractions are expensive to construct in
practice.
Furthermore, we develop a four-valued probabilistic computation tree
logic (PCTL) semantics for game abstractions.
Together, the preorder and PCTL semantics comprise a powerful verification and
refutation framework for arbitrary PCTL properties of MDPs.