Erratum 1

In [1], we have described a technique for computing non-regular approximations using synchronized tree languages. This technique can handle the reachability problem of [2]. These synchronized tree languages [4, 3] are recognized using CSprograms [5], i.e. a particular class of Horn clauses. From an initial CS-program Prog and a left-linear term rewrite system (TRS) R, another CS-program Prog′ is computed in such a way that its language represents an over-approximation of the set of terms (called descendants) reachable by rewriting using R, from the terms of the language of Prog. This algorithm is called completion. However, the assumptions of the result showing that all the descendants are obtained, i.e. Theorem 14 in [1], are not correct. Actually, preserving should be replaced by non-copying (a variable cannot occur several times in the head of a clause). However, the non-copying nature of a CS-program is not preserved by completion as soon as the given TRS is not right-linear. Consequently, the final result presented in [1] holds for completely linear TRS, and not for just left-linear TRS. In this paper, we propose a correction of [1], assuming that the initial CSprogram is non-copying, and the TRS is completely linear (see Section 3).