[tempguy9999]

Are there other systems where combinatorial explosions of states do not occur? Is there something in TLA that makes it prone to this where other model checkers perhaps aren't? Slightly related, isn't state space explosion an intrinsic part of any such problem?

If possible, could you explain what you mean by symmetry, and how it reduces state space (it's a big ask, I know).

sorry for the firehose of Q's! I'd really appreciate an expert's view though.

[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

[0815test]

Model checkers are essentially glorified fuzzers, so the way they work is inherently vulnerable to state space explosion. The way to address that is to move closer to building things that are correct "by construction", and prove them as such. Symmetry is one way of doing this, it allows you to "reduce" a whole lot of redundant checking to something much simpler, based on some underlying properties of what you're working with. A logical proof works much the same way, of course.

TLA specifications are typically "checked", or rather "fuzzed" by model checkers; this is not formally required (TLA+ even includes a proof language) but things tend to be done that way.

[tempguy9999]

Would whoever downvoted this please explain why so we can learn from it. Thanks.

[hwayne]

Not the downvoter, but:

- (Bounded) model checking is exhaustive, fuzzing is not. If your system successfully model checks, then no possible input can cause an error. Fuzzing is randomized, so there still _could_ be a bad input. That's why model checking is considered formal verification and fuzzing is not.

- Not all model checking is brute force searches. A lot of model checkers use SMT or SAT, so the check time grows slowly even with large state spaces.

- _Empirically speaking_, model-checking has scaled much better and been used for a wider range of applications than correct-by-construction has.

[0815test]

> (Bounded) model checking

Oh come on. If your bounded model checking is actually checking every possible input or program state, then it's not just a method of verification but an actual proof. (It may be a subjectively inelegant proof, but it's a proof nonetheless.) That much is obvious. What I clearly meant by "glorified fuzzing" was the far more common use of model checking in ways that stop short of this standard. That sort of use can still be nicely scalable, it does count as a formal method, and it can point out remarkably complex bugs in your system - but by definition, it cannot give any assurance that you're doing things correctly! That still requires proof.

[tempguy9999]

To put my oar in, and this is purely based on what I've read about spin, spin can verify 100% for 'small' models. If larger models are checked, it will run out of memory so you put it in a probabilistic mode which gives probabilistic assurances, still 'good' but less than 100%. In that respect I suppose it's degenerated to rather posh fuzzing.

I think the difference between small and large is down to how long you're prepared to let it run, but even more fundamentally, how much memory you can give it.

I'd agree that if the model matches the code and you successfully check the entire state space then it's a proof.