LIVENESS VERIFICATION IN TRSS USING TREE AUTOMATA AND TERMINATION ANALYSIS
Mousa Mousazadeh, Behrouz Tork Ladani, Hans Zantema, TU Eindhoven, M. Mousazadeh, B. Tork Ladani, H. Zantema · TU/e Research Portal · 2010
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).