Abstract <p>We present an efficient algorithm for checking language equivalence of states in top-down deterministic finite tree automata (DFTAs). Unlike string automata, tree automata operate over hierarchical structures, posing unique challenges for algorithmic analysis. Our approach reduces the equivalence checking problem to that of checking the solvability of a system of language-theoretic equations which specify the behavior of a DFTA. By constructing such a system of equations and systematically manipulating with it through substitution and conflict detection rules, we develop a decision procedure that determines whether two states accept the same tree language. We formally prove the correctness and termination of the algorithm and establish its worst-case time complexity as <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\(O(n^{2})\)</EquationSource> <!--CMatCMGU2570021Zakharov-m1--> </InlineEquation> under the RAM (Random Access Machine) model of computation augmented with pointers.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On the Equivalence Checking Problem for Deterministic Top-Down Automata

  • V. A. Zakharov,
  • Zhibo Deng

摘要

Abstract

We present an efficient algorithm for checking language equivalence of states in top-down deterministic finite tree automata (DFTAs). Unlike string automata, tree automata operate over hierarchical structures, posing unique challenges for algorithmic analysis. Our approach reduces the equivalence checking problem to that of checking the solvability of a system of language-theoretic equations which specify the behavior of a DFTA. By constructing such a system of equations and systematically manipulating with it through substitution and conflict detection rules, we develop a decision procedure that determines whether two states accept the same tree language. We formally prove the correctness and termination of the algorithm and establish its worst-case time complexity as \(O(n^{2})\) under the RAM (Random Access Machine) model of computation augmented with pointers.