A POLYNOMIAL-TIME ALGORITHM FOR CHECKING THE INCLUSION FOR STRICT DETERMINISTIC RESTRICTED ONE-COUNTER AUTOMATA

A deterministic pushdown automaton (dpda) having just one stack symbol is called a deterministic restricted one-counter automaton (droca). W hen it accepts by empty stack, it is called strict. A deterministic on e-counter automaton (doca) is a dpda having only one stack symbol, wit h the exception of a bottom-of-stack marker. The class of languages ac cepted by strict droca's is a subclass of the class of languages accep ted by doca's. Valiant has proved the decidability of the equivalence problem for doca's and the undecidability of the inclusion problem for doca's. Hence the decidability of the equivalence problem for strict droca's is obvious. In this paper, we present a new direct branching a lgorithm for checking the inclusion for a pair of languages accepted b y strict droca's. Then we show that the worst-case time complexity of our algorithm is polynomial with respect to these automata.