Is anyone familiar with any prior work on exploiting types of "translational" symmetry during model checking? For protocols that maintain, say, a counter, it often seems that the safety of the protocol is, to some extent, "translation invariant". That is, if the set of states reachable from a state <<counter, v1, ..., vn>> is safe, then the set of states reachable from <<counter + T, v1, ..., vn>> for T > 0 should also be safe, assuming that the safety property and algorithm behavior doesn't depend on the specific (i.e. concrete) value of the counter. The closest mention of it that I've encountered is in Section 3.5 of [1], where it discusses "Symmetry Under Time Translation" in the context of model checking real time specifications.
I imagine you may be able to implement something like this using a clever VIEW _expression_ in TLC.