Liveness verification in trss using tree automata and termination analysis

Abstract

This paper considers verification of the liveness property Live(.R, I, G) for a term rewrite system (TRS) R, where I (Initial states) and G (Good states) are two sets of ground terms represented by finite tree automata. Considering I and G, we transform R to a new TRS R' such that termination of R' proves the property Live(R,I,G).