Comparing Syntactic and Semantic Action Refinement

AbstractThe semantic definition of action refinement on labelled configuration structures is compared with the notion ofsyntactic substitution, which can be used as another notion of action refinement in a process algebraic setting. The comparison is done by studying a process algebra equipped with sequential composition, parallel composition with an explicit synchronisation set, and an operator for action refinement. On the one hand, the language (including the refinement operator) is given a configuration structure semantics. On the other hand, a reduction procedure transforms a process termPinto aflatterm (i.e., with the refinement operator not occurring in it)red(P) by means of syntactic substitution, defined in a structural inductive way. The main aim of the paper is to investigate general conditions under which the termsPandred(P) have the same semantics. The results we present are essentially dependent on the question whether the refined action can be synchronised or not. In the latter case,Pandred(P) give rise to isomorphic configuration structures under mild assumptions. The former case is considerably more difficult, since then refinement cannot be expected to distribute over parallel composition. We give necessary and sufficientsemanticconditions under which distribution still holds up to semantic equivalence. Subsequently, we also give sufficient (but not necessary)syntacticconditions for reducible terms. Finally, we generalise these results to a language with recursion