The notion of action refinement has been studied intensively in the past few years. It is usually introduced in the form of an operator in a process algebraic language, for which a denotational semantics in a suitable model is then given. In this paper we complement this approach by defining a corresponding operational semantics for refinement, in the form of derivation rules for a transition relation. Because of the (well-known) fact that ordinary transition systems are not expressive enough to capture the effects of refinement, we use an event-based transition system model described elsewhere in the literature. The operational semantics of refinement thus defined is equivalent (in fact event isomorphic) to the usual denotational semantics.
|Number of pages||16|
|Publication status||Published - 1995|
|Event||Structures in Concurrency Theory - Berlin, Germany|
Duration: 1 Jan 1995 → 1 Jan 1995
|Workshop||Structures in Concurrency Theory|
|Period||1/01/95 → 1/01/95|