Unique Parallel Decomposition in Branching and Weak Bisimulation Semantics

TL;DR

This paper investigates the conditions under which processes can be uniquely decomposed into parallel components within the framework of branching and weak bisimulation, revealing that boundedness ensures uniqueness.

Contribution

It establishes conditions for unique parallel decomposition in weak bisimulation semantics, including boundedness criteria and a general theorem for partial commutative monoids.

Findings

Infinite behaviors may lack parallel decompositions.

Totally normed behaviors have decompositions, but not necessarily unique.

Weakly bounded behaviors have guaranteed unique decompositions.

Abstract

We consider the property of unique parallel decomposition modulo branching and weak bisimilarity. First, we show that infinite behaviours may fail to have parallel decompositions at all. Then, we prove that totally normed behaviours always have parallel decompositions, but that these are not necessarily unique. Finally, we establish that weakly bounded behaviours have unique parallel decompositions. We derive the latter result from a general theorem about unique decompositions in partial commutative monoids.