3 ms·
Model checking is a proof method. If all possible states are explored, that is a pfoof (Proof by exhaustion).
by avodonosov 8y ago
Model checking is a proof method. If all possible states are explored, that is a pfoof (Proof by exhaustion).
- pron 8y agoIt's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state cases, verified propositions are about infinite behaviors; you often model-check propositions much more elaborate than "X never happens in any state"), and algorithms like DPLL for SAT model-checking don't even do explicit state visits. Rather, it is a proof in the model theory of the logic.