On Unique Decomposition of Processes in the Applied π-CalculusReport as inadecuate

On Unique Decomposition of Processes in the Applied π-Calculus - Download this document for free, or read online. Document in PDF available to download.

1 CASSIS - Combination of approaches to the security of infinite states systems FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods 2 VERIMAG - IMAG - VERIMAG 3 LIMOS - Laboratoire d-Informatique, de Modélisation et d-optimisation des Systèmes

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 π-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|.

|Pn. We also prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity.

Keywords : Applied π-Calculus Unique Decomposition Normal Form Weak Bisimilarity Strong Bisimilarity Factorization Cancellation

Author: Jannik Dreier - Cristian Ene - Pascal Lafourcade - Yassine Lakhnech -

Source: https://hal.archives-ouvertes.fr/


Related documents