Reachability analysis of Term Rewriting Systems
What is a Term?
The most usual terms we all know are arithmetic expressions built
on operators (or symbols) +, *,  , on numbers and on variables x, y, z,
etc. For instance, 1+2 is a term, (x+y)*2 is a term, (x+y) is a term and
it is a subterm of (x+y)*2 .
What are Term Rewriting Systems?
A Term Rewriting System is a set of rewrite rules, i.e.
transformation rules on terms. For instance, x+0 > x is a rewrite rule.
Applying this rule to the term (1+0)+(0+0), can be done in the following
way:
(1+0)+(0+0) > 1 + (0 + 0)
where the rule x+0 > x has been applied on the subterm (1+0)
of (1+0)+(0+0), and the variable x has taken the value 1. Replacing x by
1 in the rule x+0 > x, we obtain the instanciated rule 1+0 > 1 meaning
that we can replace subterm 1+0 by 1, hence thus:
(1+0)+(0+0) > 1 + (0 + 0)
Similarly 1+(0+0) can be rewritten, and so on, until we get 1 which
cannot be rewritten. It is a normal form.
(1+0)+(0+0) > 1 + (0 + 0) > 1 + 0 > 1
Note that there is in fact another way to rewrite (1+0)+(0+0), where
we first rewrite the second subterm (0+0):
(1+0)+(0+0) > (1 + 0) + 0 > 1 + 0 > 1
What are reachable terms (or descendants)?
From term (1+0)+(0+0), with the term rewriting system R={x+0
> x}, the set of reachable terms R*( (1+0)+(0+0) ) is equal to:

(1 + 0)+(0 + 0)

1 + (0 + 0)

(1 + 0) + 0

1 + 0

1
It is, in fact, the set of terms that can be obtained by rewriting (1 +
0) + (0 + 0) zero or more times. Note that when the term rewriting system
is not terminating, the set of reachable terms may be infinite. For instance,
with the system R={x+0 > (x+0)+0} on the initial term 1 + 0 the
set of reachable terms becomes:

1 + 0

(1 + 0) + 0

((1 + 0) + 0) + 0

...
What is reachability analysis on term rewriting
systems?
Given a Tern Rewriting System R and two terms s and t,
reachability analysis consists in proving that, either

t is reachable from s with R, i.e. t is in
R*(s),
or

t is not reachable from s with R, i.e. t is
not in R*(t).
When the term rewriting system is not terminating, the set of reachable
terms is infinite,. In that case, for computing the set of reachable terms,
we need some special algorithms and data structures (tree
automata) for representing, finitely, infintely many reachable
terms.
Why reachability analysis on Term Rewriting Systems
well adapted for program verification?

Term rewriting systems are a very simple and powerful tool
for modeling programs, protocols, processors, at various level of precision
(see [1,2] and examples on cryptographic protocols here).
On the modeled systems, reachability analysis permits thus to check that
an event will occur (i.e. it is reachable) or that an event will never
occur (i.e. it is not reachable)[1,2].

Reachability analysis on term rewriting systems can deal with infinite
state systems.

Reachability analysis on Term Rewriting Systems is semiautomatic [2,3,4,5].
Reachability analysis and the Timbuk tool are currently used for
verifying cryptographic protocols
and verifying Java applications.
How to experiment?
The Timbuk software
implements term rewriting systems, tree automata and reachability analysis.
See Timbuk documentation for user manual
and tutorial.
Our publications on reachability analysis
[1] (zipped
or not)
T. Genet.
Decidable approximations of sets of descendants and sets of
normal forms. In T. Nipkow, editor, Proceedings 9th International
Conference on Rewriting Techniques and Applications, Tsukuba (Japan),
volume 1379 of Lecture Notes in Computer Science, pages 151165.
SpringerVerlag, 1998.
[2] (gzipped
or not)
T. Genet and V. Viet Triem Tong.
Reachability Analysis of Term Rewriting
Systems with Timbuk. In Proceedings 8th International Conference
on Logic for Programming, Artificial Intelligence, and Reasoning, Havana
(Cuba), volume 2250 of Lecture Notes in Artificial Intelligence.
SpringerVerlag, 2001.

[3] (gzipped)

G. Feuillade, T. Genet and V. Viet Triem Tong.
Reachability Analysis
over Term Rewriting Systems. In Journal of Automated Reasonning.
2004. Volume 33 (34). 2004.

[4] (pdf)

T. Genet and V. Rusu.
Equational Tree Automata
Completion. In Journal of Symbolic Computation.
Volume 45. Elsevier, 2010.

[5] (pdf)

T. Genet.
Reachability analysis of rewriting for
software verification. Habilitation à diriger des recherches, Université de
Rennes 1, 2009.