Hostname: page-component-6898cfcb55-th4rj Total loading time: 0 Render date: 2026-11-11T23:26:00.504Z Has data issue: false hasContentIssue false

On the expressive power of recursion, replication and iteration in process calculi

Published online by Cambridge University Press:  04 December 2009

NADIA BUSI
Affiliation:
Dip. di Scienze dell'Informazione, Univ. di Bologna, Mura A.Zamboni 7, 40127 Bologna, Italy Email: gabbri@cs.unibo.it; zavattar@cs.unibo.it
MAURIZIO GABBRIELLI
Affiliation:
Dip. di Scienze dell'Informazione, Univ. di Bologna, Mura A.Zamboni 7, 40127 Bologna, Italy Email: gabbri@cs.unibo.it; zavattar@cs.unibo.it
GIANLUIGI ZAVATTARO
Affiliation:
Dip. di Scienze dell'Informazione, Univ. di Bologna, Mura A.Zamboni 7, 40127 Bologna, Italy Email: gabbri@cs.unibo.it; zavattar@cs.unibo.it
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In this paper we investigate the expressive power of three alternative approaches to the definition of infinite behaviours in process calculi, namely, recursive definitions, replication and iteration. We prove several results discriminating between the calculi obtained from a core CCS by adding the three mechanisms mentioned above. These results are derived by considering the decidability of four basic properties: termination (that is, all computations are finite); convergence (that is, the existence of a finite computation); barb (that is, the ability to perform an action on a given channel) and weak bisimulation.

Our results, which are summarised in Table 1, show that the three calculi form a strict expressiveness hierarchy in that: all the properties mentioned are undecidable in CCS with recursion; only termination and barb are decidable in CCS with replication; all the properties are decidable in CCS with iteration.

As a corollary, we also obtain a strict expressiveness hierarchy with respect to weak bisimulation, since there exist weak bisimulation preserving encodings of iteration in replication and of replication in recursion, whereas there are no weak bisimulation preserving encodings in the other directions.

Information

Type
Paper
Copyright
Copyright © Cambridge University Press 2009