Sciweavers

ATVA
2006
Springer

Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives

13 years 7 months ago
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
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.
Alastair F. Donaldson, Alice Miller
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Alastair F. Donaldson, Alice Miller
Comments (0)