Monday, August 18, 2003

Better verification through symmetry Symmetry is preserved when process IDs are only tested for equality as members of an unordered set.

The number of processes in a given state matters, not the order in which processes appear in a given state. So that state 0,1 is identical to state 1,0. (if that state of process A is first and the state of process B is second in the pair A,B). The new problem is determining if two states are members of the same symmetry class. This is done by canonicalization. A canonicalization function returns the same result (namely, the canonical state) for all members of the same class.

So what does it mean for our heuristic? Our cost function should return the same cost for states in the same class. It means we need to find out if we are computing the cost before or after canonicalization.

No comments: