Iosif, R.; Rogalewicz, A. Automata-Based Termination Proofs. Comput. Inform. 2013, 32, 739-775.