Termination criteria for tree automata completion

Thomas Genet 1, *
* Auteur correspondant
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper presents two criteria for the termination of tree automata completion. Tree automata completion is a technique for computing a tree automaton recognizing or over-approximating the set of terms reachable w.r.t. a term rewriting system. The first criterion is based on the structure of the term rewriting system itself. We prove that for most of the known classes of linear rewriting systems preserving regularity, the tree automata completion is terminating. Moreover, it outputs a tree automaton recognizing exactly the set of reachable terms. When the term rewriting system is outside of such classes, the set of reachable terms can be approximated using a set of equations defining an abstraction. The second criterion, which holds for any left-linear term rewriting system, defines sufficient restrictions on the set of equations for the tree automata completion to terminate. We then show how to take advantage of this second criterion to use completion as a new static analysis technique for functional programs. Some examples are demonstrated using the Timbuk completion tool.
Type de document :
Article dans une revue
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2016, 85, Issue 1, part 1, pp.3-33. 〈10.1016/j.jlamp.2015.05.003〉
Liste complète des métadonnées

Littérature citée [49 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01194533
Contributeur : Thomas Genet <>
Soumis le : lundi 7 septembre 2015 - 10:59:45
Dernière modification le : mardi 16 janvier 2018 - 15:54:17
Document(s) archivé(s) le : mardi 8 décembre 2015 - 11:12:49

Fichier

Genet-JLAMP15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Thomas Genet. Termination criteria for tree automata completion. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2016, 85, Issue 1, part 1, pp.3-33. 〈10.1016/j.jlamp.2015.05.003〉. 〈hal-01194533〉

Partager

Métriques

Consultations de la notice

435

Téléchargements de fichiers

85