Advertisement

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

  • Jesús Aranda
  • Frank D. Valencia
  • Cristian Versari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

Abstract

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\(_{!}^{-!\nu}\) is the fragment of CCS! not allowing restrictions under the scope of a replication. CCS\(_{!}^{-\nu}\) is the restriction-free fragment of CCS!. The third variant is CCS\(_{!+pr}^{-!\nu}\) which extends CCS\(_{!}^{-!\nu}\) 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\(_{!}^{-!\nu}\) which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into CCS\(_{!}^{-!\nu}\) nor from CCS\(_{!}^{-!\nu}\) into CCS\(_{!}^{-\nu}.\) As lemmata for the above results we prove that convergence is decidable for CCS\(_{!}^{-!\nu}\) and that language equivalence is decidable for CCS\(_{!}^{-\nu}\). 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}^{-!\nu}\).

Keywords

Transition Relation Expressive Power Computable Function Parallel Composition Visible Action 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Amadio, R., Meyssonnier, C.: On decidability of the control reachability problem in the asynchronous π−calculus. Nordic Journal of Computing 9(2) (2002)Google Scholar
  2. 2.
    Aranda, J., Giusto, C.D., Nielsen, M., Valencia, F.D.: CCS with replication in the chomsky hierarchy: The expressive power of divergence. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 383–398. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Aranda, J., Valencia, F., Versari, C.: On the expressive power of restriction and priorities in ccs with replication. Technical report, l’École Polytechnique (2008), http://www.lix.polytechnique.fr/Labo/Jesus.Aranda/publications/trccs.pdf
  4. 4.
    Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation equivalence for processes generating context-free languages. J. ACM 40(3), 653–682 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Borger, E., Gradel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1994)zbMATHGoogle Scholar
  6. 6.
    Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31(3), 560–599 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Busi, N., Gabbrielli, M., Zavattaro, G.: Replication vs. recursive definitions in channel based calculi. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 133–144. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Busi, N., Gabbrielli, M., Zavattaro, G.: Comparing recursion, replication, and iteration in process calculi. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 307–319. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, Edinburgh University (1993)Google Scholar
  10. 10.
    Christensen, S., Hirshfeld, Y., Moller, F.: Decidable subsets of ccs. Comput. J. 37(4), 233–242 (1994)CrossRefGoogle Scholar
  11. 11.
    Esparza, J., Nielsen, M.: Decidability issues for petri nets. Technical report, BRICS RS-94-8 (1994)Google Scholar
  12. 12.
    Giambiagi, P., Schneider, G., Valencia, F.D.: On the expressiveness of infinite behavior and name scoping in process calculi. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 226–240. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Goltz, U.: Ccs and petri nets. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 334–357. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  14. 14.
    Hirshfeld, Y.: Petri nets and the equivalence problem. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, pp. 165–174. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  15. 15.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  16. 16.
    Minsky, M.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)zbMATHGoogle Scholar
  17. 17.
    Phillips, I.: Ccs with priority guards. J. Log. Algebr. Program. 75(1), 139–165 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Taubner, D.: Finite representation of CCS and TCSP programs by automata and Petri nets. In: Taubner, D.A. (ed.) Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS, vol. 369. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  19. 19.
    Versari, C., Busi, N., Gorrieri, R.: On the expressive power of global and local priority in process calculi. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 241–255. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Zavattaro, G., Cardelli, L.: Termination problems in chemical kinetics. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 477–491. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Jesús Aranda
    • 1
  • Frank D. Valencia
    • 2
  • Cristian Versari
    • 3
  1. 1.LIX École Polytechnique and Universidad del Valle ColombiaColombia
  2. 2.CNRS and LIX École PolytechniqueFrance
  3. 3.Università di BolognaItaly

Personalised recommendations