Incremental Bisimulation Abstraction Refinement

TitleIncremental Bisimulation Abstraction Refinement
Publication TypeJournal Article
Year of Publication2014
AuthorsSong L., Zhang L., Hermanns H., Godesken J.C
JournalACM Transactions on Embedded Computing Systems (TECS)
PaginationArtcle No. 142
Date PublishedJuly

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.