In theoretical computer science and formal language theory, the equivalence problem is the question of determining, given two representations of formal languages, whether they denote the same formal language.

The complexity and decidability of this decision problem depend upon the type of representation under consideration.

For instance, in the case of finite-state automata, equivalence is decidable, and the problem is PSPACE-complete. Further, in the case of deterministic pushdown automata, equivalence is decidable, Géraud Sénizergues won the Gödel Prize for this result. Subsequently, the problem was shown to lie in TOWER, the least non-elementary complexity class.

It becomes an undecidable problem for pushdown automata or any machine that can decide context-free languages or more powerful languages.