## Abstract / Description of output

Flat iteration is a variation on the original binary version of the Kleene star operation P *Q, obtained by restricting the first argument to be a sum of atomic actions. It generalizes prefix iteration, in which the first argument is a single action. Complete finite equational axiomatizations are given for five notions of bisimulation congruence over basic CCS with flat iteration, viz. strong congruence, branching congruence, η-congruence, delay congruence and weak congruence. Such axiomatizations were already known for prefix iteration and are known not to exist for general iteration. The use of flat iteration has two main advantages over prefix iteration:

1. The current axiomatizations generalize to full CCS, whereas the prefix iteration approach does not allow an elimination theorem for an asynchronous parallel composition operator.

2. The greater expressiveness of flat iteration allows for much shorter completeness proofs.

In the setting of prefix iteration, the most convenient way to obtain the completeness theorems for η-, delay, and weak congruence was by reduction to the completeness theorem for branching congruence. In the case of weak congruence this turned out to be much simpler than the only direct proof found. In the setting of flat iteration on the other hand, the completeness theorems for delay and weak (but not η-) congruence can equally well be obtained by reduction to the one for strong congruence, without using branching congruence as an intermediate step. Moreover, the completeness results for prefix iteration can be retrieved from those for flat iteration, thus obtaining a second indirect approach for proving completeness for delay and weak congruence in the setting of prefix iteration.

1. The current axiomatizations generalize to full CCS, whereas the prefix iteration approach does not allow an elimination theorem for an asynchronous parallel composition operator.

2. The greater expressiveness of flat iteration allows for much shorter completeness proofs.

In the setting of prefix iteration, the most convenient way to obtain the completeness theorems for η-, delay, and weak congruence was by reduction to the completeness theorem for branching congruence. In the case of weak congruence this turned out to be much simpler than the only direct proof found. In the setting of flat iteration on the other hand, the completeness theorems for delay and weak (but not η-) congruence can equally well be obtained by reduction to the one for strong congruence, without using branching congruence as an intermediate step. Moreover, the completeness results for prefix iteration can be retrieved from those for flat iteration, thus obtaining a second indirect approach for proving completeness for delay and weak congruence in the setting of prefix iteration.

Original language | English |
---|---|

Title of host publication | CONCUR'97: Concurrency Theory - 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings |

Editors | A. Mazurkiewicz, J. Winkowski |

Publisher | Springer Berlin Heidelberg |

Pages | 228-242 |

Number of pages | 15 |

ISBN (Electronic) | 978-3-540-69188-4 |

ISBN (Print) | 978-3-540-63141-5 |

DOIs | |

Publication status | Published - 11 Jun 1997 |

Event | The 8th International Conference on Concurrency Theory, 1997 - Warsaw, Poland Duration: 1 Jul 1997 → 4 Jul 1997 Conference number: 8 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 1243 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | The 8th International Conference on Concurrency Theory, 1997 |
---|---|

Abbreviated title | CONCUR 1997 |

Country/Territory | Poland |

City | Warsaw |

Period | 1/07/97 → 4/07/97 |