| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Tree automata with equality constraints modulo equational theories
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.
Cited literature [22 references]
https://hal.inria.fr/inria-00579011
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:01:55 PM
Last modification on : Thursday, July 2, 2020 - 5:26:03 PM
Document(s) archivé(s) le : Thursday, June 23, 2011 - 2:59:16 AM
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:01:55 PM
Last modification on : Thursday, July 2, 2020 - 5:26:03 PM
Document(s) archivé(s) le : Thursday, June 23, 2011 - 2:59:16 AM
File
rr-lsv-2006-07.pdf
Files produced by the author(s)