LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that this class has a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodu- lation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.
https://hal.inria.fr/inria-00579011
Contributeur : Florent Jacquemard
<>
Soumis le : mardi 22 mars 2011 - 23:01:55
Dernière modification le : jeudi 15 février 2018 - 08:48:09
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:59:16
Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron. Tree automata with equality constraints modulo equational theories. Ulrich Furbach and Natarajan Shankar. 3d International Joint Conference on Automated Reasoning (IJCAR), Aug 2006, Seattle, United States. Springer, 4130, pp.557-571, 2006, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/j354023699610786/〉. 〈10.1007/11814771_45〉. 〈inria-00579011〉
