Skip to Main content Skip to Navigation
Reports

Unification in Non-Disjoint Combinations with Forward-Closed Theories

Résumé : On étudie le problème d’unification dans les théories définies par des systèmes de réécriture qui sont à la fois convergents et fermés en avant. Ces théories sont connues dans le contexte de l’analyse de protocoles de sécurité comme les théories ayant la propriété des variants finis et admettant de ce fait un algorithme d’unification à base de variants. Dans ce papier, on présente un nouvel algorithme d’unification à base de règles qui peut être vu comme une alternative à l’approche basée sur le calcul de variants. On étudie l’union d’un système de réécriture convergent et fermé en avant avec une autre théorie dont les symboles de fonction peuvent apparaître dans les membres droits du système de réécriture. Finalement, on présente un algorithme de combinaison pour cette classe particulière d’unions non-disjointes de théories.
Document type :
Reports
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-02006179
Contributor : Christophe Ringeissen <>
Submitted on : Monday, February 4, 2019 - 2:33:48 PM
Last modification on : Thursday, August 8, 2019 - 4:04:07 PM
Document(s) archivé(s) le : Sunday, May 5, 2019 - 3:19:41 PM

File

RR-9252.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02006179, version 1

Citation

Ajay Eeralla, Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Unification in Non-Disjoint Combinations with Forward-Closed Theories. [Research Report] RR-9252, Inria Nancy - Grand Est. 2019. ⟨hal-02006179⟩

Share

Metrics

Record views

100

Files downloads

125