On the Expressiveness and Decidability of Higher-Order Process Calculi

Ivan Lanese 1, 2 Jorge Perez 3 Davide Sangiorgi 1, 4 Alan Schmitt 5
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
5 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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 deterministic encoding of Minsky machines, the calculus is shown to be Turing complete. Therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Furthermore, 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 :
Article dans une revue
Journal of Information and Computation, Elsevier, 2011, 209 (2), pp.29. 〈10.1016/j.ic.2010.10.001〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01112294
Contributeur : Alan Schmitt <>
Soumis le : lundi 2 février 2015 - 15:45:50
Dernière modification le : jeudi 15 novembre 2018 - 11:57:41
Document(s) archivé(s) le : mercredi 27 mai 2015 - 15:43:14

Fichier

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Ivan Lanese, Jorge Perez, Davide Sangiorgi, Alan Schmitt. On the Expressiveness and Decidability of Higher-Order Process Calculi. Journal of Information and Computation, Elsevier, 2011, 209 (2), pp.29. 〈10.1016/j.ic.2010.10.001〉. 〈hal-01112294〉

Partager

Métriques

Consultations de la notice

1494

Téléchargements de fichiers

110