Michael Benedikt
Bell Laboratories

Some Decision Problems on Tree Automata

Classical string automata theory gives correspondences between
subclasses of regular languages and definability in logics (MSOL, FO
...).  In the string setting we have also decision procedures for
determining whether a regular language is definable in a given
logic. We discuss here the status of the corresponding questions for
regular tree languages. Our main result is an algebraic
characterization of definability, from which a decision procedure
follows. We give some applications of this in finite model theory
and databse theory.

This is joint work with Luc Segoufin.