Liveness Verification in TRSs Using Tree Automata and Termination Analysis
keywords: Term rewriting systems, liveness properties, finite tree automata, termination
This paper considers verification of the liveness property textsfLive(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 textsfLive(R, I, G).
reference: Vol. 29, 2010, No. 3, pp. 407–426
