On the existence and decidability of unique decompositions of processes in the applied π-calculus

Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2] and [3]), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied π-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P   can be decomposed uniquely into prime factors PiPi with respect to strong labeled bisimilarity, i.e. such that P∼lP1|…|PnP∼lP1|…|Pn. Moreover, we prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. We also investigate whether efficient algorithms that compute the unique decompositions exist. The simpler problem of deciding whether a process is in its unique decomposition form is undecidable in general in both cases, due to potentially undecidable equational theories. Moreover, we show that the unique decomposition remains undecidable even given an equational theory with a decidable word problem.