A CAUSAL OPERATIONAL SEMANTICS OF ACTION REFINEMENT

A TCSP-like concurrent language is extended with an operator for actio n refinement which plays a role similar to that of procedure-call for sequential languages. The language is given a denotational semantics t hat fully expresses causality in terms of Causal Trees. These are Sync hronization Trees where each are has a richer labelling containing, be sides an action name, also the set of backward pointers to those arcs ''causing'' the present action, An operational semantics reflecting ca usality is also defined in SOS style by a causal transition system, th e unfoldings of which are causal trees. The denotational and operation al semantics agree up to causal bisimulation, which is proved to be a congruence for ail the operators of the calculus; notably, for the ref inement operator. Also, a complete set of axioms is provided that char acterizes the congruence classes of causal bisimulation for finite age nts. The main result of the paper is an operational semantics firmly b ased on a view of action refinement as purely semantic substitution. T herefore, its operational definition provides a ''parallel copy rule,' ' i.e., the concurrent analogous of the classic ''copy rule'' for sequ ential languages. (C) 1995 Academic Press, Inc.