On Asymmetric Unification and the Combination Problem in Disjoint Theories

Autor: Deepak Kapur, Paliath Narendran, Serdar Erbatur, Andrew M. Marshall, Catherine Meadows, Christophe Ringeissen
Přispěvatelé: Department of Computer Science [Verona] (UNIVR | DI), University of Verona (UNIVR), The University of New Mexico [Albuquerque], Naval Research Laboratory (NRL), University at Albany [SUNY], State University of New York (SUNY), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Università degli studi di Verona = University of Verona (UNIVR), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Jazyk: angličtina
Rok vydání: 2014
Předmět:
Physics::General Physics
Unification
Modulo
0102 computer and information sciences
02 engineering and technology
Disjoint sets
Cryptographic protocol analysis
01 natural sciences
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
0202 electrical engineering
electronic engineering
information engineering
Mathematics
Discrete mathematics
High Energy Physics::Phenomenology
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing)
State (functional analysis)
16. Peace & justice
combination method
Free abelian group
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
Computer Science::Programming Languages
Irreducibility
020201 artificial intelligence & image processing
equational theories
Combination method
Asymmetric unification
Zdroj: Foundations of Software Science and Computation Structures-17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS
Foundations of Software Science and Computation Structures-17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Apr 2014, Grenoble, France. pp.15, ⟨10.1007/978-3-642-54830-7_18⟩
Lecture Notes in Computer Science ISBN: 9783642548291
FoSSaCS
DOI: 10.1007/978-3-642-54830-7_18⟩
Popis: International audience; Asymmetric unification is a new paradigm for unification modulo theories that introduces irreducibility constraintson one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis, for which itis often necessary to put irreducibility constraints on portions of a state. However many facets of asymmetricunification thatare of particular interest, includingits behavior under combinations of disjoint theories, remain poorly understood.In this paper we give a new formulation of the method for unificationin the combination of disjoint equational theories developed by Baader and Schulz that bothgives additional insights into the disjoint combination problem in general, and furthermore allowsus to extend the method to asymmetric unification, giving the first unification method for asymmetric unification in the combination of disjoint theories.
Databáze: OpenAIRE
Externí odkaz: