Skip to main content
SpringerLink
Log in

The Value-Passing Calculus

  • Chapter
Book cover Theories of Programming and Formal Methods

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

Abstract

A value-passing calculus is a process calculus in which the contents of communications are values chosen from some data domain, and the propositions appearing in the conditionals are formulas constructed from a logic. Previous studies treat the domain models, as well as the logic theories, as unspecified oracles. The open-ended approach leaves open some fundamental issues unanswered. The paper provides a more formal account of the value-passing calculi. The new treatment is self-contained in that the logic theory a value-passing calculus refers to is formally defined. A value-passing calculus consists of a complete first order theory with an operational model that makes use of the terms and the boolean expressions of the theory. A systematic investigation into the theory of the value-passing calculi is carried out. A particular value-passing calculus, \(\mathbb{VPC}\), is shown to be the least expressive among all Turing complete value-passing calculi.

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. Brookes, S., Hoare, C., Roscoe, A.: A theory of communicating sequential processes. Journal of ACM 31, 560–599 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  2. Brookes, S.: A Model of Communicating Sequential Processes. PhD thesis, Oxford University (1983)

    Google Scholar 

  3. Cutland, N.: Computability: An Introduction to Recursive Function Theory. Cambridge University Press (1980)

    Google Scholar 

  4. De Nicola, R., Mantanari, U., Vaandrager, F.: Back and forth bisimulations. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 152–165. Springer, Heidelberg (1990)

    Google Scholar 

  5. Fu, Y., Lu, H.: On the expressiveness of interaction. Theoretical Computer Science 411, 1387–1451 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  6. Fischer, M., Rabin, M.: Super-exponential complexity of presburger arithmetic. In: Karp, R. (ed.) Complexity of Computation, pp. 27–41. American Mathematical Society (1974)

    Google Scholar 

  7. Fu, Y.: Nondeterministic structure of computation (2012)

    Google Scholar 

  8. Fu, Y.: Theory of interaction (2012)

    Google Scholar 

  9. Fu, Y., Zhu, H.: The name-passing calculus (2011)

    Google Scholar 

  10. Gödel, K.: Über formal unentscheidbare sätze der principia mathematica und verwandter systeme. Monatshefte für Mathematik und verwandter Systeme I 38, 173–198 (1931)

    Article  MATH  Google Scholar 

  11. Hennessy, M.: A proof system for communicating processes with value-passing. Journal of Formal Aspects of Computer Science 3, 346–366 (1991)

    Article  MATH  Google Scholar 

  12. Hennessy, M., Ingólfsdóttir, A.: Communicating processes with value-passing and assignment. Journal of Formal Aspects of Computing 5, 432–466 (1993)

    Article  MATH  Google Scholar 

  13. Hennessy, M., Ingólfsdóttir, A.: A theory of communicating processes with value-passing. Information and Computation 107, 202–236 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  14. Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138, 353–369 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  15. Hennessy, M., Lin, H.: Proof systems for message passing process algebras. Formal Aspects of Computing 8, 379–407 (1996)

    Article  MATH  Google Scholar 

  16. Hennessy, M., Lin, H.: Unique fixpoint induction for message-passing process calculi. In: Proc. Computing: Australian Theory Symposium (CAT 1997), vol. 8, pp. 122–131 (1997)

    Google Scholar 

  17. Hennessy, M., Lin, H., Rathke, J.: Unique fixpoint induction for message-passing process calculi. Science of Computer Programming 41, 241–275 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  18. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of ACM 32, 137–161 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hoare, C.: Communicating sequential processes. Communications of ACM 21, 666–677 (1978)

    Article  MATH  Google Scholar 

  20. Hoare, C.: Communicating Sequential Processes. Prentice Hall (1985)

    Google Scholar 

  21. Ingólfsdóttir, A., Lin, H.: A symbolic approach to value-passing processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 427–478. North-Holland (2001)

    Google Scholar 

  22. Lohrey, M., D’Argenio, P.R., Hermanns, H.: Axiomatising divergence. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 585–596. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  23. Lohrey, M., D’Argenio, P., Hermanns, H.: Axiomatising divergence. Information and Computatio 203, 115–144 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  24. Lin, H.: A verification tool for value-passing processes. In: Proceedings of 13th International Symposium on Protocol Specification, Testing and Verification, IFIP Transactions (1993)

    Google Scholar 

  25. Lin, H.: Symbolic transition graphs with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  26. Lin, H.: “On-the-fly” instantiation of value-passing processes. In: Proc. FORTH/PSTV 1998 (1998)

    Google Scholar 

  27. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

    Google Scholar 

  28. Milner, R.: A complete axiomatization system for observational congruence of finite state behaviours. Information and Computation 81, 227–247 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  29. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation 100, 1–40 (Part I), 41–77 (Part II) (1992)

    Google Scholar 

  30. Oppen, D.: A \(2^{2^{2^{pn}}}\) upper bound on the complexity of presburger arithmetic. Journal of Computer and System Sciences 16, 323–332 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  31. Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous π-calculus. Mathematical Structures in Computer Science 13, 685–719 (2003)

    Article  Google Scholar 

  32. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  33. Presburger, M.: Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Warsaw Mathematics Congress, vol. 395, pp. 92–101 (1929)

    Google Scholar 

  34. Priese, L.: On the concept of simulation in asynchronous, concurrent systems. Progress in Cybernatics and Systems Research 7, 85–92 (1978)

    MathSciNet  Google Scholar 

  35. Parrow, J., Sangiorgi, D.: Algebraic theories for name-passing calculi. Information and Computation 120, 174–197 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  36. Rathke, J.: Symbolic Techniques for Value-Passing Calculi. PhD thesis, University of Sussex (1997)

    Google Scholar 

  37. Rathke, J.: Unique fixpoint induction for value-passing processes. In: Proc. LICS 1997. IEEE Press (1997)

    Google Scholar 

  38. Rogers, H.: Theory of Recursive Functions and Effective Computability. MIT Press (1987)

    Google Scholar 

  39. Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)

    Google Scholar 

  40. Sangiorgi, D.: From π-calculus to higher order π-calculus–and back. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.)TAPSOFT 1993. LNCS, vol. 668, pp. 151–166. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  41. Thomsen, B.: A calculus of higher order communicating systems. In: Proc. POPL 1989, pp. 143–154 (1989)

    Google Scholar 

  42. Thomsen, B.: Plain chocs — a second generation calculus for higher order processes. Acta Informatica 30, 1–59 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  43. Thomsen, B.: A theory of higher order communicating systems. Information and Computation 116, 38–57 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  44. van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. In: Information Processing 1989, pp. 613–618. North-Holland (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BASICS, Department of Computer Science, Shanghai Jiaotong University, China

    Yuxi Fu

  2. MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems, Shanghai Jiaotong University, China

    Yuxi Fu

Authors
  1. Yuxi Fu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, P.O. Box 3058, Macau, China

    Zhiming Liu

  2. Department of Computer Science, University of York, Deramore Lane, YO10 5GH, York, UK

    Jim Woodcock

  3. Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), 200062, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Fu, Y. (2013). The Value-Passing Calculus. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39698-4_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39697-7

  • Online ISBN: 978-3-642-39698-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation