Cinzia Di Giusto (INRIA Grenoble)

On the expressiveness of higher order communication

Abstract:

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. Finally we present an hierarchy of languages to discuss how the presence/absence of higher order capabilities and passivation affects the expressive power of a language.