On the Axiomatisability of Parallel Composition

TL;DR

This paper investigates the possibility of finite axiomatizations for parallel composition in process algebra, providing positive results for some semantics and negative results for others, highlighting the limits of axiomatizability.

Contribution

It offers the first finite, ground-complete axiomatisations for certain semantics in BCCSP and proves the non-existence of such axiomatizations for others, including bisimilarity.

Findings

Finite, ground-complete axiomatisations for some semantics

No finite axiomatization exists for bisimilarity and related semantics

Negative results apply to nested trace and simulation semantics

Abstract

This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. We also show that no congruence over BCCSP that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation; this negative result applies to all the nested trace and nested simulation semantics.