Adding action refinement to a finite process algebra

  • Aceto L
  • Hennessy M
  • 9


    Mendeley users who have this article in their library.
  • 34


    Citations of this article.


In this paper we present a Process Algebra for the specification of concurrent, communicating processes which incorporates operators for the refinement of actions by processes, in addition to the usual operators for communication, nondeterminism, internal actions, and restrictions, and study a suitable notion of semantic equivalence for it. We argue that action refinements should not, in some formal sense, interfere with the internal evolution of processes and their application to processes should consider the restriction operator as a "binder." We show that, under the above assumptions, the weak version of the refine equivalence introduced by Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269) is preserved by action refinements and, moreover, is the largest such equivalence relation contained in weak bismulation equivalence. We also discuss an example showing that, contrary to what happens in Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269), refine equivalence and timed equivalence are different notions of equivalence over the language considered in this paper. © 1994 Academic Press, Inc.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • L. Aceto

  • M. Hennessy

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free