Translational Symmetry for Model Checking

[Willy Schultz]

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.

[1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/charme2005.pdf

[Andrew Helwer]

Yes, see my prior thread here: https://groups.google.com/g/tlaplus/c/JZaBcIhA1UY/m/olfrUJ5xCQAJ

And Leslie's paper Real Time is Really Simple, which you found.

You are correct it is implemented with the VIEW expression, assuming your counter values don't "contaminate" any of the other variable's values.

Andrew

[Willy Schultz]

Thanks, that thread is helpful! I was thinking about it in the context of distributed protocols that utilize various types of logical version numbers. One thought was to define a VIEW function that looks at all version values in the current state, and shifts them all downward so the smallest version in that state is sent to zero e.g.

View(1,1,1) == (0,0,0) 

View(1,2,1) == (0,1,0)

View(1,2,4) == (0,1,3) 

I attached a simple experiment of this for a toy quorum based election protocol based on monotonically increasing terms/epochs. The VIEW expression in TLA+ is written as:

MinTerm == Min(Range(currentTerm))

currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]

View == <<currentTermsShifted, state>>

where currentTerm is variable that maps from server identifiers to natural numbers. 

Without the view expression and setting a state constraint of MaxTerm=10, TLC finds 631 reachable states for the SimpleElection spec and attached config. With the VIEW expression enabled it finds 118 reachable states. For a MaxTerm=20 it finds 2461 states without the view, and 238 states with the view. For a MaxTerm=50 it finds 15151 states without the view and 598 states with it. I wonder if this approach would help reduce model checking burden for some real world specs, or if the gains in most cases wouldn't be significant enough to warrant it.

I suppose it may be sound in some cases to abstract further and have the view expression only look at the ordering relationships between counter values in a state. This seems like a kind of manual predicate abstraction i.e. if a protocol only depends on the fact that one value is <,>,= another, but doesn't care about the concrete values. This seems to echo some of Ron's comments in the linked thread.

Will

[Andrew Helwer]

One interesting thing Leslie talks about a lot in Real Time (and somewhat mentioned in the other thread) is that these sorts of VIEW functions have model checking correctness implications. I wonder whether there is some general way of writing & testing a refinement relation to ensure that reducing all the counters modulo some number maintains all the important invariants of your spec, and no valid behaviors are accidentally removed.

Andrew