On the Expressiveness and Decidability of Higher-Order Process Calculi

Abstract : In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky machines, the calculus is shown to be Turing complete and therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.
Type de document :
Communication dans un congrès
23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), Jun 2008, Pittsburgh, Pennsylvania, United States. pp.145--155, 2008, Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008). 〈10.1109/LICS.2008.8〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00494584
Contributeur : Alan Schmitt <>
Soumis le : mercredi 23 juin 2010 - 15:57:40
Dernière modification le : vendredi 12 octobre 2018 - 01:18:06
Document(s) archivé(s) le : lundi 22 octobre 2012 - 14:36:04

Fichier

Lanese2008On-the-Expressivenes...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Ivan Lanese, Jorge Peréz, Davide Sangiorgi, Alan Schmitt. On the Expressiveness and Decidability of Higher-Order Process Calculi. 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), Jun 2008, Pittsburgh, Pennsylvania, United States. pp.145--155, 2008, Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008). 〈10.1109/LICS.2008.8〉. 〈inria-00494584〉

Partager

Métriques

Consultations de la notice

258

Téléchargements de fichiers

155