ADDING ACTION REFINEMENT TO A FINITE PROCESS ALGEBRA

In this paper we present a Process Algebra for the specification of co ncurrent, communicating processes which incorporates operators for the refinement of actions by processes, in addition to the usual operator s for communication, nondeterminism, internal actions, and restriction s, and study a suitable notion of semantic equivalence for it. We argu e that action refinements should not, in some formal sense, interfere with the internal evolution of processes and their application to proc esses should consider the restriction operator as a ''binder.'' We sho w that, under the above assumptions, the weak version of the refine eq uivalence introduced by Aceto and Hennessy ((1993) Inform. and Comput. 103, 204-269) is preserved by action refinements and, moreover, is th e largest such equivalence relation contained in weak bismulation equi valence. We also discuss an example showing that, contrary to what hap pens in Aceto and Hennessy ((1993) Inform. and Comput. 103, 204-269), refine equivalence and timed equivalence are different notions of equi valence over the language considered in this paper. (C) 1994 Academic Press, Inc.