Sciweavers

Share
CADE
2006
Springer

Tree Automata with Equality Constraints Modulo Equational Theories

9 years 9 months ago
Tree Automata with Equality Constraints Modulo Equational Theories
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.
Florent Jacquemard, Laurent Vigneron, Michaël
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Florent Jacquemard, Laurent Vigneron, Michaël Rusinowitch
Comments (0)
books