An extended direct branching algorithm for checking equivalence of deterministic pushdown automata (Q801689)

This paper extends the author's direct branching algorithm [Inf. Control. 52, 187-238 (1982; Zbl 0541.68053)] for checking equivalence of deterministic pushdown automata. It does so by providing a technique called 'halting' for dealing with nodes with unbounded degree in the comparison tree. This may occur when a skipping step may be applied infinitely many times to a certain node, as a result of infinite sequences of \(\epsilon\)-moves. This extension allows the algorithm to check equivalence of the deterministic pushdown automata when none of them is real-time, but in a certain condition that properly contains a case where one of them is real-time strict.