# Decision procedure for the problem of regular expression equivalence with not

As stated in the title, I need a decision procedure for the problem of regular expression equivalence with not. Wikipedia states the problem is in the NONELEMENTARY complexity class. All I really need is link to the paper that describes the problem and its solution. This is NOT a homework problem. I need the procedure for a program static analysis tool.

Thanks!

-
The fact that it is in NONELEMENTARY should discourage any attempts to implement the decision procedure... –  Aryabhata Mar 16 '11 at 16:42
Crossposted to stackoverflow. –  Chris Eagle Mar 16 '11 at 16:51
FOL is semi-decidable but people still write theorem provers. –  Tony Johnson Mar 16 '11 at 17:56
But if you're expecting to use nested 'not's, as one might expect if you need to implement this, the stack of two's goes up by the nesting depth. By depth 5 or $2^{65536}$, you're already well beyond the number of particles in the universe. –  Mitch Mar 17 '11 at 1:59
The hope is that the nested not's will be avoided, but if they are there, a worst case time will be displayed that will encourage the user to fiddle around with the expression. –  Tony Johnson Mar 17 '11 at 12:53

The derivation is fairly intuitive: every negation in the regular expression 'somehow' requires conversion to a DFA, and a lower bound of $\Theta(2^n)$ states guaranteed for conversion. Nest your $\neg$'s and you get a stack of exponentials.