Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2011: CONCUR 2011 – Concurrency Theory pp 373–388Cite as

The Decidability of the Reachability Problem for CCS!

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6901))

Abstract

CCS! is a variant of CCS in which infinite behaviors are defined by the replication operator. We show that the reachability problem for CCS! is decidable by a reduction to the same problem for Petri Nets.

The work is supported by NSFC (60873034, 61033002).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Acciai, L., Boreale, M.: Spatial and behavioral types in the pi-calculus. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 372–386. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Acciai, L., Boreale, M.: Deciding safety properties in infinite-state pi-calculus via behavioural types. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 31–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Aranda, J., Di Giusto, C., 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)

    Chapter  Google Scholar 

  4. Aranda, J., Valencia, F.D., Versari, C.: On the expressive power of restriction and priorities in CCS with replication. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 242–256. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. Busi, N., Gabbrielli, M., Zavattaro, G.: On the expressive power of recursion, replication and iteration in process calculi. Mathematical Structures in Computer Science 19(6), 1191–1222 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  8. Busi, N., Gorrieri, R.: Distributed conflicts in communicating systems. In: Pareschi, R. (ed.) ECOOP 1994. LNCS, vol. 821, pp. 49–65. Springer, Heidelberg (1994)

    Google Scholar 

  9. Fu, Y.: Theory of interaction (2011), Submitted and downloadable at http://basics.sjtu.edu.cn/~yuxi/

  10. Fu, Y., Lu, H.: On the expressiveness of interaction. Theor. Comput. Sci. 411(11-13), 1387–1451 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  11. 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)

    Google Scholar 

  12. Goltz, U.: CCS and petri nets. In: Semantics of Systems of Concurrent Processes, pp. 334–357 (1990)

    Google Scholar 

  13. He, C.: The decidability of the reachability problem for CCS! (2011), Downloadable at http://basics.sjtu.edu.cn/~chaodong/

  14. He, C., Fu, Y., Fu, H.: Decidability of behavioral equivalences in process calculi with name scoping. In: FSEN (2011)

    Google Scholar 

  15. Jancar, P., Moller, F.: Checking regular properties of petri nets. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 348–362. Springer, Heidelberg (1995)

    Google Scholar 

  16. Křetínský, M., Řehák, V., Strejček, J.: Extended process rewrite systems: Expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 355–370. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Křetínský, M., Řehák, V., Strejček, J.: Reachability of hennessy-milner properties for weakly extended PRS. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 213–224. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Mayr, E.W.: An algorithm for the general petri net reachability problem. In: STOC, pp. 238–246 (1981)

    Google Scholar 

  19. Mayr, R.: Process rewrite systems. Inf. Comput. 156(1-2), 264–286 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  20. Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  21. Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press, Cambridge (1999)

    Google Scholar 

  22. Park, D.M.R.: Concurrency and automata on infinite sequences. Theoretical Computer Science, 167–183 (1981)

    Google Scholar 

  23. Taubner, D.: Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS, vol. 369. Springer, Heidelberg (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BASICS, Department of Computer Science, MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems, Shanghai Jiao Tong University, Shanghai, 200240, China

    Chaodong He

Authors
  1. Chaodong He
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Software Modeling and Verification, RWTH Aachen, Ahornstraße 55, 52074, Aachen, Germany

    Joost-Pieter Katoen

  2. Fakultät für Ingenieurwesen, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen,, Lotharstraße 65, 47057, Duisburg, Germany

    Barbara König

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

He, C. (2011). The Decidability of the Reachability Problem for CCS! . In: Katoen, JP., König, B. (eds) CONCUR 2011 – Concurrency Theory. CONCUR 2011. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23217-6_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-23217-6_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-23216-9

  • Online ISBN: 978-3-642-23217-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation