[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Translational Symmetry for Model Checking
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
On Wednesday, June 16, 2021 at 8:44:09 PM UTC-4 will...@xxxxxxxxx wrote:
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.
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/75f4d42c-c0c5-42db-97bf-e18a87253451n%40googlegroups.com.