A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice

Rob J. van Glabbeek, Jan Friso Groote, Erik P. de Vink

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

Abstract

This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabilistic bisimilarity, an equational theory is proposed for a basic, recursion-free process language with non-deterministic as well as probabilistic choice. The proof of completeness of the axiomatization builds on the completeness of strong probabilistic bisimilarity on the one hand and on the notion of a concrete process, i.e. a process that does not display (partially) inert backslashtau -moves, on the other hand. The approach is first presented for the non-deterministic fragment of the calculus and next generalized to incorporate probabilistic choice, too.
Original languageEnglish
Title of host publicationThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
EditorsMário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, Frank Valencia
Place of PublicationCham
PublisherSpringer
Pages139-162
Number of pages24
ISBN (Electronic)978-3-030-31175-9
ISBN (Print)978-3-030-31174-2
DOIs
Publication statusPublished - 4 Nov 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
Volume11760
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice'. Together they form a unique fingerprint.

Cite this