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
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00578896
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 3:57:23 PM
Last modification on : Thursday, February 7, 2019 - 5:29:22 PM
Long-term archiving on : Saturday, December 3, 2016 - 7:45:54 AM

File

tosca.pdf
Files produced by the author(s)

Identifiers

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. Theory of Security and Applications (TOSCA, joint workshop affiliated to ETAPS), Mar 2011, Saarbrücken, Germany. pp.166-185, ⟨10.1007/978-3-642-27375-9⟩. ⟨inria-00578896⟩

Share

Metrics

Record views

514

Files downloads

225