Higher-Order Concurrency: Expressiveness and Decidability Results

This page collects results on the expressiveness and decidability of HoCore (a core calculus for higher-order concurrency), and its extensions/specializations.
Comments and suggestions are most welcome!
Feel free to contact me: perezNOSPAM@cs.unibo.it (remove NOSPAM)

Higher-Order Concurrency: Expressiveness and Decidability Results (PhD Thesis)
Jorge A. Perez, University of Bologna, Italy
Download:
Draft (Submitted, January 19, 2010): [PDF].

On the Expressiveness of Polyadicity in Higher-Order Communication
Ivan Lanese, Jorge A. Perez, Davide Sangiorgi University of Bologna, Italy
Alan Schmitt INRIA Grenoble Rhone-Alpes, France

In higher-order process calculi the values exchanged in communications may contain processes. We describe a study of the expressive power of strictly higher-order pro- cess calculi, i.e. calculi in which only process passing is allowed and no name-passing is present. In this setting, the polyadicity (i.e. the number of parameters) allowed in commu- nications is shown to induce a hierarchy of calculi of strictly increasing expressiveness: a higher-order calculus with n-adic communication cannot be encoded into a calculus with n − 1-adic communication. In this note we outline this result, and discuss on how it relies on a notion of encoding that takes a rather fine standpoint with respect to internal behavior.
Download:
Extended Abstract (to appear in Proc. of ICTCS'09): [PDF].
Slides (soon to come)

On the Expressiveness of Forwarding in Higher-Order Communication
Cinzia Di Giusto, Jorge A. Perez, and Gianluigi Zavattaro University of Bologna, Italy

In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable. Then, as a way of recovering the expressiveness loss due to limited forwarding, we extend the calculus with a form of process suspension called passivation. Somewhat surprisingly, in the calculus extended with passivation both termination and convergence are undecidable.
Download:
Conference Version (in Proc. of ICTAC'09, pp. 155-169, volume 5684 of LNCS, Springer, 2009): [PDF]
Extended and Revised Version, with proofs (34pp) ---DRAFT, 06/12/2009---: [PDF]
Slides: [PDF]

On the Expressiveness and Decidability of Higher-Order Process Calculi
Ivan Lanese, Jorge A. Perez, Davide Sangiorgi University of Bologna, Italy
Alan Schmitt INRIA Grenoble Rhone-Alpes, France

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 andtherefore its termination problem is undecidable. Strong bisimilarity, however, is proved 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.
Download:
Conference Version (in Proc. of LICS'08, pp. 145--155, IEEE Computer Society, 2008.): [PDF]
Extended and Revised Version, with proofs ---DRAFT, 11/02/2009---: [PDF]
Slides (as presented in the COPLAS Seminar, August 12, 2008): [PDF]