TY - GEN
T1 - Effectively checking the finite variant property
AU - Escobar, Santiago
AU - Meseguer, José
AU - Sasse, Ralf
N1 - S. Escobar has been partially supported by the EU (FEDER) and the Spanish MEC under grant TIN2007-68093-C02-02, and Integrated Action HA 2006-0007. J. Meseguer and R. Sasse have been partially supported by the ONR Grant N00014-02-1-0715, and by the NSF Grants IIS 07-20482 and CNS 07-16638.
PY - 2008
Y1 - 2008
N2 - 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,..., tn} of → Δ,B -normalized instances of t so that any instance of t normalizes to an instance of some ti 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.
AB - 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,..., tn} of → Δ,B -normalized instances of t so that any instance of t normalizes to an instance of some ti 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.
UR - https://www.scopus.com/pages/publications/48949107143
UR - https://www.scopus.com/pages/publications/48949107143#tab=citedBy
U2 - 10.1007/978-3-540-70590-1_6
DO - 10.1007/978-3-540-70590-1_6
M3 - Conference contribution
AN - SCOPUS:48949107143
SN - 3540705880
SN - 9783540705888
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 79
EP - 93
BT - Rewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
T2 - 19th International Conference on Rewriting Techniques and Applications, RTA 2008
Y2 - 15 July 2008 through 17 July 2008
ER -