[xhgdvjky]

if the checker can prove that the state of A is not important to B, then it can check them independently.

this is the biggest difference between relatively naive checkers like tla+ and your brain. you don't think about all the states at the same time. I do not of a model checker that does this.

symmetry was kind of explained by the other commenter. in short, you often have sets of things that have the same allowable states, and the order of these items is irrelevant. e.g. you have several worker nodes... they have state, but if two of them instantly swap states, it's possible that nothing really changed