On unique decomposition of processes in the applied π-calculus

Abstract

Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [2] or CCS [11,13]), as it provides a normal form with useful cancellation properties. We provide two parallel decomposition results for subsets of the Applied π-Calculus: we show that any 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 ∼l P1|...|P n. We also prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. © 2013 Springer-Verlag.