zbMATH — the first resource for mathematics

Replication vs. recursive definitions in channel based calculi. (English) Zbl 1039.68082
Baeten, Jos C. M. (ed.) et al., Automata, languages and programming. 30th international colloquium, ICALP 2003, Eindhoven, The Netherland, June 30 – July 4, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40493-7/pbk). Lect. Notes Comput. Sci. 2719, 133-144 (2003).
Summary: We investigate the expressive power of two alternative approaches used to express infinite behaviours in process calculi, namely, replication and recursive definitions. These two approaches are equivalent in the full \(\pi\)-calculus, while there is a common agreement that this is not the case when name mobility is not allowed (as in the case of CCS), even if no formal discriminating results have been proved so far. We consider a hierarchy of calculi, previously proposed by Sangiorgi, that spans from a fragment of CCS (named “the core of CCS”) to the \(\pi\)-calculus with internal mobility. We prove the following discrimination result between replication and recursive definitions: the termination of processes is an undecidable property in the core of CCS, provided that recursive process definitions are allowed, while termination turns out to be decidable when only replication is permitted. On the other hand, this discrimination result does not hold any longer when we move to the next calculus in the hierarchy, which supports a very limited form of name mobility.
For the entire collection see [Zbl 1029.00041].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: Link