6 ms·
Exhaustive search across all states and state transitions. There's a distributed version which helps with especially large state spaces. Combinatorial explosion
by ahelwer 11y ago
Exhaustive search across all states and state transitions. There's a distributed version which helps with especially large state spaces. Combinatorial explosion is an issue. In some cases the best/only option is to formally prove correctness with the built-in proof language; the model checker works well in tandem, for quickly checking assertions before putting effort into a proof.
Generally the model checker alone works just fine, though.
- pja 11y agoYeah, it’s exhaustive search. Fortunately storage costs have dropped like a rock over the last few decades, so problems that were hilariously impractical only a few years ago are now checkable on commodity hardware. A fully interlinked (ie guaranteed symmetric inter-node bandwidth) cluster on Amazon EC2 with aggregate memory (even before you start touching secondary storage) in the Terabytes can be rented for a few 10s of $ an hour at spot prices. It may be that Formal Methods time has finally come!