Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A modal logic for message passing processes

  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

A first-order modal logic is given for describing properties of processes which may send and receive values or messages along communication ports. We give two methods for proving that a process enjoys such a property. The first is the construction, for each processP and formulaF, of acharacteristic formula P satF such thatP enjoys the propertyF if and only if the formulaP satF is logically equivalent to tt. The second is a sound and complete proof system whose judgements take the formB ⊢P: F, meaning: under the assumptionB the processP enjoys the propertyF.

The notion ofsymbolic operational semantics plays a crucial role in the design of both the characteristic formulae and the proof system.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. R. Cleaveland, J. Parrow, B. Steffen: The concurrency workbench. University of Edinburgh, Scotland, 1988

    Google Scholar 

  2. J.C. Godskesen, K.G. Larsen, M. Zeeberg: Tav — tools for automatic verification — users manual. Technical Report R 89-19, Department of Matheamtics and Computer Science, Aalborg University, 1989. Presented at workshop on Automatic Methods for Finite State, Systems, Grenoble, France, Juni 1989

  3. S. Graf, J. Sifakis: A logic for the description of non-deterministic programs and their properties. Information and Control, 68 (1–3), 1986

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

    Google Scholar 

  5. M. Hennessy, H. Lin: Symbolic bisimulation. Technical Report Technical Report 1/92, School of Congnitive and Computing Sciences, University of Sussex, 1992

  6. M. Hennessy, X. Liu: A modal logic for message passing processes. Technical Report Technical Report 3/93, School of Congnitive and Computing Sciences, University of Sussex 1993

  7. A. Ingolfsdottir, B. Thomsen: Semantic models for ccs with values. Technical Report 63, Programming Methodology Group, Chalmers University of Technology, 1992. In Proceedings of the Workshop on Concurrency

  8. K.G. Larsen: Proof systems for Hennessy-Milner logic with recursion.Lecture Notes In Computer Science, Springer Verlag, 299, 1988. in Proceedings of 13th Colloquium on Trees in Algebra and Programming 1988

  9. H. Lin: A verification tool for value-passing processes. Technical report, School of Congnitive and Computing Sciences, University of Sussex, 1993. To appear

  10. R. Milner:Communication and Concurrency. Prentice-Hall, 1989

  11. R. Milner, J. Parrow, D. Walker: Modal logics for mobile processes.Theoretical Computer Science, 1992. To appear

  12. B. Steffen, A. Ingolfsdottir: Characteristic formulae for processes with divergence. Technical Report Technical Report 1/91, School of Congnitive and Computing Sciences, University of Sussex, 1991

  13. C. Stirling: Modal logics for communicating systems.Theoretical Computer Science, (311–347), 1987

Download references

Author information

Authors and Affiliations

  1. School of Cognitive and Computing Sciences, University of Sussex, BN1 9QH, Brighton, England

    M. Hennessy & X. Liu

Authors
  1. M. Hennessy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. X. Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This work was been supported by the SERC grant GR/H16537 and the ESPRIT BRA CONCUR II

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hennessy, M., Liu, X. A modal logic for message passing processes. Acta Informatica 32, 375–393 (1995). https://doi.org/10.1007/BF01178384

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01178384

Keywords

Search

Navigation