Deciding bisimilarities on distributions

Christian Eisentraut, H. Hermanns, Julia Krämer, Andrea Turini, Lijun Zhang

    Research output: Contribution to conferencePaper

    16 Citations (Scopus)
    7 Downloads (Pure)


    Probabilistic automata (PA) are a prominent compositional concurrency model. As a way to justify property-preserving abstractions, in the last years, bisimulation relations over probability distributions have been proposed both in the strong and the weak setting. Different to the usual bisimulation relations, which are defined over states, an algorithmic treatment of these relations is inherently hard, as their carrier set is uncountable, even for finite PAs. The coarsest of these relation, weak distribution bisimulation, stands out from the others in that no equivalent state-based characterisation is known so far. This paper presents an equivalent state-based reformulation for weak distribution bisimulation, rendering it amenable for algorithmic treatment. Then, decision procedures for the probability distribution-based bisimulation relations are presented.
    Original languageUndefined
    Number of pages17
    Publication statusPublished - Aug 2013
    Event10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - University of Buenos Aires, Buenos Aires, Argentina
    Duration: 27 Aug 201330 Aug 2013
    Conference number: 10


    Conference10th International Conference on Quantitative Evaluation of Systems, QEST 2013
    Abbreviated titleQEST
    CityBuenos Aires
    Internet address


    • EC Grant Agreement nr.: FP7/318490
    • IR-101833
    • EC Grant Agreement nr.: FP7/295261
    • EC Grant Agreement nr.: FP7/318003
    • EWI-27349
    • EC Grant Agreement nr.: FP7/2007-2013

    Cite this