Tree automata with equality constraints modulo equational theories

Florent Jacquemard 1 Michael 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, 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. 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.
Type de document :
Article dans une revue
Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pp.182-208. 〈10.1016/j.jlap.2007.10.006〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00329693
Contributeur : Michaël Rusinowitch <>
Soumis le : lundi 13 octobre 2008 - 11:27:35
Dernière modification le : jeudi 15 février 2018 - 08:48:09
Document(s) archivé(s) le : lundi 7 juin 2010 - 19:30:48

Fichier

JacquemardRusinowitchVigneron-...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron. Tree automata with equality constraints modulo equational theories. Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pp.182-208. 〈10.1016/j.jlap.2007.10.006〉. 〈inria-00329693〉

Partager

Métriques

Consultations de la notice

289

Téléchargements de fichiers

140