论文标题
用于分层概率模型的抽象再填充
Abstraction-Refinement for Hierarchical Probabilistic Models
论文作者
论文摘要
马尔可夫决策过程是一种无处不在的形式主义，用于建模具有非确定性和概率行为的系统。这些模型的验证应遵守著名的状态爆炸问题。我们通过利用具有重复零件的层次结构来缓解这个问题。这种结构不仅在机器人技术中自然发生，而且在描述网络协议的概率程序中也出现。这样的程序通常会反复称呼具有相似行为的子例程。在本文中，我们关注的是当地案例，其中子例程对整个系统状态的影响有限。加速对此类程序的分析的关键思想是（1）将子例程的行为视为不确定的行为，并且仅通过详细分析（如果需要）消除这种不确定性，（2）将类似的子例程抽象成参数模板，然后分析该模板。这两个想法嵌入到分析层次MDP的抽象循环中。原型实施显示了该方法的功效。
Markov decision processes are a ubiquitous formalism for modelling systems with non-deterministic and probabilistic behavior. Verification of these models is subject to the famous state space explosion problem. We alleviate this problem by exploiting a hierarchical structure with repetitive parts. This structure not only occurs naturally in robotics, but also in probabilistic programs describing, e.g., network protocols. Such programs often repeatedly call a subroutine with similar behavior. In this paper, we focus on a local case, in which the subroutines have a limited effect on the overall system state. The key ideas to accelerate analysis of such programs are (1) to treat the behavior of the subroutine as uncertain and only remove this uncertainty by a detailed analysis if needed, and (2) to abstract similar subroutines into a parametric template, and then analyse this template. These two ideas are embedded into an abstraction-refinement loop that analyses hierarchical MDPs. A prototypical implementation shows the efficacy of the approach.
