Deciding bisimilarities on distributions

Christian Eisentraut, Holger Hermanns, Julia Krämer, Andrea Turrini, Lijun Zhang

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

Abstract

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 languageEnglish
Title of host publicationQuantitative Evaluation of Systems : 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings
PublisherSpringer
Publication date2013
Pages72-88
ISBN (Print)978-3-642-40195-4
ISBN (Electronic)978-3-642-40196-1
DOIs
Publication statusPublished - 2013
Event10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013
http://www.qest.org/qest2013/

Conference

Conference10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)
CountryArgentina
CityBuenos Aires
Period27/08/201330/08/2013
Internet address
SeriesLecture Notes in Computer Science
Volume8054
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Deciding bisimilarities on distributions'. Together they form a unique fingerprint.

Cite this