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
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. 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 (embedding the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. We sketch an application of these tree automata classes to the reachability problem for a fragment of the applied pi-calculus.
https://hal.inria.fr/inria-00071215 Contributor : Rapport de Recherche InriaConnect in order to contact the contributor Submitted on : Tuesday, May 23, 2006 - 2:40:11 PM Last modification on : Friday, January 21, 2022 - 3:09:04 AM Long-term archiving on: : Sunday, April 4, 2010 - 10:01:30 PM