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 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 151-165. Springer-Verlag, 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. Springer-Verlag, 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 (3-4). 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.