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
Rapport (Rapport De Recherche) Année : 2005

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. 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.
Fichier principal
Vignette du fichier
RR-5754.pdf (518.24 Ko) Télécharger le fichier

Dates et versions

inria-00071215 , version 1 (23-05-2006)

Identifiants

  • HAL Id : inria-00071215 , version 1

Citer

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron. Tree Automata with Equality Constraints Modulo Equational Theories. [Research Report] RR-5754, INRIA. 2005, pp.27. ⟨inria-00071215⟩
83 Consultations
111 Téléchargements

Partager

Gmail Facebook X LinkedIn More