Sasha Rubin
"An introduction to Automatic Structures"

Rabin showed, using automata theory, that the monadic second-order
theory of two successors (S2S) is decidable. He concluded that various
other MSO theories (such as that of the rational order) are decidable
by interpreting these in S2S. Using a different type of interpretation
one may conclude that the first-order theories of certain structures
are decidable. Such structures are called automatic. This talk will
focus on basic properties of automatic structures, and mention some
foundational problems that are still open.