Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
Yohan Boichut, Vivien Pelletier, Yohan Boichut, Vivien Pelletier · 2016
Abstract. Over-approximating the descendants (successors) of an ini-tial set of terms under a rewrite system is used in reachability analysis. The success of such methods depends on the quality of the approxima-tion. Regular approximations (i.e. those using finite tree automata) have been successfully applied to protocol verification and Java program anal-ysis. In [9, 2], non-regular approximations have been shown more precise than regular ones. In [3] (fixed version of [2]), we have shown that sound over-approximations using synchronized tree languages can be computed for left-and-right-linear term rewriting systems (TRS). In this paper, we present two new contributions extending [3]. Firstly, we show how to compute at least all innermost descendants for any left-linear TRS. Secondly, a procedure is introduced for computing over-approximations independently of the applied rewrite strategy for any left-linear TRS.