PI-1565: Reachability Analysis over - Term Rewriting Systems
Guillaume Feuillade, Thomas Genet, Valérie Viet Triem Tong
http://www.irisa.fr/bibli/publi/pi/2003/1565/1565.html
40 pages - octobre 2003

Abstract
This paper surveys some techniques and tools for achieving reachability
analysis over term rewriting systems. The core of those techniques is a
generic tree automata completion algorithm used to compute in an exact
or approximated way the set of descendants (or reachable terms). This
algorithm has been implemented in the Timbuk tool. Furthermore, we show
that classes with regular sets of descendants of the literature
corresponds to specific instances of the tree automata completion
algorithm and can thus be efficiently computed by Timbuk. An extension
of the completion algorithm to conditional term rewriting systems and
some applications are also presented.

Résumé
Cet article regroupe un ensemble de techniques destinées à l'analyse
d'atteignabilité sur les systèmes de réécriture. La technique principale
est un algorithme générique de complétion des automates d'arbre qui
permet de calculer de façon exacte ou approchée l'ensemble des
descendants (ou termes accessibles). Cet algorithme est implanté dans
l'outil Timbuk. Nous montrons également que les classes ayant des
ensembles de descendants réguliers, que l'on trouve dans la littérature,
correspondent à des instances spécifiques de l'algorithme de complétion
d'automates. En conséquence, ces classes régulières peuvent être
calculées de façon efficace par Timbuk. Nous proposons également une
extension de l'algorithme de complétion au cas des systèmes de
réécriture conditionnels ainsi que des applications.

Keywords: Term Rewriting Systems, Reachability, Tree Automata

Mots clefs: Systèmes de réécriture, Atteignabilité, Automates d'arbres