The paper and slides are available. The tail of the slides are a brief discussion of Tree Set Automata for Prolog Mode Analysis (2016) in hopes of soliciting feedback on the larger research program.


Rigid Tree Automata (RTAs) are a strict super-class of Regular Tree Automata (TAs), additionally capable of recognizing certain nonlinear patterns such as {f⟨x, x⟩ ∣ x ∈ X}. RTAs were developed for use in tree-automata-based model checking; we hope to use them as part of a static analysis system for a logic programming language. In developing that system, we noted that RTAs are not closed under Kleene-star or pre-concatenation with a regular language. We now introduce a strict super-class of RTA, called Isolating Rigid Tree Automata, which can accept rigid structures with arbitrarily many isolated rigid substructures, such as “lists of equal pairs” by allowing rigidity to be confined within subtrees. This class is Kleene-star and concatenation closed and retains many features of RTAs, including linear-time emptiness testing and NP-complete membership testing. However, it gives up closure under intersection.


  author  = {Nathaniel Wesley Filardo and Jason Eisner},
  title   = {Rigid Tree Automata With Isolation},
  booktitle={Proceedings of the Fourth International Workshop on Trends in
            Tree Automata and Tree Transducers (TTATT)},
  year    = {2016},
  month   = {8},
  address = {Seoul}