Failures semantics for a simple process language with refinement
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].
KeywordsOperational Semantic Sequential Composition Label Process Denotational Semantic Refinement Operator
Unable to display preview. Download preview PDF.
- [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
- [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
- [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
- [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
- [Eng90]Uffe Henrik Engberg. True Concurrency Can Be Traced. Technical Report DAIMI PB-308, Department of Computer Science, Aarhus University, April 1990.Google Scholar
- [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
- [Gla90]Rob van Glabbeek. The Refinement Theorem for ST-bisimulation. To appear in Proc. IFIP Working Group, Sea of Galilee, 1990.Google Scholar
- [Gra81]Jan Grabowski. On Partial Languages. Annales Societatis Mathematicae Polonae, IV(2):427–498, 1981.Google Scholar
- [GV87]Rob van Glabbeek and Fritz Vaandrager. Petri Net Models for Algebraic Theories of Concurrency. LNCS, 259:224–242, 1987.Google Scholar
- [Hoa85]Charles Anthony Richard Hoare. Communicating Sequential Processes. Series In Computer Science. Prentice-Hall, 1985.Google Scholar
- [Mil89]Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
- [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
- [Plo81]Gordon D. Plotkin. A Structural Approach to Operational Semantics. Lecture Notes DAIMI FN-19, Department of Computer Science, Aarhus University, 1981.Google Scholar
- [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