A complete axiomatization of weighted branching bisimulation

Research output: Contribution to journalJournal articleResearchpeer-review


We propose an axiomatization for weighted branching bisimulation over a weighted process algebra with positive rational weights including zero and show that this axiomatization is both sound and complete. Our proof of soundness and completeness are inspired by similar results by Milner for strong and weak bisimulation and by van Glabbeek for branching bisimulation. We also show that the claim that weighted branching bisimilarity is an equivalence relation indeed holds true. As auxiliary results, we give two alternative characterizations of weighted branching bisimulation, one in terms of weighted stuttering transitions and another in terms of a relative branching base which can be seen as a linear basis from which we can construct all weighted stuttering transitions.
Original languageEnglish
JournalActa Informatica
Pages (from-to)689-725
Number of pages37
Publication statusPublished - 1 Oct 2020

Fingerprint Dive into the research topics of 'A complete axiomatization of weighted branching bisimulation'. Together they form a unique fingerprint.

Cite this