Toward Determining NFA Equivalence via QBFs

Equivalence of deterministic finite automata (DFAs) has been researched for several decades, but equivalence of nondeterministic finite automata (NFAs) is not as studied.  Equivalence of two NFAs is a PSPACE-complete problem.  NFA quivalence is a challenging theoretical problem with practical applications such as lexical analysis.  Quantified boolean formulas (QBFs) naturally encode PSPACE-complete problems, and we share our preliminary work towards determining NFA equivalence via QBFs.