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

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 - Essays 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
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