A Complete Equational Axiomatization for Prefix Iteration with Silent Steps

Luca Aceto
Anna Ingólfsdóttir

January 1995


Fokkink ((1994) Inf. Process. Lett. 52: 333-337) has recently proposed a complete equational axiomatization of strong bisimulation equivalence for the language obtained by extending Milner's basic CCS with prefix iteration. Prefix iteration is a variation on the original binary version of the Kleene star operation tex2html_wrap_inline23 obtained by restricting the first argument to be an atomic action. In this paper, we extend Fokkink's results to a setting with the unobservable action tex2html_wrap_inline25 by giving a complete equational axiomatization of Milner's observation congruence over Fokkink's language. The axiomatization is obtained by extending Fokkink's axiom system with two of Milner's standard tex2html_wrap_inline25 -laws and the following three equations that describe the interplay between the silent nature of tex2html_wrap_inline25 and prefix iteration:


Using a technique due to Groote, we also show that the resulting axiomatization is tex2html_wrap_inline31 -complete, i.e., complete for equality of open terms.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.