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 class of languages accepted by droca's which accept by final state is a proper subclass of the class of languages accepted 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 droca's is obvious. In this paper, we evaluate the upper bound of the length of the shortest input string (witness) that disproves the inclusion for a pair of real-time droca's which accept by final state, and present a new direct branching algorithm for checking the inclusion for a pair of languages accepted by these droca's. Then we show that the worst-case time complexity of our algorithm is polynomial in the size of these droca's.
社団法人電子情報通信学会の論文
1995-08-25