The theory of ends, pushdown automata, and second-order logic (Q1084096)

In this carefully written paper the authors give detailed graph-theoretic proofs of several interesting finiteness results in the automata theory of ends, which deals with well behaved ways of going to infinity. Their approach is to define a broad class of graphs called ''context-free graphs''. Basically, the underlying idea is that a context-free graph is well behaved at infinity. The bottom line is that a graph is context-free iff it is the complete transition graph of some pushdown automaton. Such graphs are generalizations of Cayley graphs of context-free groups. Using Rabin's theorem on the decidability of monadic second-order theory for the infinite binary tree, such graphs have also a decidable monadic second-order theory. Solvable decision problems about tiling systems and cellular automata are discussed in great detail. Finally, the authors show that the membership problem and the inclusion problem for reachability sets of vector addition systems on a context- free graph are uniformly solvable.