Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Effectively Checking the Finite Variant Property
verfasst von : Santiago Escobar, José Meseguer, Ralf Sasse
Erschienen in: Rewriting Techniques and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
An equational theory decomposed into a set
B
of equational axioms and a set
Δ
of rewrite rules has the
finite variant
(FV)
property
in the sense of Comon-Lundh and Delaune iff for each term
t
there is a finite set {
t
1
,...,
t
n
} of →
Δ
,
B
-normalized instances of
t
so that any instance of
t
normalizes to an instance of some
t
i
modulo
B
. This is a very useful property for cryptographic protocol analysis, and for solving both unification and disunification problems. Yet, at present the property has to be established by hand, giving a separate mathematical proof for each given theory: no checking algorithms seem to be known. In this paper we give both a necessary and a sufficient condition for FV from which we derive an algorithm ensuring the sufficient condition, and thus FV. This algorithm can check automatically a number of examples of FV known in the literature.