Tree automata with equality constraints modulo equational theoriesReportar como inadecuado

Tree automata with equality constraints modulo equational theories - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 SECSI - Security of information systems 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 2 CASSIS - Combination of approaches to the security of infinite states systems 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 these classes have 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 paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.

Keywords : first order theorem proving tree automata basic paramodulation splitting verification of infinite state systems

Autor: Florent Jacquemard - Michael Rusinowitch - Laurent Vigneron -



Documentos relacionados