Skip to Main content Skip to Navigation
New interface
Conference papers

Characterizing Conclusive Approximations by Logical Formulae

Yohan Boichut 1 Thi-Bich-Hanh Dao 1 Valérie Murat 2, * 
* Corresponding author
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Yohan Boichut Connect in order to contact the contributor
Submitted on : Tuesday, July 5, 2011 - 1:47:42 PM
Last modification on : Saturday, June 25, 2022 - 10:11:32 AM
Long-term archiving on: : Monday, November 12, 2012 - 10:10:17 AM


Publisher files allowed on an open archive


  • HAL Id : inria-00606100, version 1


Yohan Boichut, Thi-Bich-Hanh Dao, Valérie Murat. Characterizing Conclusive Approximations by Logical Formulae. Reachability Problems 2011, Sep 2011, Gênes, Italy. ⟨inria-00606100⟩



Record views


Files downloads