Survey on infinite automata

The term of infinite automaton was introduced to
designate finitely generated infinite labeled graphs together with two
sets of initial and final vertices. These infinite automata naturally arise
in the verification of systems with infinite state spaces. They can also
be seen as language acceptors: the accepted language being the set
of words labeling a path from an initial vertex to a final vertex.

In this talk, we will try give an overview of the main families of
infinite automata that have been studied in the past twenty-years. We
will present their logical properties as well as their language
theoritical properties.