[DMP09]
Alastair Donaldson, Alice Miller and David Parker.
Language-level Symmetry Reduction for Probabilistic Model Checking.
In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), pages 289-298, IEEE Computer Society.
September 2009.
[pdf]
[bib]
[Presents symmetry reduction techniques based on translation of PRISM models.]
|
Notes:
A full version of this paper, with proofs, is
available.
|
Links:
[Google]
[Google Scholar]
|
Abstract.
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.
|