The last decade has seen renewed interest in automated techniques for proving the termination of programs. A popular termination criterion is based on the covering of the transitive hull of the transition relation of a program by a finite number of well-founded relations. In an automated analysis, this termination criterion is usually established by an inductive proof using transition predicate abstraction. Such termination proofs have the structure of a finite automaton. These automata, which we call transition automata, are the central object of study in this talk. Our main results are as follows: (1) A previous criterion for termination analysis with transition automata is not complete; we provide a complete criterion. (2) We show how to bound the height of the transition relation of the program using the termination proof by transition predicate abstraction. This result has applications in the automated complexity analysis of programs. (3) We show that every termination proof by transition predicate abstraction gives rise to a termination proof by the size-change abstraction; this connection is crucial to obtain results (1) and (2) from previous results on the size-change abstraction. Further, our result establishes that transition predicate abstraction and size-change abstraction have the same expressivity for automated termination proofs.