On the equivalence checking problem for deterministic top-down automata

Recieved: 04/18/2025

Accepted: 05/04/2025

Keywords: tree automaton, tree language, equivalence checking, language equation

To cite this article

Zakharov V., Deng Zhibo On the equivalence checking problem for deterministic top-down automata. // Moscow University Journal. Series 15. Computational Mathematics and Cybernetics. 2025. N 4, p.38-45 https://doi.org/10.55959/MSU/0137–0782–15–2025–49–4–38–45.

This work is licensed under a Сreative Commons Atribiution - NonCommercial 4.0 International (CC BY-NC 4.0)

Zakharov V. (Shenzhen MSU-BIT University)
Deng Zhibo (Shenzhen MSU-BIT University)

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²) under the RAM (Random Access Machine) model of computation augmented with pointers.