A POLYNOMIAL-TIME ALGORITHM FOR CHECKING THE INCLUSION FOR REAL-TIME DETERMINISTIC RESTRICTED ONE-COUNTER AUTOMATA WHICH ACCEPT BY FINAL-STATE

A deterministic pushdown automaton (dpda) having just one stack symbol is called a deterministic restricted one-counter automaton (droca). A deterministic one-counter automaton (doca) is a dpda having only one stack symbol, with the exception of a bottom-of-stack marker. The clas s of languages accepted by droca's which accept by final state is a pr oper subclass of the class of languages accepted by doca's. Valiant ha s proved the decidability of the equivalence problem for doca's and th e undecidability of the inclusion problem for doca's. Hence the decida bility of the equivalence problem for droca's is obvious. In this pape r, we evaluate the upper bound of the length df the shortest input str ing (witness) that disproves the inclusion for a pair of real-time dro ca's which accept by final state, and present a new direct branching a lgorithm for checking the inclusion for a pair of languages accepted b y these droca's. Then we show that the worst-case time complexity of o ur algorithm is polynomial in the size of these droca's.