Symmetry reduction for probabilistic model checking using generic representatives. (English) Zbl 1161.68564

Graf, Susanne (ed.) et al., Automated technology for verification and analysis. 4th international symposium, ATVA 2006, Beijing, China, October 23–26, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-47237-7/pbk). Lecture Notes in Computer Science 4218, 9-23 (2006).
Summary: 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.
For the entire collection see [Zbl 1137.68008].


68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: DOI Link