Skip to main content
SpringerLink
Log in

Spatial and Behavioral Types in the Pi-Calculus

  • Conference paper
CONCUR 2008 - Concurrency Theory (CONCUR 2008)

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

Included in the following conference series:

Abstract

We present a framework that combines ideas from spatial logics and Igarashi and Kobayashi’s behavioural type systems, drawing benefits from both. In our approach, type systems for the pi-calculus are introduced where newly declared (restricted) names are annotated with spatial process properties, predicating on those names, that are expected to hold in the scope of the declaration. Types are akin to ccs terms and account for the processes abstract behaviour and “shallow” spatial structure. The type systems relies on spatial model checking, but properties are checked against types rather than against processes. The considered class of properties is rather general and, differently from previous proposals, includes both safety and liveness ones, and is not limited to invariants.

Research partly supported by the EU within the FET-GC2 initiative, project Sensoria.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Acciai, L., Boreale, M.: A type system for client progress in a service-oriented calculus. In: Degano, P., et al. (eds.) Montanari Festschrift. LNCS, vol. 5065, pp. 642–658. Springer, Heidelberg (2008)

    Google Scholar 

  2. Acciai, L., Boreale, M.: Type abstractions of name-passing processes. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 302–317. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Acciai, L., Boreale, M.: Responsiveness in process calculi. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 136–150. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Caires, L.: Logical Semantics of Types for Concurrency. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 16–35. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Caires, L.: Spatial-Behavioral Types, Distributed Services, and Resources. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 98–115. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Caires, L.: Behavioral and Spatial Observations in a Logic for the pi-Calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 72–89. Springer, Heidelberg (2004)

    Google Scholar 

  7. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194–235 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  8. Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: POPL 2002, pp. 45–57 (2002)

    Google Scholar 

  9. Cardelli, L., Gordon, A.D.: Anytime, Anywhere: Modal Logics for Mobile Ambients. In: POPL 2000, pp. 365–377 (2000)

    Google Scholar 

  10. Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. Theor. Comput. Sci. 311(1-3), 121–163 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  11. Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4-5), 291–347 (2005)

    Article  MATH  Google Scholar 

  12. Kobayashi, N., Suenaga, K., Wischik, L.: Resource Usage Analysis for the pi-Calculus. Logical Methods in Computer Science 2(3) (2006)

    Google Scholar 

  13. Kobayashi, N., Suto, T.: Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the pi -Calculus. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 740–751. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Milner, R.: The polyadic π-calculus: a tutorial. In: Logic and Algebra of Specification, pp. 203–246. Springer, Heidelberg (1993)

    Google Scholar 

  15. Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  16. Sangiorgi, D.: The Name Discipline of Uniform Receptiveness. Theoretical Computer Science 221(1-2), 457–493 (1999)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Sistemi e Informatica, Università di Firenze,  

    Lucia Acciai & Michele Boreale

Authors
  1. Lucia Acciai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michele Boreale
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Franck van Breugel Marsha Chechik

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Acciai, L., Boreale, M. (2008). Spatial and Behavioral Types in the Pi-Calculus . In: van Breugel, F., Chechik, M. (eds) CONCUR 2008 - Concurrency Theory. CONCUR 2008. Lecture Notes in Computer Science, vol 5201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85361-9_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85361-9_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85360-2

  • Online ISBN: 978-3-540-85361-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation