Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song, Lijun Zhang, Jens Chr. Godskesen

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    Probabilistic automata (PA) [20] 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 [11] and its extension PCTL∗ [4]. 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
    Title of host publicationCONCUR 2011 – Concurrency Theory : 22nd International Conference, CONCUR 2011 Aachen, Germany, September 6-9, 2011 Proceedings
    Volume6901
    PublisherSpringer
    Publication date2011
    Pages108-123
    ISBN (Print)978-3-642-23216-9
    ISBN (Electronic)978-3-642-23217-6
    DOIs
    Publication statusPublished - 2011
    Event22nd International Conference on Concurrency Theory - Aachen, Germany
    Duration: 5 Sept 201110 Sept 2011
    Conference number: 22
    http://concur2011.rwth-aachen.de/

    Conference

    Conference22nd International Conference on Concurrency Theory
    Number22
    Country/TerritoryGermany
    CityAachen
    Period05/09/201110/09/2011
    Internet address
    SeriesLecture Notes in Computer Science
    Number6901
    ISSN0302-9743

    Fingerprint

    Dive into the research topics of 'Bisimulations Meet PCTL Equivalences for Probabilistic Automata'. Together they form a unique fingerprint.

    Cite this