Models of nondeterministic regular expressions

Nondeterminism is a direct outcome of interactions and is, therefore a cent ral ingredient for modelling concurrent systems. Trees are very useful for modelling nondeterministic behaviour. We aim at a tree-based interpretation of regular expressions and study the effect of removing the idempotence la w X+X=X and the distribution law X.(Y+Z)=X.Y+X.Z from Kleene algebras. We s how that the free model of the new set of axioms is a class of trees labell ed over A. We also equip regular expressions with a two-level behavioural s emantics. The basic level is described in terms of a class of labelled tran sition systems that are detailed enough to describe the number of equal act ions a system can perform from a given state. The abstract level is based o n a so-called resource bisimulation preorder that permits ignoring unintere sting details of transition systems. The three proposed interpretations of regular expressions (algebraic, denotational, and behavioural) are proven t o coincide. When dealing with infinite behaviours, we rely on a simple vers ion of the omega-induction and obtain a complete proof system also for the full language of nondeterministic regular expressions, (C) 1999 Academic Pr ess.