Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
复制标题
使用通用代表进行概率模型检查的对称性约简
DOI：
10.1007/11901914_4
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Alice Miller
中科院分区：
文献类型：
--
作者：
Alastair F. Donaldson;Alice Miller
在非概率模型检验中，提出了一种将对称约简和符号表示有效地结合在一起的通用表示方法。这种方法包括将对称源程序转换为简化程序，在简化程序中，计数器通常用于表示原始模型的状态。原程序的对称性质也可以翻译，并直接在简化程序上进行检查。我们将此方法扩展到具有马尔可夫决策过程或离散时间马尔可夫链语义的概率系统，表示为mtbdd。我们实现了一个原型工具GRIP，它将对称的PRISM程序和PCTL属性转换为简化形式。然后，可以通过将PRISM应用于简化后的程序所对应的较小模型来推断原始程序的模型检查结果。我们对两个案例研究提出了令人鼓舞的实验结果。
Generic representatives have been proposed for the effective combination of symmetry reduction and symbolic representation with BDDs in non-probabilistic model checking. This approach involves the translation of a symmetric source program into a reduced program, in which counters are used to generically represent states of the original model. Symmetric properties of the original program can also be translated, and checked directly over the reduced program. We extend this approach to apply to probabilistic systems with Markov decision process or discrete time Markov chain semantics, represented as MTBDDs. We have implemented a prototype tool, GRIP, which converts a symmetric PRISM program and PCTL property into reduced form. Model checking results for the original program can then be inferred by applying PRISM, unchanged, to the smaller model underlying the reduced program. We present encouraging experimental results for two case studies.