Characterizing Conclusive Approximations by Logical Formulae

Yohan Boichut 1 Thi-Bich-Hanh Dao 1 Valérie Murat 2, *
* Auteur correspondant
2 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Considering an initial set of terms E, a rewriting relation R and a goal set of terms Bad, reachability analysis in term rewriting tries to answer to the following question: does there exists at least one term of Bad that can be reached from E using the rewriting relation R? Some of the approaches try to show that there exists at least one term of Bad reachable from E using the rewriting relation R by computing the set of reachable terms. Some others tackle the unreachability problem i.e. no term of Bad is reachable by rewriting from E. For the latter, over-approximations are computed. A main obstacle is to be able to compute an over-approximation precise enough that does not intersect Bad i.e. a conclusive approximation. This notion of precision is often defined by a very technical parameter of techniques implementing this over-approximation approach. In this paper, we propose a new characterization of conclusive approximations by logical formulae generated from a new kind of automata called symbolic tree automata. Solving a such formula leads automatically to a conclusive approximation without extra technical parameters.
Type de document :
Communication dans un congrès
Giorgio Delzanno and Igor Potapov. Reachability Problems 2011, Sep 2011, Gênes, Italy. LNCS 6945, 2011, Reachability Problems (RP 2011)
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00606100
Contributeur : Yohan Boichut <>
Soumis le : mardi 5 juillet 2011 - 13:47:42
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 12 novembre 2012 - 10:10:17

Fichier

main.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00606100, version 1

Citation

Yohan Boichut, Thi-Bich-Hanh Dao, Valérie Murat. Characterizing Conclusive Approximations by Logical Formulae. Giorgio Delzanno and Igor Potapov. Reachability Problems 2011, Sep 2011, Gênes, Italy. LNCS 6945, 2011, Reachability Problems (RP 2011). 〈inria-00606100〉

Partager

Métriques

Consultations de la notice

360

Téléchargements de fichiers

90