Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Boolean Closure of Deterministic Top-Down Tree Automata

Christof Löding, Wolfgang Thomas

TL;DR

This work investigates the Boolean closure of languages recognized by deterministic top-down tree automata (DTDA), denoted Bool($\mathcal{T}(DTDA)$). It introduces DTDA with set acceptance to provide a direct automata-theoretic characterization of Bool($\mathcal{T}(DTDA)$) and demonstrates closure under Boolean operations, including practical non-membership proofs via simple counterexamples. For fixed $k$, the authors prove decidability of membership in $k$-Bool($\mathcal{T}(DTDA)$) by reducing to monadic second-order logic (MSO) on the infinite $|\Gamma|$-branching tree and leveraging Rabin’s decidability results for MSO on trees. This yields a workable decision procedure for bounded Boolean combinations of DTDA languages and highlights significant open questions about the full decidability of Bool($\mathcal{T}(DTDA)$) and potential characterizations via minimal automata patterns.

Abstract

The class of Boolean combinations of tree languages recognized by deterministic top-down tree automata (also known as deterministic root-to-frontier automata) is studied. The problem of determining for a given regular tree language whether it belongs to this class is open. We provide some progress by two results: First, a characterization of this class by a natural extension of deterministic top-down tree automata is presented, and as an application we obtain a convenient method to show that certain regular tree languages are outside this class. In the second result, it is shown that, for fixed $k$, it is decidable whether a regular tree language is a Boolean combination of $k$ tree languages recognized by deterministic top-down tree automata.

On the Boolean Closure of Deterministic Top-Down Tree Automata

TL;DR

This work investigates the Boolean closure of languages recognized by deterministic top-down tree automata (DTDA), denoted Bool(). It introduces DTDA with set acceptance to provide a direct automata-theoretic characterization of Bool() and demonstrates closure under Boolean operations, including practical non-membership proofs via simple counterexamples. For fixed , the authors prove decidability of membership in -Bool() by reducing to monadic second-order logic (MSO) on the infinite -branching tree and leveraging Rabin’s decidability results for MSO on trees. This yields a workable decision procedure for bounded Boolean combinations of DTDA languages and highlights significant open questions about the full decidability of Bool() and potential characterizations via minimal automata patterns.

Abstract

The class of Boolean combinations of tree languages recognized by deterministic top-down tree automata (also known as deterministic root-to-frontier automata) is studied. The problem of determining for a given regular tree language whether it belongs to this class is open. We provide some progress by two results: First, a characterization of this class by a natural extension of deterministic top-down tree automata is presented, and as an application we obtain a convenient method to show that certain regular tree languages are outside this class. In the second result, it is shown that, for fixed , it is decidable whether a regular tree language is a Boolean combination of tree languages recognized by deterministic top-down tree automata.
Paper Structure (5 sections, 7 theorems, 7 equations, 2 figures)

This paper contains 5 sections, 7 theorems, 7 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Automata with Set Acceptance
  4. Decidability of Membership in $k$-${\rm Bool}({\@fontswitch\mathcal{T}}({\rm DTDA}))$
  5. Conclusion

Key Result

Theorem 1

A tree language $T$ over $\Sigma$ is DTDA-recognizable iff $T=\mathit{trees}(P)$ for a regular set $P \subseteq \Gamma^*$ of paths.

Figures (2)

  • Figure 1: The set $\mathit{trees}(P)$ for $P = \{a1b1c, a1b2d, a1a1d, a1a2c, a2c, a2d, b2c\}$. Note that the path $b2c$ is in $P$ but does not occur in any of the trees because no tree with $b$ at the root can be built from paths in $P$.
  • Figure 2: Illustration for the proof of Proposition \ref{['twoexamples']}. All inner nodes of the tree are labeled with $a$. All leaves not shown in the illustration are labeled with $c$.

Theorems & Definitions (9)

  • Theorem 1: Viragh80
  • Remark 2
  • Remark 3
  • Proposition 4
  • Proposition 5
  • Proposition 6
  • Lemma 7
  • Theorem 8: Rabin69
  • Theorem 9