Under consideration for publication in Math. Struct. in Comp. Science On the expressive power of recursion, replication and iteration in process calculi

We investigate the expressive power of three alternative approaches for the definition of infinite behaviors in process calculi, namely, recursive definitions, replication and iteration. We prove several discrimination results between the calculi obtained from a core CCS by adding the three mechanisms mentioned above. These results are obtained by considering the decidability of four basic properties: termination (i.e. all computations are finite), convergence (i.e. the existence of a finite computation), barb (i.e. the ability of performing a synchronization) and weak bisimulation. Our results, summarized in Table 1, show that the three calculi form a strict expressiveness hierarchy, since all the mentioned properties are undecidable in CCS with recursion, while termination and barb are decidable in CCS with replication and all the properties are decidable in CCS with iteration. As a corollary we obtain also a strict expressiveness hierarchy w.r.t. weak bisimulation, since there exist weak bisimulation preserving encodings of iteration in replication and of replication in recursion, whereas there exist no weak bisimulation preserving encoding in the other directions. 1