The set of initial states can be specified by a propositional
formula I(v) which holds for exactly those assignments to v
that correspond to initial states. Likewise, the transition
relation can be given by a propositional formula R(v, v´).
A path of length k starting in an initial state can be encoded
by means of the following formula:
36 circuit co-factoring,
37 But, the problem remains a topic of
active research. Meanwhile, an efficient way of finding
subtle counterexamples is still quite useful in debugging
path (k) = I (v0) Ù R (v0, v
1) Ù . . . Ù R (vk− 1,, vk).
The path ends in a cycle if and only if
cycle (k) = R (v k, v0) Ú . . . Ú R (vk, vk− 1) Ú R (v k, vk).
The property P is false in each of the k steps if and only if
property (k) = ¬ P (v0) Ù ¬ P (v
1) Ù . . . Ù ¬ P (vk).
2. 3. 4. The Abstraction Refinement Loop. This technique
uses counterexamples to refine an initial abstraction. We begin by defining what it means for one state-transition system
to be an abstraction of another. We write Ma = áSa , s0a, Ra , La ñ
to denote the abstraction of state-transition system M = áS, s0,
R, Lñ with respect to an abstraction mapping a. (Here we include the start states s0 and s0a as parts of the state-transition
systems.) We assume that the states of M are labeled with
atomic propositions from a set A of atomic propositions,
and that Ma is labeled with atomic propositions from a set
Aa that is a subset of A. We call M the concrete system and Ma
the abstract system.
Thus, the liveness property FP has a counterexample of
length k if and only if the conjunction W(k) of Formulas 1, 2,
and 3 is satisfiable.
W (k) = path (k) Ù cycle (k) Ù property (k).
Definition 1. A function a: S ® Sa is an abstraction mapping from the concrete system M to the abstract system Ma with
respect to the propositions in Aa if and only if
We start with k = 1. If the formula W(k) is satisfiable, we
know that FP has a counterexample of length k. A counterexample execution trace can be extracted from the satisfying assignment to W(k). If the formula W(k) is not satisfiable,
then it could be the case that either the temporal formula
FP holds on all paths starting from an initial state (and our
specification is true) or there is a counterexample that is
longer than k. When W(k) is unsatisfiable, we can do one of
two things: Either increase the value of k and look for longer counterexamples or stop if time or memory constraints
We note that the idea of checking safety properties such
as gP by reduction to propositional satisfiability is implicit
in the work of Kautz and Selman.
30 However, they do not
consider more general temporal properties such as the liveness property that we consider above.
In practice, BMC can often find counterexamples in
circuits with thousands of latches and inputs. Armin Biere
recently reported an example in which the circuit had 9510
latches and 9499 inputs. This resulted in a propositional formula with 4 × 106 variables and 1. 2 × 107 clauses. The shortest bug of length 37 was found in 69 seconds! Many others
have reported similar results.
Can BMC ever be used to prove correctness if no counterexamples are found? It is easy to see that for safety and
liveness properties of the form FP and gP where P is a
propositional formula, if there is a counterexample, then
there is one that is less than the diameter (i.e., the longest
shortest path between any two states) of the state-transition system. So, the diameter could be used to place an
upper bound on how much the transition relation would
need to be unwound. Unfortunately, it appears to be computationally difficult to compute the diameter when the
state-transition system is given implicitly as a circuit or
in terms of propositional formulas for the set of initial
states, the transition relation, and the set of bad states.
Other ways for making BMC complete are based on cube
• a (s0) = s0a.
• If there is a transition from state s to state t in M, then there
is a transition from a (s) to a (t) in Ma.
• For all states s, L(s) Aa = La(a (s)).
The three conditions ensure that Ma simulates M. Note that
only identically labeled states of the concrete model (
modulo propositions absent from Aa) will be mapped into the
same state of the abstract model (see Figure 4). The key theorem relating concrete and abstract systems is the Property
Theorem 1 (Clarke, Grumberg, and Long13). If a universal CTL property holds on the abstract model, then it holds on
the concrete model.
Here, a universal CTL* property is one that contains no
existential path quantifiers when written in negation-normal form. For example, aFP is a universal property but
eFP is not.
figure 4. a concrete system and its abstraction.