[BogdollHZ08] An Experimental Evaluation of Probabilistic Simulation Bogdoll, J.; Hermanns, H. and Zhang, L. In Formal Techniques for Networked and Distributed Systems (FORTE), pages 37-52, Springer, Lecture Notes in Computer Science 5048, 2008.
Downloads: pdf, bibURL: Abstract. Probabilistic model checking has emerged as a versatile system verification approach, but is frequently facing state-space explosion problems. One promising attack to this is to construct an abstract model which simulates the original model, and to perform model checking on that abstract model. Recently, efficient algorithms for deciding simulation of probabilistic models have been proposed. They reduce the theoretical complexity bounds drastically by exploiting parametric maximum flow algorithms. In this paper, we report on experimental comparisons of these algorithms, together with various interesting optimizations. The evaluation is carried out on both standard PRISM example cases as well as randomly generated models. The results show interesting time-space tradeoffs, with the parametric maximum flow algorithms being superior for large, dense models.