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

Axiomatization
Branching
Concretes
Completeness
Equational Theory
Recursion
Fragment
Calculus
Language

Cite this

van Glabbeek, R. J., Groote, J. F., & de Vink, E. P. (2019). A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice: (extended abstract). In M. S. Alvim, K. Chatzikokolakis, C. Olarte, & F. Valencia (Eds.), The 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 (pp. 139-162). (Lecture Notes in Computer Science; Vol. 11760 LNCS). Cham: Springer. https://doi.org/10.1007/978-3-030-31175-9_9
van Glabbeek, Rob J. ; Groote, Jan Friso ; de Vink, Erik P. / A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice : (extended abstract). The 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. editor / M.S. Alvim ; K. Chatzikokolakis ; C. Olarte ; F. Valencia. Cham : Springer, 2019. pp. 139-162 (Lecture Notes in Computer Science).
@inbook{7a9726a4b6e040d188f70e0e7541fbd4,
title = "A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice: (extended abstract)",
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.",
author = "{van Glabbeek}, {Rob J.} and Groote, {Jan Friso} and {de Vink}, {Erik P.}",
year = "2019",
month = "11",
day = "4",
doi = "10.1007/978-3-030-31175-9_9",
language = "English",
isbn = "978-3-030-31174-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "139--162",
editor = "M.S. Alvim and K. Chatzikokolakis and C. Olarte and F. Valencia",
booktitle = "The 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",
address = "Germany",

}

van Glabbeek, RJ, Groote, JF & de Vink, EP 2019, A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice: (extended abstract). in MS Alvim, K Chatzikokolakis, C Olarte & F Valencia (eds), The 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. Lecture Notes in Computer Science, vol. 11760 LNCS, Springer, Cham, pp. 139-162. https://doi.org/10.1007/978-3-030-31175-9_9

A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice : (extended abstract). / van Glabbeek, Rob J.; Groote, Jan Friso; de Vink, Erik P.

The 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. ed. / M.S. Alvim; K. Chatzikokolakis; C. Olarte; F. Valencia. Cham : Springer, 2019. p. 139-162 (Lecture Notes in Computer Science; Vol. 11760 LNCS).

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

TY - CHAP

T1 - A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice

T2 - (extended abstract)

AU - van Glabbeek, Rob J.

AU - Groote, Jan Friso

AU - de Vink, Erik P.

PY - 2019/11/4

Y1 - 2019/11/4

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85075050692&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-31175-9_9

DO - 10.1007/978-3-030-31175-9_9

M3 - Chapter

AN - SCOPUS:85075050692

SN - 978-3-030-31174-2

T3 - Lecture Notes in Computer Science

SP - 139

EP - 162

BT - The 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

A2 - Alvim, M.S.

A2 - Chatzikokolakis, K.

A2 - Olarte, C.

A2 - Valencia, F.

PB - Springer

CY - Cham

ER -

van Glabbeek RJ, Groote JF, de Vink EP. A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice: (extended abstract). In Alvim MS, Chatzikokolakis K, Olarte C, Valencia F, editors, The 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. Cham: Springer. 2019. p. 139-162. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-31175-9_9