Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song, Lijun Zhang, Jens Christian Godskesen

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

    Abstrakt

    Probabilistic automata (PA) have beensuccessfully applied in the formal verification of concurrent andstochastic systems. Efficient model checking algorithms have beenstudied, where the most often used logics for expressing propertiesare based on PCTL and its extensionPCTL*. Variousbehavioral equivalences are proposed for PAs, asa powerful tool for abstraction and compositional minimization forPAs. Unfortunately, the behavioral equivalencesare well-known to be strictly stronger than the logical equivalences inducedby PCTL or PCTL*. This paper introduces novel notions of strongbisimulation relations, which characterizes PCTL and PCTL*exactly. We also extend weak bisimulations characterizingPCTL and PCTL* without next operator, respectively. Thus, ourpaper bridges the gap between logical and behavioral equivalences inthis setting.

    OriginalsprogEngelsk
    TitelCONCUR'11 Proceedings of the 22nd international conference on Concurrency theory
    Antal sider15
    ForlagSpringer
    Publikationsdato5 sep. 2011
    Sider108-123
    ISBN (Trykt)978-3-642-23216-9
    DOI
    StatusUdgivet - 5 sep. 2011
    Begivenhed22nd International Conference on Concurrency Theory 2011 (CONCUR 2011) - Aachen, Tyskland
    Varighed: 5 sep. 201110 sep. 2011
    Konferencens nummer: 22nd
    http://concur2011.rwth-aachen.de/

    Konference

    Konference22nd International Conference on Concurrency Theory 2011 (CONCUR 2011)
    Nummer22nd
    Land/OmrådeTyskland
    ByAachen
    Periode05/09/201110/09/2011
    Internetadresse

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Bisimulations Meet PCTL Equivalences for Probabilistic Automata'. Sammen danner de et unikt fingeraftryk.

    Citationsformater