Skip to Main content Skip to Navigation
Conference papers

Tree automata with equality constraints modulo equational theories

Florent Jacquemard 1 Michael Rusinowitch 2 Laurent Vigneron 2
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Florent Jacquemard Connect in order to contact the contributor
Submitted on : Tuesday, March 22, 2011 - 11:01:55 PM
Last modification on : Friday, January 21, 2022 - 3:08:33 AM
Long-term archiving on: : Thursday, June 23, 2011 - 2:59:16 AM


Files produced by the author(s)



Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron. Tree automata with equality constraints modulo equational theories. 3d International Joint Conference on Automated Reasoning (IJCAR), Aug 2006, Seattle, United States. pp.557-571, ⟨10.1007/11814771_45⟩. ⟨inria-00579011⟩



Les métriques sont temporairement indisponibles