2
$\begingroup$

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!

  • 4
    The fact that it is in NONELEMENTARY should discourage any attempts to implement the decision procedure...2011-03-16
  • 0
    Crossposted to [stackoverflow](http://stackoverflow.com/questions/5327506/decision-procedure-for-the-problem-of-regular-expression-equivalence-with-not).2011-03-16
  • 2
    FOL is semi-decidable but people still write theorem provers.2011-03-16
  • 1
    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.2011-03-17
  • 0
    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.2011-03-17

1 Answers 1

2

Stockmeyer and Meyer, "Word problems requiring exponential time", Proc. 5th ACM Symposium on the Theory of Computing, pp 1-9, 1973.

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.