Skip to Main content Skip to Navigation
Conference papers

Symbolic Bisimulation for Probabilistic Systems

Peng Wu 1 Catuscia Palamidessi 1 Huimin Lin 2
1 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 sug- gests a solution to the open problem on the axiomati- zation for weak bisimulation in the case of unguarded recursion. Furthermore, we present an efficient char- acterization of symbolic bisimulations for the calculus, which allows the ”on-the-fly” instantiation of bound names and dynamic construction of equivalence rela- tions for quantitative evaluation. This directly results in a local decision algorithm that can explore just a minimal portion of the state spaces of probabilistic pro- cesses in question.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/inria-00201068
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, December 23, 2007 - 12:58:19 AM
Last modification on : Thursday, March 5, 2020 - 6:18:30 PM
Long-term archiving on: : Tuesday, April 13, 2010 - 3:21:38 PM

File

qest2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Peng Wu, Catuscia Palamidessi, Huimin Lin. Symbolic Bisimulation for Probabilistic Systems. 4th International Conference on the Quantitative Evaluation of SysTems (QEST), Sep 2007, Edinburgh, United Kingdom. pp.179-188, ⟨10.1109/QEST.2007.46⟩. ⟨inria-00201068⟩

Share

Metrics

Record views

344

Files downloads

190