Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions


IEICE TRANSACTIONS on Information and Systems   Vol.E78-D   No.11   pp.1488-1497
Publication Date: 1995/11/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Automata, Languages and Theory of Computing
infinite-state pushdown automata,  stack structure,  partially ordered set,  resolution deduction,  

Full Text: PDF>>
Buy this Article

In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.