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:

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:

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

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?

Reachability analysis and the Timbuk tool are currently used for verifying cryptographic protocols, verifying Java applications, and verifying higher-order functional programs.

How to experiment?

The Timbuk software implements term rewriting systems, tree automata and reachability analysis.