Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech
On Unique Decomposition of Processes in the Applied Pi Calculus (2012)
On Unique Decomposition of Processes in the Applied Pi Calculus (2012)
TR-2012-3.pdf
Keywords: Applied Pi Calculus, Unique Decomposition, Factorization, Prime Process, Weak Labeled Bisimilarity, Strong Labeled Bisimilarity, Cancellation
Abstract: Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP or CCS), as it provides a normal form with useful cancellation properties. We provide two parallel decomposition results for subsets of the Applied Pi-Calculus: We show that a closed finite process P can be decomposed uniquely into prime factors P_i with respect to weak labeled bisimilarity, i.e. such that P = P_1 | ... | P_n. We also prove that closed normed processes (i.e. processes with a finite shortest trace) can be decomposed uniquely with respect to strong labeled bisimilarity.
