Skip to main content
SpringerLink
Log in

Failures semantics for a simple process language with refinement

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 560))

Abstract

We study a suitable semantic theory based on the standard failures preorder [BHR84] for a simple process algebra which includes operators for the refinement of actions by processes. We present a model-theoretic and a behavioural characterization of the largest precongruence associated with failures preorder, ⫇ cF , over the language we consider.

The model-theoretic characterization is in terms of a pomset failures model which is shown to be fully abstract with respect to ⫇ cF . Pomset failures (labelled partial orders with refusal sets) allow us to express the nonsequential as well as the nondeterministic characteristics of ⫇ cF . The behavioural characterization is in terms of a variation on the standard failures preorder based on ideas of ST-semantics, [Gla90].

Supported by Esprit B.R.A. CEDISYS

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Luca Aceto and Uffe Henrik Engberg. Failures Semantics for a Simple Process Language with Refinement. To appear as INRIA Reseach Report, 1991.

    Google Scholar 

  2. Luca Aceto and Matthew Hennessy. Towards action-refinement in process algebras. In LICS' 89, Ann. Symp. on Logic in Computer Science, Pacific Grove, California, pages 138–145. IEEE, June 1989.

    Google Scholar 

  3. Steven D. Brookes, Charles Anthony Richard Hoare, and A.W. Roscoe. A Theory of Communicating Sequential Processes. Journal of the ACM, 31(3):560–599, 1984.

    Article  Google Scholar 

  4. Jan A. Bergstra and Jan W. Klop. Algebra of Communicating Processes with Abstraction. Journal of the ACM, 37(1):77–121, 1985.

    Google Scholar 

  5. Uffe Henrik Engberg. Partial Orders and Fully Abstract Models for Concurrency. PhD thesis, Computer Science Department, Aarhus University, 4. October 1989. Technical Teport DAIMI PB 307, 1990.

    Google Scholar 

  6. Uffe Henrik Engberg. True Concurrency Can Be Traced. Technical Report DAIMI PB-308, Department of Computer Science, Aarhus University, April 1990.

    Google Scholar 

  7. Rob van Glabbeek and Ursula Goltz. Equivalence Notions for Concurrent Systems and Refinement of Actions. In Proceedings 14th Symp. on Math. Foundations of Computer Science, pages 237–248. Springer-Verlag (LNCS, 379), 1988.

    Google Scholar 

  8. Jay Loren Gischer. The Equational Theory of Pomsets. Theoretical Computer Science, 61(2,3):199–224, 1988.

    Article  Google Scholar 

  9. Rob van Glabbeek. The Refinement Theorem for ST-bisimulation. To appear in Proc. IFIP Working Group, Sea of Galilee, 1990.

    Google Scholar 

  10. Jan Grabowski. On Partial Languages. Annales Societatis Mathematicae Polonae, IV(2):427–498, 1981.

    Google Scholar 

  11. Rob van Glabbeek and Fritz Vaandrager. Petri Net Models for Algebraic Theories of Concurrency. LNCS, 259:224–242, 1987.

    Google Scholar 

  12. Matthew Hennessy. Axiomatising Finite Concurrent Processes. SIAM Journal on Computing, 17(5):997–1017, 1988.

    Article  Google Scholar 

  13. Charles Anthony Richard Hoare. Communicating Sequential Processes. Series In Computer Science. Prentice-Hall, 1985.

    Google Scholar 

  14. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  15. Mogens Nielsen, Uffe Engberg, and Kirn Skak Laxsen. A Simple Process Language with Refinement. In REX School/ Workshop on Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency, Nordwijkerhout, The Netherlands, May/ June 1988, pages 523–548. Springer-Verlag (LNCS, 354), 1989.

    Google Scholar 

  16. Gordon D. Plotkin. A Structural Approach to Operational Semantics. Lecture Notes DAIMI FN-19, Department of Computer Science, Aarhus University, 1981.

    Google Scholar 

  17. Vaughan Pratt. Modeling Concurrency with Partial Orders. International Journal of Parallel Programming, 15(1):33–71, 1986.

    Article  Google Scholar 

  18. Walter Vogler. Failures Semantics Based on Interval Semiwords is a Congruence for Refinement. In STACS' 90, Symp. on Theoretical Aspects of Computer Science, Rouen, France, pages 285–297. Springer-Verlag (LNCS, 415), February 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Hewlett-Packard Laboratories, Pisa Science Center, Corso Italia 115, I-56125, Pisa, Italia

    Luca Aceto

  2. Computer Science Department, Aarhus University, Ny Munkegade, DK-8000, Aarhus C, Denmark

    Uffe Engberg

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uffe Engberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Somenath Biswas Kesav V. Nori

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aceto, L., Engberg, U. (1991). Failures semantics for a simple process language with refinement. In: Biswas, S., Nori, K.V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1991. Lecture Notes in Computer Science, vol 560. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54967-6_63

Download citation

  • DOI: https://doi.org/10.1007/3-540-54967-6_63

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54967-3

  • Online ISBN: 978-3-540-46612-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation