Mousazadeh, M.; Ladani, B. T.; Zantema, H. Liveness Verification in TRSs Using Tree Automata and Termination Analysis. Comput. Inform. 2012, 29, 407-426.