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

Jannik Dreier 1 Cristian Ene 2 Pascal Lafourcade 3 Yassine Lakhnech 2
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
Abstract : 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 π-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors P i with respect to strong labeled bisimilarity, i.e. such that P ∼ l P_1 | ... | 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.
Type de document :
Article dans une revue
Journal of Theoretical Computer Science (TCS), Elsevier, 2015, <10.1016/j.tcs.2015.11.033>
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-01238097
Contributeur : Jannik Dreier <>
Soumis le : mardi 12 septembre 2017 - 13:35:05
Dernière modification le : jeudi 14 septembre 2017 - 01:03:28

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Citation

Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech. On the existence and decidability of unique decompositions of processes in the applied π-calculus. Journal of Theoretical Computer Science (TCS), Elsevier, 2015, <10.1016/j.tcs.2015.11.033>. <hal-01238097v2>

Partager

Métriques

Consultations de
la notice

43

Téléchargements du document

4