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 semi-automatic [2,3,4,5].

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.