A. Armando, R. Carbone, and L. Compagna, Ltl model checking for security protocols, CSF, pp.385-396, 2007.

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

E. Balland, Y. Boichut, T. Genet, and P. Moreau, Towards an Efficient Implementation of Tree Automata Completion, AMAST, pp.67-82, 2008.
DOI : 10.1007/978-3-540-79980-1_6
URL : https://hal.archives-ouvertes.fr/inria-00304010

B. Bogaert and S. Tison, Equality and disequality constraints on direct subterms in tree automata, STACS, pp.161-171, 1992.
DOI : 10.1007/3-540-55210-3_181

Y. Boichut, R. Courbis, P. Héam, and O. Kouchnarenko, Finer Is Better: Abstraction Refinement for Rewriting Approximations, Rewriting Techniques and Application, RTA'08, pp.48-62, 2008.
DOI : 10.1007/978-3-540-70590-1_4
URL : https://hal.archives-ouvertes.fr/hal-00563422

Y. Boichut, . Th, . Genet, . Th, L. L. Jensen et al., Rewriting Approximations for Fast Prototyping of Static Analyzers, Rewriting Techniques and Applications, RTA'07, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6
URL : https://hal.archives-ouvertes.fr/hal-00463418

Y. Boichut, P. Héam, and O. Kouchnarenko, Approximation-based tree regular model-checking, Nordic Journal of Computing, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00429345

E. M. Clarke, Counterexample-guided abstraction refinement, TIME-ICTL, page 7, 2003.

H. Comon and V. Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science (TCS'05, p.331, 2005.
DOI : 10.1016/j.tcs.2004.09.036
URL : https://hal.archives-ouvertes.fr/inria-00000553

J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. P?s?reanu et al., Bandera, Proceedings of the 22nd international conference on Software engineering , ICSE '00, pp.439-448, 2000.
DOI : 10.1145/337180.337234

M. Dauchet, A. Caron, and J. Coquidé, Automata for Reduction Properties Solving, Journal of Symbolic Computation, vol.20, issue.2, pp.215-233, 1995.
DOI : 10.1006/jsco.1995.1048

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pp.244-320, 1990.

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Property specification patterns for finite-state verification, Proceedings of the Second Workshop on Formal Methods in Software Practice, pp.7-15, 1998.

S. Escobar and J. Meseguer, Symbolic Model Checking of Infinite-State Systems Using Narrowing, Rewriting Techniques and Applications, RTA'07, pp.153-168, 2007.
DOI : 10.1007/978-3-540-73449-9_13

G. Feuillade, . Th, V. Genet, and . Viettriemtong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

E. Filiot, J. Talbot, and S. Tison, Tree automata with global constraints, Developments in Language Theory, pp.314-326, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00292027

. Th, F. Genet, and . Klay, Rewriting for Cryptographic Protocol Verification, Conference on Automated Deduction, pp.271-290, 2000.

R. Gilleron and S. Tison, Regular tree languages and rewrite systems, Fundamenta Informatica, vol.24, issue.12, pp.157-174, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00538882

P. Gyenizse and S. Vágvölgyi, Linear generalized semi-monadic rewrite systems effectively preserve recognizability, Theoretical Computer Science, vol.194, issue.1-2, pp.87-122, 1998.
DOI : 10.1016/S0304-3975(96)00333-7

K. Havelund, . Th, and . Pressburger, Model checking JAVA programs using JAVA PathFinder, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, pp.366-381, 2000.
DOI : 10.1007/s100090050043

F. Jacquemard, Decidable approximations of term rewriting systems, Rewriting Techniques and Applications, RTA'96, pp.362-376, 1996.
DOI : 10.1007/3-540-61464-8_65

F. Jacquemard, M. Rusinowitch, and L. Vigneron, Tree automata with equality constraints modulo equational theories, IJCAR, pp.557-571, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00579011

W. Karianto, . Ch, and . Löding, Unranked Tree Automata with Sibling Equalities and Disequalities, ICALP, pp.875-887, 2007.
DOI : 10.1007/978-3-540-73420-8_75

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. SV, 1992.
DOI : 10.1007/978-1-4612-0931-7

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

J. Meseguer, The temporal logic of rewriting, 2007.

J. Meseguer, The temporal logic of rewriting: A gentle introduction. Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, pp.354-382, 2008.

H. Ohsaki and T. Takai, ACTAS : A System Design for Associative and Commutative Tree Automata Theory, Electronic Notes in Theoretical Computer Science, vol.124, issue.1, pp.97-111, 2005.
DOI : 10.1016/j.entcs.2004.07.017

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

H. Seidl, . Th, A. Schwentick, P. Muscholl, and . Habermehl, Counting in Trees for Free, ICALP, pp.1136-1149, 2004.
DOI : 10.1007/978-3-540-27836-8_94
URL : https://hal.archives-ouvertes.fr/hal-00159525

T. Takai, Y. Kaji, and H. Seki, Right-Linear Finite Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, proceedings of RTA, 2000.
DOI : 10.1007/10721975_17