<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>8251</REFNUM><AUTHORS><AUTHOR>Donaldson,A.F.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>Symmetry reduction for probabilistic model checking</TITLE><PLACE_PUBLISHED>Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06). Lecture Notes in Computing Science volume 4218.</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>9-23</PAGES><LABEL>Donaldson:2006:8251</LABEL><KEYWORDS><KEYWORD>Probabilistic model checking</KEYWORD></KEYWORDS<ABSTRACT>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.</ABSTRACT><NOTES>To appear</NOTES></RECORD></RECORDS></XML>