© 2002 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Article |
An Equational Axiomatization of Bisimulation over Regular Expressions
1 Dip. di Mat. Pura ed Appl., Università dell'Aquila, Italy. E-mail: flavio{at}univaq.it 2 Dip. di Sistemi e Informatica, Università di Firenze, Italy. E-mail: denicola{at}dsi.unifi.it 3 Dip. di Scienze dell'Informazione, Università di Roma "La Sapienza", Italy. E-mail: labella{at}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
Received September 2000.