Incremental Bisimulation Abstraction Refinement

Jens Christian Godskesen, Lei Song, Lijun Zhang

    Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

    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 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 languageEnglish
    JournalProceedings of the International Conference on Application of Concurrency to System Design
    Pages (from-to)11-20
    ISSN1550-4808
    DOIs
    Publication statusPublished - 8 Jul 2013
    Event13th International Conference on Application of Concurrency to System Design: http://acsd.lsi.upc.edu/ - Barcelona, Spain
    Duration: 8 Jul 201310 Jul 2013
    http://acsd.lsi.upc.edu/

    Conference

    Conference13th International Conference on Application of Concurrency to System Design
    Country/TerritorySpain
    CityBarcelona
    Period08/07/201310/07/2013
    Internet address

    Fingerprint

    Dive into the research topics of 'Incremental Bisimulation Abstraction Refinement'. Together they form a unique fingerprint.

    Cite this