CPO Models for a Class of GSOS Languages

Luca Aceto
Anna Ingólfsdóttir

In 6th NWPT, pages 51-66

Abstract:

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.

Comments
BRICS, Department of Mathematics and Computer Science, Aalborg University, Denmark.

Available as PostScript, DVI.

BRICS WWW home page