Language-Level Symmetry Reduction for Probabilistic Model Checking
Language-Level Symmetry Reduction for Probabilistic Model Checking
复制标题
DOI：
10.1109/qest.2009.21
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
Alastair F. Donaldson;Alice Miller;D. Parker
中科院分区：
文献类型：
--
作者：
Alastair F. Donaldson;Alice Miller;D. Parker
对称性约简是模型检验中对抗状态空间爆炸的一种技术。对称约简的通用代表方法使用了将对称模型转换为简化形式的语言级转换，使得它可以直接与现有工具和实现相结合。这些技术已经被提出用于非概率和概率模型检验，但由于建模语言中的令人望而却步的限制，目前难以应用于复杂模型。我们提出了一种更丰富的语言，它允许以一种保证通用代表技术的适用性的方式来规范概率系统，并结合扩展的翻译算法，并在大量的案例研究中展示了我们的技术的有效性。
Symmetry reduction is a technique for combatingstate-space explosion in model checking. The generic representatives approach to symmetry reduction uses a language-level translation of symmetric models to a reduced form, making it straightforward to combine with existing tools and implementations. These techniques have been proposed for both non-probabilistic and probabilistic model checking, but are currently difficult to apply to complex models due to prohibitive restrictions in the modelling language. We present a much richer language, which allows specification of probabilistic systems in a way that guarantees the applicability of the generic representatives technique, together with an extended translation algorithm, and demonstrate the effectiveness of our techniques on a large set of case studies.