Bisimulation Meet PCTL Equivalences for Probabilistic Automata (Journal Version)

Lei Song, Lijun Zhang, Jens Christian Godskesen

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

    Abstract

    Probabilistic automata (PA) have been successfully applied in the formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on PCTL and its extension PCTL*. Various behavioral equivalences are proposed for PAs, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the behavioral equivalences are well-known to be strictly stronger than the logical equivalences induced by PCTL or PCTL*. This paper introduces novel notions of strong bisimulation relations, which characterizes PCTL and PCTL* exactly. We also extend weak bisimulations characterizing PCTL and PCTL* without next operator, respectively. Thus, our paper bridges the gap between logical and behavioral equivalences in this setting.
    Original languageEnglish
    JournalLogical Methods in Computer Science
    Volume9
    Issue number2
    Number of pages34
    ISSN1860-5974
    Publication statusPublished - 2013

    Keywords

    • PCTL
    • Probabilistic Automata
    • Bisimulation
    • Logic Characterization

    Fingerprint

    Dive into the research topics of 'Bisimulation Meet PCTL Equivalences for Probabilistic Automata (Journal Version)'. Together they form a unique fingerprint.

    Cite this