Equivalence of Deterministic One-Counter Automata is NL-complete

TL;DR

This paper establishes that determining language equivalence of deterministic one-counter automata is NL-complete, providing a tight complexity classification and a polynomial-length distinguishing word characterization.

Contribution

It proves the NL-completeness of the equivalence problem and shows that inequivalence can be distinguished by a polynomial-length word, improving previous superpolynomial bounds.

Findings

Language equivalence is NL-complete.

Inequivalence can be distinguished by a polynomial-length word.

Provides a tight complexity classification for the problem.

Abstract

We prove that language equivalence of deterministic one-counter automata is NL-complete. This improves the superpolynomial time complexity upper bound shown by Valiant and Paterson in 1975. Our main contribution is to prove that two deterministic one-counter automata are inequivalent if and only if they can be distinguished by a word of length polynomial in the size of the two input automata.