
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Control Problem of a Class of Pushdown Automata Based on Posets and Its Application to Resolution Deductions
Susumu YAMASAKI
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E78D
No.11
pp.14881497 Publication Date: 1995/11/25 Online ISSN:
DOI: Print ISSN: 09168532 Type of Manuscript: PAPER Category: Automata, Languages and Theory of Computing Keyword: infinitestate pushdown automata, stack structure, partially ordered set, resolution deduction,
Full Text: PDF>>
Summary:
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.

