Volume 33, Numbers 3-4, 341-383, DOI: 10.1007/s10817-004-6246-0

Reachability Analysis over Term Rewriting Systems

Guillaume Feuillade, Thomas Genet and Valérie Viet Triem Tong

From the issue entitled "First-Order Theorem Proving"

View Related Documents

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 \textsf{Timbuk} tool. Furthermore, we show that many 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 \textsf{Timbuk} . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.

Keywords  completion algorithm - reachability analysis - term rewriting - Timbuk - tree automaton

Fulltext Preview

Image of the first page of the fulltext document