Based on Mitch's presentation yesterday, traversal automata (TA) are useful
to reason about traversals. We could build tools to check
TA for equivalence.

One of the insights of the compilation of strategies was that
we must have state-passing methods. If we restrict ourselves
to parameter-less methods we can experience an exponential
explosion in the number of generated traversal methods.

TA are of this state-passing nature. As we discussed in the seminar,
we can take a strategy and a class graph and produce an
equivalent TA. The traversal graph defined in the paper with Boaz
seems to contain quite explicitly the state-transition information
for the TA.

Equivalence checking of TA seems to have an efficient
algorithm since equivalence of finite automata is of order
O(n*G(n)) where G(n) < 5 for all practical purposes.
The algorithm uses the Union-Find data structure with path compression.
That is what I learned when I was in graduate school.
Now there are even better techniques, so called BDD techniques,
to operate on finite automata.

Given strategy, class graph pairs (S1,G1) and (S2,G2), we may want
to know whether they define identical traversals.
And a TA equivalence checker would allow us to answer such questions.

Is someone interested in exploring algorithms for equivalence checking of
traversal specifications? 

-- Karl