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}, }