Symbolic bisimulations for probabilistic systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

The paper introduces symbolic bisimulations for a simple probabilistic π-calculus to overcome the infinite branching problem that still exists in checking ground bisimulations between probabilistic systems. Especially the definition of weak (symbolic) bisimulation does not rely on the random capability of adversaries and suggests a solution to the open problem on the axiomatization for weak bisimulation in the case of unguarded recursion. Furthermore, we present an efficient characterization of symbolic bisimulations for the calculus, which allows the "on-the-fly" instantiation of bound names and dynamic construction of equivalence relations for quantitative evaluation. This directly results in a local decision algorithm that can explore just a minimal portion of the state spaces of the probabilistic processes in question.

Original languageEnglish
Title of host publicationProceedings - 4th International Conference on the Quantitative Evaluation of Systems, QEST 2007
PublisherIEEE Computer Society
Pages179-188
Number of pages10
ISBN (Print)076952883X, 9780769528830
DOIs
Publication statusPublished - 1 Jan 2007
Externally publishedYes
Event4th International Conference on the Quantitative Evaluation of Systems, QEST 2007 - Edinburgh, United Kingdom
Duration: 17 Sept 200719 Sept 2007

Publication series

NameProceedings - 4th International Conference on the Quantitative Evaluation of Systems, QEST 2007

Conference

Conference4th International Conference on the Quantitative Evaluation of Systems, QEST 2007
Country/TerritoryUnited Kingdom
CityEdinburgh
Period17/09/0719/09/07

Fingerprint

Dive into the research topics of 'Symbolic bisimulations for probabilistic systems'. Together they form a unique fingerprint.

Cite this