2003 | OriginalPaper | Buchkapitel
Replication vs. Recursive Definitions in Channel Based Calculi
verfasst von : Nadia Busi, Maurizio Gabbrielli, Gianluigi Zavattaro
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 π-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 π-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.