Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 2, April 2002: pp. 301-320

An Equational Axiomatization of Bisimulation over Regular Expressions

Flavio Corradini1, Rocco De Nicola2 and Anna Labella3

1Dip. di Mat. Pura ed Appl., Università dell'Aquila, Italy. E-mail: flavio@univaq.it
2Dip. di Sistemi e Informatica, Università di Firenze, Italy. E-mail: denicola@dsi.unifi.it
3Dip. di Scienze dell'Informazione, Università di Roma "La Sapienza", Italy. E-mail: labella@dsi.uniroma1.it

We provide a finite equational axiomatization for bisimulation equivalence of nondeterministic interpretation of regular expressions. Our axiomatization is heavily based on the one by Salomaa, that provided an implicative axiomatization for a large subset of regular expressions, namely all those that satisfy the non-empty word property (i.e. without 1 summands at the top level) in *-contexts. Our restriction is similar, it essentially amounts to recursively requiring that the non-empty word property be satisfied not just at top level but at any depth. We also discuss the impact on the axiomatization of different interpretations of the 0 term, interpreted either as a null process or as a deadlock.

Keywords: Bisimulation; concurency; equational axiomatization; nondeterminism; process algebras; regular expressions

Table of Contents   Full-Text PDF (195 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement