CPO MODELS FOR COMPACT GSOS LANGUAGES

In this paper, we present a general way of giving denotational semanti cs to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail, and Meyer. The canonical mode l used for this purpose will be Abramsky's domain of synchronization t rees, and the denotational semantics automatically generated by our me thods will be guaranteed to be fully abstract with respect to the fini tely observable part of the bisimulation preorder. In the process of e stablishing the full abstraction result, we also obtain several genera l results on the bisimulation preorder (including a complete axiomatiz ation for it), and give a novel operational interpretation of GSOS lan guages. (C) 1996 Academic Press, Inc.