### A Complete Equational Axiomatization for Prefix Iteration with Silent Steps

#### Abstract

Fokkink ((1994) Inf. Process. Lett. 52: 333{337) has recently proposed a complete

equational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),

i.e., 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

p*q 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 by

giving a complete equational axiomatization of Milner's observation congruence over

MPA_delta^*(A_tau ).

The axiomatization is obtained by extending Fokkink's axiom system

with two of Milner's standard tau-laws and the following three equations that describe

the interplay between the silent nature of tau and prefix iteration:

tau . x = tau*x

a*(x+tau.y) = a*(x+tau.y + a.y)

tau.(a*x) = a*(tau.a*x) .

Using a technique due to Groote, we also show that the resulting axiomatization is

omega-complete, i.e., complete for equality of open terms.

AMS Subject Classification (1991): 68Q40, 68Q42.

CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.

Keywords and Phrases: Minimal Process Algebra, prefix iteration, equational

logic, omega-completeness, observation congruence.

equational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),

i.e., 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

p*q 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 by

giving a complete equational axiomatization of Milner's observation congruence over

MPA_delta^*(A_tau ).

The axiomatization is obtained by extending Fokkink's axiom system

with two of Milner's standard tau-laws and the following three equations that describe

the interplay between the silent nature of tau and prefix iteration:

tau . x = tau*x

a*(x+tau.y) = a*(x+tau.y + a.y)

tau.(a*x) = a*(tau.a*x) .

Using a technique due to Groote, we also show that the resulting axiomatization is

omega-complete, i.e., complete for equality of open terms.

AMS Subject Classification (1991): 68Q40, 68Q42.

CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.

Keywords and Phrases: Minimal Process Algebra, prefix iteration, equational

logic, omega-completeness, observation congruence.

#### Full Text:

PDFDOI: http://dx.doi.org/10.7146/brics.v2i5.19507

ISSN: 0909-0878

Hosted by the State and University Library and Aarhus University Library