A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice - (Extended Abstract).

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

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)

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 τ -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
Subtitle of host publicationEssays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
EditorsM.S. Alvim, K. Chatzikokolakis, C. Olarte, F. 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
Volume11760 LNCS
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 - (Extended Abstract).'. Together they form a unique fingerprint.

Cite this