Manipulation of regular expressions under length constraints using zero-suppressed-BDDs

We present a new technique that broadens the scope of BDD application. It is a method for manipulating regular expressions that represent sets of sequences including repetitions of symbols. In general, sequences in the set represented by a regular expression have an infinite length and this makes representing and manipulating them difficult. In this paper, we introduce length constraints into a representation of regular expressions. Under these constraints, our method can represent and manipulate large-scale sets of sequences of regular expressions compactly and uniquely and greatly accelerates operations of regular expressions. As regular expressions can represent behaviors of a finite state machine, our technique provides a useful analysis method of finite state machines and can be applied to formal hardware verification techniques