Language-Level Symmetry Reduction for Probabilistic Model Checking

—Symmetry reduction is a technique for combating state-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. Keywords-Symmetry reduction; probabilistic model checknter abstraction

• Type: Conference
• Year: 2009
• Where: QEST
• Authors: Alastair F. Donaldson, Alice Miller, David Parker
• Keywords: Generic Representatives, Model Checking, Probabilistic Model, QEST 2009, Quantitative Evaluation Of Systems