A Congruence-Based Perspective on Finite Tree Automata

TL;DR

This paper introduces a congruence-based framework for determinization and minimization of finite tree automata, extending classical automata theory results to the more complex tree structures.

Contribution

It extends Brzozowski's minimization algorithm to tree automata using congruences, providing correctness proofs and new insights into automata-based and language-based congruences.

Findings

Proved correctness of a Brzozowski-style minimization for tree automata.

Extended automata-based congruences to trees, overcoming expressive limitations.

Linked automata-based and language-based congruences for minimal automata.

Abstract

We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algorithm for tree automata. First, we prove correct this method relying on the following fact: when the automata-based and the language-based congruences coincide, determinizing the automaton yields the minimal one. Such automata-based congruences, in the case of word automata, are defined using pre and post operators. Now we extend these operators to tree automata, a task that is particularly challenging due to the reduced expressive power of deterministic top-down (or equivalently co-deterministic bottom-up) automata. We leverage further our framework to offer an extension of the original result by Brzozowski for word automata.