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

摘要

Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2,3]), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied pi-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors Pi with respect to strong labeled bisimilarity, i.e. such that P similar to(l) P-1 vertical bar(center dot center dot center dot)vertical bar P-n. 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. (C) 2015 Elsevier B.V. All rights reserved.