Skip to Main content Skip to Navigation
Reports

Tree Automata with Equality Constraints Modulo Equational Theories

Florent Jacquemard 1 Michaël Rusinowitch 2 Laurent Vigneron 2
1 SECSI - Security of information systems
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
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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Keywords : first order theorem proving tree automata basic paramodulation splitting verification of infinite state systems
Document type :
Reports
Complete list of metadatas
https://hal.inria.fr/inria-00071215
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 2:40:11 PM
Last modification on : Thursday, November 12, 2020 - 9:42:09 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:01:30 PM

Files

Vignette du document
RR-5754.pdf

Identifiers

  • HAL Id : inria-00071215, version 1

Collections

INRIA | INRIA-RRRT | CNRS | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | ENS-CACHAN | LARA | LORIA | UNIV-LORRAINE

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

277

Files downloads

270

 

Contact                    Legal Notice                    Personal Data