Tree automata with equality constraints modulo equational theories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Logic and Algebraic Programming Année : 2008

Tree automata with equality constraints modulo equational theories

Résumé

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.
Fichier principal
Vignette du fichier
JacquemardRusinowitchVigneron-JLAP.pdf (339.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00329693 , version 1 (13-10-2008)

Identifiants

Citer

Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron. Tree automata with equality constraints modulo equational theories. Journal of Logic and Algebraic Programming, 2008, 75 (2), pp.182-208. ⟨10.1016/j.jlap.2007.10.006⟩. ⟨inria-00329693⟩
136 Consultations
173 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More