On the Parallel Composition for True Concurrency

TL;DR

This paper investigates the axiomatization of parallel composition in true concurrency, establishing finite axiomatizations for some equivalences and proving limitations for others, advancing the theoretical understanding of process algebra.

Contribution

It provides the first finite axiomatizations of parallel composition modulo certain bisimulations and clarifies the limitations for others, using process algebra APTC.

Findings

Finite axiomatization for pomset, step, and hp-bisimulations without auxiliary operators.

No finite axiomatization for hhp-bisimulation without auxiliary operators.

Finite axiomatization for all considered bisimulations with auxiliary operators.

Abstract

For insight into the parallel composition for true concurrency, we recall the axiomatization of the parallel composition modulo truly concurrent behavioral equivalences as the sidelights of truly concurrent process algebra APTC. We prove that: (1) There is a finite sound and complete axiomatization of the parallel composition modulo pomset, step and hp-bisimulations, without any auxiliary operators. (2) There does not exist a finite sound and complete axiomatization of the parallel composition modulo hhp-bisimulation, without any auxiliary operator. (3) There is a finite sound and complete axiomatization of the parallel composition modulo pomset, step, hp-. and hhp-bisimulations, with the auxiliary left parallel composition and communication merge.