Reachability Analysis over Term Rewriting Systems

Guillaume Feuillade 1 Thomas Genet 2 Valérie Viet Triem Tong 2
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00071609
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:14:14 PM
Last modification on : Thursday, December 13, 2018 - 8:06:02 PM
Long-term archiving on : Sunday, April 4, 2010 - 8:21:40 PM

Identifiers

  • HAL Id : inria-00071609, version 1

Citation

Guillaume Feuillade, Thomas Genet, Valérie Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. [Research Report] RR-4970, INRIA. 2003. ⟨inria-00071609⟩

Share

Metrics

Record views

354

Files downloads

420