Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus

Florent Jacquemard 1 Etienne Lozes 2 Ralf Treinen 3 Jules Villard 4
1 DAHU - Verification in databases
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
Abstract : We investigate the problem of deciding first-order theories of finite trees with several distinguished congruence relations, each of them given by some equational axioms. We give an automata-based solution for the case where the different equational axiom systems are linear and variable-disjoint (this includes the case where all axioms are ground), and where the logic does not permit to express tree relations x=f(y,z). We show that the problem is undecidable when these restrictions are relaxed. As motivation and application, we show how to translate the model-checking problem of Apil, a spatial equational logic for the applied pi-calculus, to the validity of first-order formulas in term algebras with multiple congruence relations.
Type de document :
Communication dans un congrès
Mdersheim, Sebastian and Palamidessi, Catuscia. Theory of Security and Applications (TOSCA, joint workshop affiliated to ETAPS), Mar 2011, Saarbrücken, Germany. Springer, 6993, pp.166-185, 2011, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/h77512586g626833/〉. 〈10.1007/978-3-642-27375-9〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00578896
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 15:57:23
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : samedi 3 décembre 2016 - 07:45:54

Fichier

tosca.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Florent Jacquemard, Etienne Lozes, Ralf Treinen, Jules Villard. Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus. Mdersheim, Sebastian and Palamidessi, Catuscia. Theory of Security and Applications (TOSCA, joint workshop affiliated to ETAPS), Mar 2011, Saarbrücken, Germany. Springer, 6993, pp.166-185, 2011, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/h77512586g626833/〉. 〈10.1007/978-3-642-27375-9〉. 〈inria-00578896〉

Partager

Métriques

Consultations de la notice

445

Téléchargements de fichiers

172