Incremental Bisimulation Abstraction Refinement
|Title||Incremental Bisimulation Abstraction Refinement|
|Publication Type||Journal Article|
|Year of Publication||2014|
|Authors||Song L., Zhang L., Hermanns H., Godesken J.C|
|Journal||ACM Transactions on Embedded Computing Systems (TECS)|
|Pagination||Artcle No. 142|
Abstraction refinement techniques in probabilistic model checking are prominent approaches for 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 article proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence 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.