论文标题
与概率模型检查的象征探索和消除
Symblicit Exploration and Elimination for Probabilistic Model Checking
论文作者
论文摘要
二进制决策图可以紧凑地表示大量状态，从而减轻模型检查中的状态空间爆炸问题。但是，概率系统需要存储有理数的多末端图。对于具有许多不同概率和迭代数字算法（如价值迭代）的模型，它们的效率低下。在本文中，我们提出了一种检查马尔可夫链和相关概率模型的新的“符合性”方法：我们首先生成一个决策图，象征性地收集所有可及的状态及其前任。然后，我们将限制在一对一的状态下，以明确的部分状态空间表示。每当国家的所有前辈都已凝结时，我们就会以保持所有相关概率和奖励的方式从明确的状态空间中消除它。因此，我们任何时候都将很少的明确状态保留在内存中。实验表明，非常大的模型可以通过这种方式进行模型检查，而记忆消耗非常低。
Binary decision diagrams can compactly represent vast sets of states, mitigating the state space explosion problem in model checking. Probabilistic systems, however, require multi-terminal diagrams storing rational numbers. They are inefficient for models with many distinct probabilities and for iterative numeric algorithms like value iteration. In this paper, we present a new "symblicit" approach to checking Markov chains and related probabilistic models: We first generate a decision diagram that symbolically collects all reachable states and their predecessors. We then concretise states one-by-one into an explicit partial state space representation. Whenever all predecessors of a state have been concretised, we eliminate it from the explicit state space in a way that preserves all relevant probabilities and rewards. We thus keep few explicit states in memory at any time. Experiments show that very large models can be model-checked in this way with very low memory consumption.
