Failures semantics for a simple process language with refinement

  • Luca Aceto
  • Uffe Engberg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 560)


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, ⫇ F c , 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 ⫇ F c . Pomset failures (labelled partial orders with refusal sets) allow us to express the nonsequential as well as the nondeterministic characteristics of ⫇ F c . The behavioural characterization is in terms of a variation on the standard failures preorder based on ideas of ST-semantics, [Gla90].


Operational Semantic Sequential Composition Label Process Denotational Semantic Refinement Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AE91]
    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. [AH89]
    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. [BHR84]
    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.CrossRefGoogle Scholar
  4. [BK85]
    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. [Eng89]
    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. [Eng90]
    Uffe Henrik Engberg. True Concurrency Can Be Traced. Technical Report DAIMI PB-308, Department of Computer Science, Aarhus University, April 1990.Google Scholar
  7. [GG88]
    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. [Gis88]
    Jay Loren Gischer. The Equational Theory of Pomsets. Theoretical Computer Science, 61(2,3):199–224, 1988.CrossRefGoogle Scholar
  9. [Gla90]
    Rob van Glabbeek. The Refinement Theorem for ST-bisimulation. To appear in Proc. IFIP Working Group, Sea of Galilee, 1990.Google Scholar
  10. [Gra81]
    Jan Grabowski. On Partial Languages. Annales Societatis Mathematicae Polonae, IV(2):427–498, 1981.Google Scholar
  11. [GV87]
    Rob van Glabbeek and Fritz Vaandrager. Petri Net Models for Algebraic Theories of Concurrency. LNCS, 259:224–242, 1987.Google Scholar
  12. [Hen88]
    Matthew Hennessy. Axiomatising Finite Concurrent Processes. SIAM Journal on Computing, 17(5):997–1017, 1988.CrossRefGoogle Scholar
  13. [Hoa85]
    Charles Anthony Richard Hoare. Communicating Sequential Processes. Series In Computer Science. Prentice-Hall, 1985.Google Scholar
  14. [Mil89]
    Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  15. [NEL89]
    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. [Plo81]
    Gordon D. Plotkin. A Structural Approach to Operational Semantics. Lecture Notes DAIMI FN-19, Department of Computer Science, Aarhus University, 1981.Google Scholar
  17. [Pra86]
    Vaughan Pratt. Modeling Concurrency with Partial Orders. International Journal of Parallel Programming, 15(1):33–71, 1986.CrossRefGoogle Scholar
  18. [Vog90]
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Luca Aceto
    • 1
  • Uffe Engberg
    • 2
  1. 1.Hewlett-Packard LaboratoriesPisa Science CenterPisaItalia
  2. 2.Computer Science DepartmentAarhus UniversityAarhus CDenmark

Personalised recommendations