On the Expressive Power of Restriction and Priorities in CCS with Replication

摘要

We study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS_! (CCS with replication instead of recursion) which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS_! which do not allow the use of an unbounded number of restrictions: CCS_!~(-!v) is the fragment of CCS_! not allowing restrictions under the scope of a replication. CCS_!~(-v) is the restriction-free fragment of CCS_!. The third variant is CCS_(!+pr)~(-!v) which extends CCS_!~(-!v) with Phillips' priority guards.rnWe show that the use of unboundedly many restrictions in CCS_! is necessary for obtaining Turing expressiveness in the sense of Busi et al [8]. We do this by showing that there is no encoding of RAMs into CCS_!~(-!v) which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS_! into CCS_!~(-!v) nor from CCS_!~(-!v) into CCS_!~(-v). As lemmata for the above results we prove that convergence is decidable for CCS_!~(-!v) and that language equivalence is decidable for CCS_!~(-!v). As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing an encoding of RAMs in CCS_(!+pr)~(-!v)