TY - GEN
T1 - On the expressive power of restriction and priorities in ccs with replication
AU - Aranda, Jesús
AU - Valencia, Frank D.
AU - Versari, Cristian
PY - 2009
Y1 - 2009
N2 - 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 is the fragment of CCS ! not allowing restrictions under the scope of a replication. CCS is the restriction-free fragment of CCS !. The third variant is CCS which extends CCS with Phillips' priority guards. We 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 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS ! into CCS nor from CCS into CCS As lemmata for the above results we prove that convergence is decidable for CCS and that language equivalence is decidable for CCS . 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 .
AB - 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 is the fragment of CCS ! not allowing restrictions under the scope of a replication. CCS is the restriction-free fragment of CCS !. The third variant is CCS which extends CCS with Phillips' priority guards. We 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 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS ! into CCS nor from CCS into CCS As lemmata for the above results we prove that convergence is decidable for CCS and that language equivalence is decidable for CCS . 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 .
UR - http://www.scopus.com/inward/record.url?scp=70349888079&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-00596-1_18
DO - 10.1007/978-3-642-00596-1_18
M3 - Conference contribution
AN - SCOPUS:70349888079
SN - 3642005950
SN - 9783642005954
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 242
EP - 256
BT - Foundations of Software Science and Computational Structures - 12th International Conference, FOSSACS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc.
T2 - 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
Y2 - 22 March 2009 through 29 March 2009
ER -