A fun piece of tree automata theory and part of the work that went into chapter 4 of my thesis.

The paper is available locally.


In Tree Automata Techniques and Applications (TATA), the emptiness test of non-deterministic Reduction Automata (RA) is shown to be undecidable. The proof is a remarkable construction, encoding the evolution of a two-counter machine (2CM) into a form analyzable by reduction automata. We have, in studying the myriad families of tree automata with equality constraints, found this 2CM reduction to be unexpectedly useful: we exhibit a family of simple tree languages whose intersection is exactly the reduction at hand. These simpler languages are often easily found to be recognized (or not) by particular classes; when they are, the 2CM reduction implies that the class at hand has at most one of a decidable emptiness test or intersection closure. We first review the relevant machines (RA, 2CM) and then present an alternate exposition of the proof from TATA, before giving our decomposed machines and concluding.


  author  = {Filardo, Nathaniel Wesley},
  title   = {The Two-Counter Machine Strikes Again},
  year    = {2016}


Relative to its initial publication here, the following errata have been fixed in this edition.