Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: How to get rid of some algebraic properties. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), pp. 294–307, Lecture Notes in Computer Science 3467, Springer, Nara, Japan, April 2005.
We consider the following problem: Given a term \(t\), a rewrite system \(\mathcalR\), a finite set of equations \(E'\) such that \(\mathcalR\) is convergent modulo \(E'\), compute finitely many instances of \(t\): \(t_1,łdots,t_n\) such that, for every substitution \(\sigma\), there is an index \(i\) and a substitution \(\theta\) such that \( t\sigma\mathord\downarrow=_E' t_i\theta\) (where \(t\sigma\mathord\downarrow\) is the normal form of \(t\sigma\) w.r.t. \(\mathcalR/E'\)).
The goal of this paper is to give equivalent (resp. sufficient) conditions for the finite variant property and to systematically investigate this property for equational theories, which are relevant to security protocols verification. For instance, we prove that the finite variant property holds for Abelian Groups, and a theory of modular exponentiation and does not hold for the theory ACUNh (Associativity, Commutativity, Unit, Nilpotence, homomorphism).
@inproceedings{ComDel-rta2005,
abstract = {We consider the following problem: Given a term
\(t\), a rewrite system \(\mathcal{R}\), a finite set
of equations \(E'\) such that \(\mathcal{R}\) is
convergent modulo~\(E'\), compute finitely many
instances of~\(t\): \(t_1,\ldots,t_n\) such that, for
every substitution~\(\sigma\), there is an index
\(i\) and a substitution~\(\theta\) such that \(
t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where
\(t\sigma\mathord{\downarrow}\) is the normal form of
\(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par The goal
of this paper is to give equivalent (resp.
sufficient) conditions for the finite variant
property and to systematically investigate this
property for equational theories, which are relevant
to security protocols verification. For instance, we
prove that the finite variant property holds for
Abelian Groups, and a theory of modular
exponentiation and does not hold for the
theory~\textit{ACUNh} (Associativity, Commutativity,
Unit, Nilpotence, homomorphism).},
address = {Nara, Japan},
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {R}ewriting {T}echniques and
{A}pplications ({RTA}'05)},
OPTDOI = {10.1007/b135673},
editor = {Giesl, J{\"u}rgen},
month = apr,
pages = {294-307},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {The finite variant property: {H}ow to get rid of some
algebraic properties},
volume = {3467},
year = {2005},
acceptrate = {31/79},
acronym = {{RTA}'05},
nmonth = {4},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}