Bounded Model Checking Encoding

See appendix for credits.

Bounded Model Checking (BMC) is a SAT-based technique, distinguished from symbolic model checking. It converts model checking problem into satisfiability problem. BMC tends to look for counter-examples by progressively increasing an integer bound, which is the number of steps in a path. Yes, once you verified there are no counter-examples within the bound $k$, it doesn't prove $M \models f$ at all. BMC is useful in troubleshooting, to capture the flaws in the model design.

The bridge

Given a Kripke model $M$, a LTL formula $f$ and a bound $k$,

$M \models_k \mathbf{E}f$ iff ⟦$M$,$f$⟧$_k$ is satisfiable.

$\models_k$ means the property is verified in the path of $k$ steps. ⟦$M$,$f$⟧$_k$ is defined as follows,

Fig. 1 The encoding of ⟦$M$,$f$⟧$_k$ in BMC

(1) divides the denotion into the model part (2) and the property part (3). (2) shows the execution of $M$ in $k$ steps, by providing the initial state ($s_0$ is a vector of boolean variables that are assigned in such state) and transition relations of each step. (3) also consists of two portions that disjunct. The first portion says there are no loops at $s_k$ to all former states (negation of transition relation from $s_k$ to $s_{k-1}$,..., $s_0$). The second one is with loops.

Fig. 2 The paths with and without loop

We do need to separate the encodings (i.e. ⟦$f$⟧$^i_k$, $_l$⟦$f$⟧$^i_k$). For instance, only the finite path carrying a loop can verify the properties like $\mathbf{G}p$. We need to describe properties in different manner according to the existence of a loop. Here is the formal chart,

Fig. 3 ⟦$f$⟧$^i_k$ and $_l$⟦$f$⟧$^i_k$ unfolded alongside their LTL correspondence

The above is a recursive definition. The indices $i$, $k$, $l$ say respectively the current state, the integer bound, the loop point (there is an edge from $s_k$ back to $s_l$). The base case $p$, an atom, matches $p_i$ which is the assignment of $p$ at the state $s_i$. The negation is thereby defined. The loop doesn't matter for these two since we only consider an atom in the current state. The disjunction and conjunction are defined recursively. Before going further, we shall see this figure,

Fig. 4 The loop case

$\mathbf{X}g$ parallels a conditional branch definition. In the loop-less case, when $i < k$, the current state is before the bound state, then there is a next state for $s_i$. Otherwise false. Similar in the loop case, but when $i = k$, since there is a loop from $s_k$ to $s_l$, the next state exists. Think there is no $i > k$, when it loops back, $k+1$ becomes $l$, so everything is still within the bound $k$.

$\mathbf{G}g$ is simply false in the loop-less case, always UNSAT. If there is a loop, we need to make sure every state (hence as a big conjunction) with in the loop verifies $g$ and also the relays from the current state $s_i$ to the loop point $s_l$ in case of $i < l$.

$\mathbf{F}g$ is straight-forward, regarding the fact that we'd like at least one $g$ on such path (both loop-less and with loop), so a big disjunction is used.

Recall that $h \mathbf{U} g$ means $h$ remains true till $g$ becomes true. So in the loop-less case, it compares to the disjunction (satisfiable at least one of the components is true) of all possible captures, e.g., $g_i$, $h_ig_{i+1}$, $h_ih_{i+1}g_{i+2}$, ..., etc. Similar for $h \mathbf{R} g$, which says the advent of the truth of $h$ releases $g$ from being always true. That said, $g$ wasn't free (being true always) before $h$ gets its truth.

The situation becomes much more complex in the loop case for these two. If $i < l$, then it gets the part similar to the loop-less one, $$ \bigvee_{j=i}^k \bigg( {}_l\llbracket \; g \; \lrbracket_k^j \wedge \bigwedge_{n=i}^{j-1} {}_l \llbracket \; h \; \lrbracket ^n_k \bigg)$$ It is accompanied by the case that $i > l$, the idea is the property shall be verified from $s_i$ to $s_k$, then from $s_l$ to $s_{i-1}$ since there is loop $(s_k, s_l)$. So we have, $$ \bigvee_{j=l}^{i-1} \bigg( {}_l\llbracket \; g \; \lrbracket_k^j \wedge \bigwedge_{n=i}^{k} {}_l \llbracket \; h \; \lrbracket ^n_k \wedge \bigwedge_{n=l}^{j-1} {}_l\llbracket \; h \; \lrbracket_k^n \bigg)$$

The last one can be accordingly rendered.

References

• R. Sebastiani, SAT-based Bounded Model Checking, slides on Formal Methods, 2012, link
• A. Biere et al, Bounded Model Checking, Vol. 58, Advances in Computers, 2003, pdf

---

Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.