Equational Approximations for Tree Automata Completion

Thomas Genet 1 Vlad Rusu 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : In this paper we deal with the verification of safety properties of infinite-state systems modeled by term-rewriting systems. An over-approximation of the set of reachable terms of a term- rewriting system R is obtained by automatically constructing a finite tree automaton. The construction is parameterized by a set E of equations on terms, and we also show that the approximating automata recognize at most the set of R/E-reachable terms. Finally, we present some experiments carried out with the implementation of our algorithm. In particular, we show how some approximations from the literature can be defined using equational approximations.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp.574-597
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00495405
Contributeur : Mister Dart <>
Soumis le : vendredi 25 juin 2010 - 22:13:13
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 27 septembre 2010 - 12:01:45

Fichier

genet-rusu-JSC-SCSS.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00495405, version 1

Citation

Thomas Genet, Vlad Rusu. Equational Approximations for Tree Automata Completion. Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp.574-597. 〈inria-00495405〉

Partager

Métriques

Consultations de la notice

907

Téléchargements de fichiers

204