[SongZHG14] Incremental Bisimulation Abstraction Refinement Song, L.; Zhang, L.; Hermanns, H. and Godskesen, J. C. In Transactions on Embedded Computing Systems (TECS), 13: 142:1-142:23, 2014.
Downloads: pdf, bibURL: http://dx.doi.org/10.1109/ACSD.2013.5 Abstract. Abstraction refinement techniques in probabilistic model checking are prominent approaches to the verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This paper proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing asequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.