[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Translational Symmetry for Model Checking



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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ad1c98a5-728c-4d3c-a077-ea7040f34e9dn%40googlegroups.com.