Incremental bisimulation abstraction refinement

Lei Song, Lijun Zhang, H. Hermanns, Jens Chr. Godskesen

    Research output: Contribution to journalArticleAcademic

    1 Citation (Scopus)


    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.
    Original languageUndefined
    Pages (from-to)Artcle No. 142
    JournalACM transactions on embedded computing systems
    Issue number4s
    Publication statusPublished - Jul 2014


    • IR-101792
    • EWI-27333
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490
    • EC Grant Agreement nr.: FP7/318003

    Cite this