Probabilistic Bisimulation for Realistic Schedulers

Christian Eisentraut, Jens Christian Godskesen, Holger Hermanns, Lei Song, Lijun Zhang

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

    Abstrakt

    Weak distribution bisimilarity is an equivalence notion on probabilistic automata, originally proposed for Markov automata. It has gained some popularity as the coarsest behavioral equivalence enjoying valuable properties like preservation of trace distribution equivalence and compositionality. This holds in the classical context of arbitrary schedulers, but it has been argued that this class of schedulers is unrealistically powerful. This paper studies a strictly coarser notion of bisimilarity, which still enjoys these properties in the context of realistic subclasses of schedulers: Trace distribution equivalence is implied for partial information schedulers, and compositionality is preserved by distributed schedulers. The intersection of the two scheduler classes thus spans a coarser and still reasonable compositional theory of behavioral semantics.
    OriginalsprogEngelsk
    TitelFM 2015: Formal Methods : 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
    Vol/bind9109
    ForlagSpringer
    Publikationsdato2015
    Sider248-264
    ISBN (Trykt)978-3-319-19248-2
    ISBN (Elektronisk)978-3-319-19249-9
    DOI
    StatusUdgivet - 2015
    BegivenhedThe 20th International Symposium on Formal Methods - University of Oslo, Oslo, Norge
    Varighed: 22 jun. 201526 jun. 2015
    Konferencens nummer: 20
    http://fm2015.ifi.uio.no/

    Konference

    KonferenceThe 20th International Symposium on Formal Methods
    Nummer20
    LokationUniversity of Oslo
    Land/OmrådeNorge
    ByOslo
    Periode22/06/201526/06/2015
    Internetadresse
    NavnLecture Notes in Computer Science
    ISSN0302-9743

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Probabilistic Bisimulation for Realistic Schedulers'. Sammen danner de et unikt fingeraftryk.

    Citationsformater