Towards More Precise Rewriting Approximations

To check a system, some verification techniques consider a set of terms

$$I$$

that represents the initial configurations of the system, and a rewrite system

$$R$$

that represents the system behavior. To check that no undesirable configuration is reached, they compute an over-approximation of the set of descendants (successors) issued from

$$I$$

by

$$R$$

, expressed by a tree language. Their success highly depends on the quality of the approximation. Some techniques have been presented using regular tree languages, and more recently using non-regular languages to get better approximations: using context-free tree languages [

16

] on the one hand, using synchronized tree languages [

2

] on the other hand. In this paper, we merge these two approaches to get even better approximations: we compute an over-approximation of the descendants, using synchronized-context-free tree languages expressed by logic programs. We give several examples for which our procedure computes the descendants in an exact way, whereas the former techniques compute a strict over-approximation.