Synchronized tree languages for reachability in non-right-linear term rewrite systems

Abstract

Over-approximating the descendants (successors) of an initial set of terms under a rewrite system is used in reachability analysis. The success of such methods depends on the quality of the approximation. Regular approximations (i.e. those using finite tree automata) have been successfully applied to protocol verification and Java program analysis. In [2,10], 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 leftlinear TRS. Secondly, a procedure is introduced for computing overapproximations independently of the applied rewrite strategy for any left-linear TRS.