Equivalence of pushdown automata via first-order grammars (Q2208249)

This article pertains to a line of research concerned with equivalence problems related to pushdown automata, which is known for its history of highly nontrivial results. Its origins can be traced back to \textit{S. Ginsburg} and \textit{S. Greibach} [Inf. Control 9, No. 6, 620--648 (1966; Zbl 0145.00802)], who have asked about decidability of the equivalence problem for deterministic context-free languages, i.e., of the language equivalence problem for deterministic pushdown automata. This question, which gradually became one of the most important open problems of theoretical computer science of its time, remained unsolved until the 1990s. \textit{V. Yu. Meitus} [Cybern. Syst. Anal. 28, No. 5, 672--690 (1992; Zbl 0875.68644)] published an affirmative solution to the problem, but it has not been widely recognised. The first generally accepted decidability proof, announced in 1997, was given by \textit{G. Sénizergues} [Theor. Comput. Sci. 251, No. 1--2, 1--166 (2001; Zbl 0957.68051)]. Several simplifications to the lengthy and technical proof of Sénizergues [loc. cit.], have been presented in subsequent works, such as [\textit{C. Stirling}, Theor. Comput. Sci. 255, No. 1--2, 1--31 (2001; Zbl 0974.68056); \textit{G. Sénizergues}, Theor. Comput. Sci. 281, No. 1--2, 555--608 (2002; Zbl 1050.68096)]. Finally, the ideas from these works have been rephrased by the author [in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012. Los Alamitos, CA: IEEE Computer Society. 415--424 (2012; Zbl 1360.68561)] using the framework of first-order grammars, which resulted in a further simplification of the decidability proof. Decidability of the language equivalence problem for deterministic pushdown automata has also been generalised by \textit{G. Sénizergues} [SIAM J. Comput. 34, No. 5, 1025--1106 (2005; Zbl 1079.68066)] to decidability of the bisimulation equivalence problem for equational graphs of finite out-degree or, equivalently, for nondeterministic pushdown automata with alternation-free transitions on the empty word. The present article simplifies the proof of this result, again by utilising the framework of first-order grammars. A sort of preliminary version of this article appeared in [Lect. Notes Comput. Sci. 8573, 232--243 (2014; Zbl 1410.68192)], but the decision algorithm presented therein has been significantly improved in a way that makes its eventual complexity analysis more conceivable.