Incremental bisimulation abstraction refinement

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

    Research output: Contribution to journalArticleAcademic

    1 Citation (Scopus)

    Abstract

    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
    Volume13
    Issue number4s
    DOIs
    Publication statusPublished - Jul 2014

    Keywords

    • 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

    Song, L., Zhang, L., Hermanns, H., & Godskesen, J. C. (2014). Incremental bisimulation abstraction refinement. ACM transactions on embedded computing systems, 13(4s), Artcle No. 142. https://doi.org/10.1145/2627352