Notes:
A full version of this paper, with proofs, is
available.
|
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.
|