A formula P \text{ is true} \equiv \neg P \text{ is unsatisfiable}.
For example, x + 1 > x is always true, which means we cannot find x that satisfies x + 1 \leq x.
Given a transition system \mathcal{T} = (S, I, T) and a safety property P, our goal is to check the property G:
G = I(s_0) \wedge \Big( \bigwedge_{i=0}^{k-1}T(s_i, s_{i+1}) \Big) \wedge \Big( \bigvee_{j=0}^k \neg P(s_j) \Big)
When k = 0, G = I(s_0) \wedge \neg P(s_0).
When k = 1, G = I(s_0) \wedge T(s_0, s_1) \wedge (\neg P(s_0) \vee \neg P(s_1)).
When k = 2, G = I(s_0) \wedge T(s_0, s_1) \wedge T(s_1, s_2) \wedge (\neg P(s_0) \vee \neg P(s_1) \vee \neg P(s_2)).
\cdots
This is k-bounded model checking.