A Direct Algorithm for Multi-Valued Bounded
Model Checking
Jeﬀerson O. Andrade and Yukiyoshi Kameyama
Department of Computer Science, University of Tsukuba
joandrade@logic.cs.tsukuba.ac.jp,kameyama@acm.org

Abstract. Multi-valued Model Checking is an extension of classical,
two-valued model checking with multi-valued logic. Multi-valuedness has
been proved useful in expressing additional information such as incompleteness, uncertainty, and many others, but with the cost of time andspace complexity. This paper addresses this problem, and proposes a newalgorithm for Multi-valued Model Checking. While Chechik et al. haveextended BDD-based Symbolic Model Checking algorithm to the multivalued case, our algorithm extends Bounded Model Checking (BMC),
which can generate a counterexample of minimum length eﬃciently (ifany). A notable feature of our algorithm is that it directly generates
conjunctive normal forms, and never reduces multi-valued formulas into
many slices of two-valued formulas. To achieve this feature, we extend the
BMC algorithm to the multi-valued case and also devise a new translation of multi-valued propositional formulas. Finally, we show experimental results and compare the performance of our algorithm with that of areduction-based algorithm.

1

Introduction

Model Checking [7] is a way to verify (or refute) a temporal speciﬁcation against
a system. Multi-valued Model Checking (mvMC) [5] is an extension of the ordinary model checking with multi-valued logic [10]. Multi-valuedness can be used
to express additional information on the system being veriﬁed, such as incompleteness, uncertainty, authenticity, capability, and many others, and has been
proved useful in various areas of system and software veriﬁcation.
The extra expressivity comes at a cost: suppose the domain of truth values
is a 2n -valued Boolean algebra. A naive approach is to decompose the multivalued Kripke structure and speciﬁcation into n components (or slices), each ofwhich constitutes the i-th bit of the original one, and run an ordinary, two-valued
model checker n times. Then the execution time would be n times as long as its
2-valued counterpart. In most applications of multi-valued model checking, eachcomponent of the Kripke structure is similar to each other, checking these nslices independently is obviously suboptimal to do multi-valued model checking.
To solve this problem, Chechik and others formulated the multi-valued model
checking problems with Quasi-Boolean algebra as the domain of truth values [5,4, 6, 8], and proposed a symbolic model checking algorithm based on multi-valuedextension of Binary Decision Diagram (BDD). If several slices of Kripke structure
share the same structures, they can be shared as in the case of BDD’s.
This paper takes an alternative way: we propose a multi-valued model checking algorithm based on bounded model checking (BMC) [1]. In the context of
two-valued model checking, BMC is known to be useful in ﬁnding a counterexamples of minimum length (and sometimes verifying speciﬁcations) eﬃciently
by making use of the propositional SAT solvers1 . We consider the BMC-based
approach is promising in multi-valued model checking, since, in the translationfrom propositional formulas to conjunctive normal forms, all common subformulas can be shared, hence the similarity among slices (components) of the multivalued Kripke structures can be captured automatically. BMC usually ﬁnds acounterexample faster than SMC, but veriﬁcation by BMC is usually slower thanSMC, so these two methods are complementary.
We propose a direct algorithm, rather than a reduction-based one. The
reduction-based one reduces multi-valued formulas into many bits of two-valued
formulas, and uses the ordinary, two-valued model checker. A merit of this approach is that we do not have to invent a new algorithm nor a new tool. A big
drawback is bad performance: if the truth domain is a ﬁnite Boolean algebrathat has 2n elements (that is, there are n slices), then we must run a two-valued
model checker n times. Instead of that we propose an algorithm which keeps
the multi-valued formulas as far as possible, and ﬁnally generates conjunctive
normal forms directly. To achieve this feature we propose a new translation frommulti-valued propositional formulas into conjunctive normal forms.
We compare the following three algorithms for multi-valued bounded model
checking:– Naive algorithm: we reduce the Kripke structures and the speciﬁcation formula into n slices, and use the ordinary, two-valued BMC algorithm n times.
– Reduction-based algorithm: we generate a multi-valued propositional formulawhich represents a bounded model, reduce it to sliced (two-valued) propositional formulas, and ﬁnally convert them to conjunctive normal forms (CNF).
– Direct algorithm: we generate a multi-valued propositional formula which
represents a bounded model, and translate this formula directly to CNF.
We have implemented the latter two and compared their performance, since
Naive algorithm is far less eﬃcient. The experimental results are encouraging:for CNF generation, Direct algorithm is more eﬃcient in time and space than
Reduction-based one, and for SAT solving, their execution time is comparative.
Since CNF generation occupies large part of the total execution time, Direct
algorithm seems to be preferable. In addition, as the size of the lattice grows,
the merit of the direct algorithm becomes larger.
The contribution of this paper can be summarized as follows:– We formulate Multi-valued Model Checking problems in the context of Bounded
Model Checking.
1

SAT for satisﬁability.

2

– We develop not only a reduction-based algorithm for mvMC but also a directtranslation algorithm.
– We compare the eﬃciency of the direct algorithm and the reduction one
using our prototypical implementation, which indicates the direct translation
is promising.
The rest of the article is organized as follows. Section 2 introduces multivalued Kripke structures (mvKS) and the semantics of multi-valued LTL as wellas multi-valued model checking. Section 3 introduces translations from multivalued model checking to multi-valued propositional satisﬁability. The subsequent sections 4, 5 and 6 explain the translation algorithms in detail. Section
7 explains our implementation, and gives performance measurement of experimental results. Section 8 gives conclusion and future work.

2

Basics of Multi-Valued Model Checking

We introduce the basic deﬁnitions of multi-valued Model Checking (mvMC).
The formalization in this section is a slightly extended version of those found in
the literature [5, 4, 6, 8], and readers are encouraged to refer to them for in-depth
explanation and motivating examples on this topic.
2.1

Lattice as the domain of truth values

Classical model checking works for Kripke structures and speciﬁcation written asa temporal logic formula. In multi-valued model checking, both Kripke structures
and temporal logic are extended to multi-valued ones where the domain of truth
values forms a lattice with possibly more than two elements. In this paper we
use ﬁnite Boolean algebras (with 2n elements) as the domains of truth values.
Although this is a more restrictive choice than those found in the literature (forinstance, Chechik et al. studied mvMC on Quasi-Boolean algebras [5]), the focusof this paper is in the algorithmic and implementational aspects. We will discuss
the extension to more general lattices brieﬂy in Section 8.
We assume that L is a ﬁnite Boolean algebra with a set L of values andoperations u (meet), t (join) and ∼ (negation). An order-n Boolean algebrais the one with 2n elements for a natural number n, and its element can be
represented by n bits (written, for instance, #1101). Then lattice operations join
defand meet can be performed in a bit-wise manner. We write > = #11...1 (top)defand ⊥ = #00...0 (bottom).
2.2

Multi-Valued Kripke Structure

Classical Kripke structures are extended to multi-valued ones as follows.
Deﬁnition 1 (Multi-Valued Kripke Structure) A Multi-Valued Kripke Structure (mvKS) over a a lattice L = hL, u, t, ∼i is the tuple M = (S, I, R, AP, V)
such that:3

– S is a ﬁnite set of states.
– I : S → L speciﬁes the initial states with its “degree”.
– R : S × S → L is the transition relation in the lattice.
– AP is a ﬁnite set of atomic propositions.
– V : S × AP → L is the valuation function that determines the truth value ofan atom at a state.
Some authors [3] keep the transition relation deﬁned over a two-valued lattice.
Here we gave a general deﬁnition for it.
Example 1 (mvKS) The following data determines an mvKS over order-4
Boolean algebra:
S = {s0 , s1 , s2 , s3 } #1100 if x = s0
I(x) = #0011 if x = s3⊥otherwise>if (x, y) ∈ {(s0 , s1 ), (s1 , s2 ), (s3 , s0 )}
#1010 if (x, y) = (s2 , s3 )R(x, y) =#0101 if (x, y) = (s2 , s0 )⊥otherwise
AP = {p}{>V(x, p) =⊥if x = s3otherwise

The mvKS in Example 1 is illustrated in the left of Figure 1.

s0
#1100

s0

s2
p
0th slice

s3

s0

s1

s0

s2

s3

s1

#1111
s0

s1

reduction

s3

#0101
#1111

#1111
#0011

s1

#1010

s3

s2

p

superposition

Multi-valued
Kripke structures3p

2nd sliceps2

1st slice
s1

p

s2

3rd slice

4 slices (Kripke structures)

Fig. 1. Multi-Valued Kripke Structure and its Reduction

We can view an mvKS as a superposition of n classical Kripke structures,
each of which corresponds to the i-th bit of the lattice. The Kripke structure4

corresponding to each bit is called a slice of the mvKS. In Figure 1, the rightﬁgure shows the decomposition (or reduction) of the mvKS into 4 slices. It
is apparent that, in the case of order-n Boolean algebra, model checking an
mvKS is equivalent to model checking of its n slices (modulo the time and spacecomplexity).
F
mvKS M is total if ( s∈S I(s)) = >, and, for all s ∈ S,
F We say an( s0 ∈S R(s, s0 )) = >. It is easy to see that an mvKS is total if and only if
all its slices are total and have at least one initial state. Following Clarke et al.
[7], we assume that every mvKS is total throughout the present paper.
We deﬁne a path as an inﬁnite sequence of states, namely, a mapping π :N → S where N is the set of natural numbers. For a path π, π j denotes the j-th
suﬃx (path), that is, π j (i) = π(i + j) for i ≥ 0.
2.3

Multi-Valued Linear-time Temporal Logic

We use Linear-time Temporal Logic (LTL) as the speciﬁcation logic with a slight
extension to express multi-valuedness over a lattice L. We call this extension
mvLTL.
Deﬁnition 2 (Formulas of mvLTL) Let AP be a set of atomic propositions,and p ∈ AP and ` ∈ L where L = hL, u, t, ∼i is a ﬁnite Boolean algebra. An
mvLTL formula is deﬁned as follows:φ, ψ ::= ` | p | ¬φ | φ ∧ ψ | φ ∨ ψ| Xφ | Fφ | Gφ | φUψ | φRψ
Deﬁnition 3 (Semantics of mvLTL) Let M be an mvKS as above, π be apath on M, and φ be an mvLTL formula. We deﬁne the interpretation of φ withrespect to π in M, written (π |= φ), as an element of L as follows:def– (π |= `) = ` for ` ∈ L.
def

– (π |= p) = V(π(0), p) for p ∈ AP.
def– (π |= ¬φ) = ∼(π |= φ).
def– (π |= (φ ∧ ψ)) = (π |= φ) u (π |= ψ).
def– (π |= (φ ∨ ψ)) = (π |= φ) t (π |= ψ).
def– (π |= X φ) = (π 1 |= φ).
def F– (π |= F φ) = i≥0 (π i |= φ).
def d– (π |= G φ) = i≥0 (π i |= φ).
ddef F– (π |= φ U ψ) = i≥0 ((π i |= ψ) u ( j<i (π j |= φ))).
F
def d– (π |= φ R ψ) = i≥0 ((π i |= φ) t ( j≤i (π j |= ψ))).
In the interpretations of temporal operators, we take inﬁnitary meet and join,
but they always exist since we are working with ﬁnite Boolean algebras.
5

2.4

Multi-Valued Model Checking Problem

We deﬁne the semantics of an mvLTL formula φ with respect to M by:ldef(M |= φ) =((∼W(π)) t (π |= φ))π∈N→Swhere W is a mapping from the set of paths to L deﬁned by:ldefW(π) = I(π(0)) u ( R(π(i), π(i + 1))).
i≥0W(π) is the weight of the path π, which represents the degree of “being a pathin M”. In particular, if the ﬁrst state of the path π is not an initial state(I(π(0)) = ⊥), then W(π) = ⊥, hence such a path does not aﬀect the value of
M |= φ.
The multi-valued model checking problem is to decide if (M |= φ) = > holds
or not. If it holds, φ is valid in M.
A counterexample of φ with respect to M is a path π such that(∼W(π)) t (π |= φ) 6= >or, equivalently,
W(π) u (π |= ¬φ) 6= ⊥.
It is easy to see that φ is valid iﬀ its counterexample does not exist. In the next
section, we present an algorithm to ﬁnd such a counterexample, if it exists.

3

Algorithms of Multi-Valued Bounded Model Checking

We aim to obtain an eﬃcient multi-valued model checker. In the literature, theBDD-based Symbolic Model Checking (SMC) has been extended to the MDDbased one where MDD is a multi-valued extension of BDD [4]. However, as longas the authors know, there has been no attempt to exemplify the multi-valued
extension of Bounded Model Checking (BMC), which is the goal of this paper.
3.1

Review of Two-Valued Bounded Model Checking

Figure 2 illustrates the process of classical Bounded Model Checking.
The process can be rephrased in words as follows.
1. Given a Kripke structure, an LTL formula φ, and a bound k > 0, it generates a propositional formula f (with state variables x0 , x1 , . . . , xk ) which
expresses a k-bounded model of ¬φ. More precisely, f (x0 , x1 , . . . , xk ) holds
if and only if x0 , x1 , . . . , xk is either a ﬁnite path or a “lasso”-shaped looping
path such that ¬φ holds along this path.
2. The formula f is converted to a conjunctive normal form (CNF) since most
SAT solvers accept CNF only.
6

Kripke Structure
propositional
conjunctive
LTL formula
formulanormal formbound k >0
prop-to-cnf
bounded model
SAT solving
conversion
generation

satisfiable

unsatisfiable

Fig. 2. Process of Bounded Model Checking

3. Finally a SAT solver decides if the CNF is satisﬁable or not. If it is satisﬁable,
there is a counterexample of length k, and otherwise, k is incremented andthe same procedure is repeated.
We have to iterate this process only ﬁnitely many times, up to the completeness threshold: if there is no counterexample until then, we can conclude thatthe given speciﬁcation is veriﬁed [1].
3.2

Overview of Multi-Valued Bounded Model Checking

We desire a BMC algorithm for the multi-valued case, but still utilizing stateof-the-art SAT solvers which works for two-valued formulas. Hence, we need toswitch from the multi-valued world to the two-valued one at some point in Figure
2. There are three possibilities for this, which are illustrated by Figure 3.

mvKS
mvLTL formula
bound k >01

mv propositional
formula5boundedmodel
generation

reduction

Kripke Structure
LTL formula
bound k >0

prop-to-cnf
conversion
6

reduction

7

reductionsatisfiable2
boundedmodel
generation

propositional
formula3
prop-to-cnf
conversion

conjunctive
normal form

4
SAT solving unsatisfiable

Fig. 3. Process of Multi-Valued Bounded Model Checking

Reﬂecting the three possibilities, we get three algorithms for Multi-valued
Bounded Model Checking:– Naive Algorithm is the route 1 → 2 → 3 → 4, which ﬁrst reduces the mvKSand mvLTL formula to two-valued one.
7

– Reduction-based Algorithm is the route 5 → 6 → 3 → 4, which reduces theoutput of the mv-formula generated by bounded model generation.
– Direct Algorithm is the route 5 → 7 → 4, which keeps the multi-valuedness
as far as possible, and directly generates CNF.
Since performance of Naive Algorithm is the worst, we will investigate thelatter two where we use or extend the following algorithms and tools that weredeveloped for the two-valued case:– For bounded model generation, we slightly extend Biere et al’s algorithm [1].
– For the conversion from propositional formula to CNF, we extend the algorithm for structure-preserving conversion [12, 1].
– For SAT solving, we use MiniSat solver [9].

4Bounded Model Generation

The process of multi-valued Bounded Model Generation (Step 5 in Figure 3)
is common to Reduction-based and Direct Algorithms. It generates a multivalued propositional formula which represents a k-bounded model, namely, acounterexample for the given speciﬁcation of length k.
The algorithm is an extension of the two-valued case [1] and generates amulti-valued propositional formula (mv-propositional formula), which is a propositional formula possibly with lattice elements as propositional constants.
Example 2 As examples of mv-propositional formula, we deﬁne the formulas
I 0 and R0 which correspond to I and R in Example 1.
I 0 (x) = (x = s0 ∧ #1100) ∨ (x = s3 ∧ #0011)
def

R0 (x, y) = (x = s0 ∧ y = s1 ) ∨ (x = s1 ∧ y = s2 ) ∨ (x = s3 ∧ y = s0 )def

∨ (x = s2 ∧ y = s3 ∧ #1010) ∨ (x = s2 ∧ y = s0 ∧ #0101)
Deﬁnition 4 (Bounded Model Generation) Let M, φ, and k be an mvKS,
an mvLTL formula, and a non-negative integer, resp., and x0 , x1 , . . . , xk bevariables for states. Then we construct a multi-valued propositional formula[[M, ¬φ]]k with free variables x0 , x1 , . . . , xk as follows:def[[M, ¬φ]]k = [[M]]k ∧ [[¬φ]]k ,[[M]]k = I 0 (x0 ) ∧
def

k−1
∧

where

R0 (xi , xi+1 )

i=0

( ( k
)
)
k
∨
∨
( 0
)
def
0
0
[[¬φ]]k = ¬R (xl , xk ) ∧ [[¬φ]]k ∨R (xk , xl ) ∧ l [[¬φ]]0k
l=0
0

l=0

0

where I and R are the mv-propositional formulas representing I and R in M,
and the mv-formulas [[¬φ]]0k and l [[¬φ]]0k are deﬁned in Figure 4.
8

i defl [[`]]k = `i def
0l [[p]]k = V (xi , p)
i def
0
def
l [[¬p]]k = ¬V (xi , p)[[`]]ik = `
def
i
i
i
def
l [[φ ∧ ψ]]k = l [[φ]]k ∧ l [[ψ]]k[[p]]ik = V 0 (xi , p)
def
i
i
i
def
l [[φ ∨ ψ]]k = l [[φ]]k ∨ l [[ψ]]k[[¬p]]ik = ¬V 0 (xi , p)succ(i)
i def
i def
i
i
l [[X φ]]k = l [[φ]]k[[φ ∧ ψ]]k = [[φ]]k ∧ [[ψ]]kji def Wkiii defl [[F φ]]k =[[ψ]]k[[φ ∨ ψ]]k = [[φ]]j=min(i,l) l [[φ]]k k ∨i+1
V
k
j
i def
[[φ]]k , if i < kdefl [[φ]]kl [[G φ]]k =j=min(i,l)[[X φ]]ik =
“
”
W
V
⊥,
otherwise
def
k
j−1
j
i
n
=
[[φ
U
ψ]]
[[ψ]]
∧
[[φ]]
∨
l
l
l
W
k
k
k
j=i
n=i
def
„
«
Vk
[[F φ]]ik = kj=i [[φ]]jk
j
n
W
[[ψ]]
∧
∧
[[φ]]
l
l
i−1
k
k
n=i
i def
W
j−1
n
j=l
[[G φ]]k = ⊥n=l l [[φ]]kVj−1 nj
i def WkVdefkj[[φ U ψ]]k = j=i ([[ψ]]k ∧ n=i [[φ]]k ) l [[φ R ψ]]i =kj=min(i,l) l [[ψ]]k ∨
V
”
def W
Wk “
Vj
j
n
[[φ R ψ]]ik = kj=i ([[φ]]jk ∧ jn=i [[ψ]]n)kj=i l [[φ]]k ∧n=i l [[ψ]]k ∨i„«V(a) Translation [[φ]]k of an mvLTL forWi−1 l [[φ]]jk ∧ kn=i l [[ψ]]nk∧Vmula φ without a loop.
jnj=l
n=l l [[ψ]]ki(b) Translation l [[φ]]k of an mvLTL formula φ

for a (l, k)-loop.

Fig. 4. The inductive deﬁnition of the translation for an mvLTL formula φ in NNF
with a bound k and i ∈ N with i ≤ k, where V 0 is the formula representing V.

As in the two-valued case, the formula [[M, ¬φ]]k is constructed so that it has
a non-⊥ value if and only if x0 , x1 , . . . , xk form either a ﬁnite path along which¬φ holds in the bounded semantics, or an (l, k)-loop (the next state of xk is xl forsome l ≤ k) along which ¬φ holds in the standard semantics. Corresponding to
the two cases, the mv-formulas [[¬φ]]0k and l [[¬φ]]0k represent the semantics of ¬φat the state 0. Note that, following Biere et al.[1], Figure 4 deﬁnes the translation
for φ in NNF (Negation Normal Form) only, hence we need to convert ¬φ to
NNF before applying the translation in Figure 4.
The deﬁnition above is almost the same as the two-valued one found in theliterature[1] except the following points:– The formulas I 0 , R0 , and V 0 are multi-valued propositional formulas, namely,
they may contain lattice elements as subformulas.
– However, the atomic formula x = sj is interpreted by either > or ⊥, namely,
it essentially remains a two-valued formula.
We say an mv-propositional formula f with free state variables x0 , . . . xk is
satisﬁable if and only if f has a non-⊥ value for some assignment of x0 , . . . xk tostates. Then we have the following theorem.
Theorem 1 (Correctness of Bounded Model Generation) Let M be an
mvKS and φ be an mvLTL formula.
9

Soundness If [[M, ¬φ]]k is satisﬁable, then there exists a counterexample of φin M whose length is k.
Completeness If φ is not valid in M, then [[M, ¬φ]]k is satisﬁable for some k.
Proof. For each i < n (where n is the order of Boolean algebra), the i-th
slice of [[M, ¬φ]]k is identical to the resulting formula of two-valued Bounded
Model Generation for the i-th slice of M and φ. Also the totality condition for
mvKS implies totality for sliced Kripke structures. Hence the soundness andcompleteness for the multi-valued version of bounded model generation follows
from that for the two-valued version, which was proved, for instance, in [2].

5Reduction-based Algorithm

Reduction-based Algorithm takes the route 5 → 6 → 3 → 4 in Figure 3, and we
explain Steps 6 and 3 in this section.
Deﬁnition 5 (Reduction of mv-Propositional Formula (Step 6)) Givena multi-valued propositional formula f , we deﬁne its i-th slice, Slicei (f ), as follows:{⊥ if the i-th bit of ` is 0
def
Slicei (`) => if the i-th bit of ` is 1
For other cases, Slicei (f ) is deﬁned homomorphicly, for instance, Slicei (φ∧ψ) =Slicei (φ) ∧ Slicei (ψ).
For example, for I 0 (x) in Example 2, Slice1 (I 0 (x)) is (x = s0 ∧ >) ∨ (x = s3 ∧ ⊥),which is simpliﬁed to (x = s0 ). Obviously, f is satisﬁable (has a non-⊥ value) if
and only if Slicei (f ) is satisﬁable for some i.
The result of Step 6 is n sliced propositional formulas. We then take their
disjunction (since we are interested in satisﬁability), and converts it to a CNF.
For the Prop-to-CNF Conversion (Step 3), we use the structure-preserving conversion [12, 1].
A few remarks follow.
– All common subformulas will be shared by the conversion, which is especially
useful in the context of multi-valued model checking, as we assume that slices
of one mvKS are similar to each other.
– However, sharing in Reduction-based Algorithm is not completely satisfactory. Since sharing occurs only among identical subformulas, a small diﬀerence in a deeply nested subformula prohibits sharing. Suppose we reduce an
mv-formula (((#10 ∧ a) ∨ b) ∧ a) ∨ b into two slices and convert the disjunction of these slices into CNF. Although the two slices ((a ∨ b) ∧ a) ∨ b and(b ∧ a) ∨ b are quite similar to each other, they do not share any subformulas except a and b. In general, if a lattice element exists in a deeply nested
subformula of the given mv-formula, sharing does not take place. In such acase, Reduction-based Algorithm cannot generate a small CNF.
10

6

Direct Algorithm

We explain Step 7 in Figure 3, which is the key step of Direct Algorithm (5 →7 → 4). This algorithm is motivated by occasional ineﬃciency of Reductionbased Algorithm as explained in the previous section. In order to generate as
small CNF’s as possible, we should share as many subexpressions as possible.
Our idea is simple: rather than generating all the sliced formulas, we introduce new propositional variables to represent slices, and leave the decision as towhich slice should be generated to the SAT solver.
Let us give an example. Example 2 uses the order-4 Boolean algebra, so we
introduce two propositional variables q0 and q1 to represent each slice number
as a binary number. For instance, the 0th slice is (¬q0 ∧ ¬q1 ), the 1st is (q0 ∧ ¬q1 )and so on.2 A lattice element #1100 has the bit 1 in the 0th and 1st slices, hence
it is represented by (¬q0 ∧ ¬q1 ) ∨ (q0 ∧ ¬q1 ), or simply ¬q1 . Then an mv-formula(x = s0 ) ∧ #1100 is represented by (x = s0 ) ∧ ¬q1 . Then the whole formula I 0 (x)is represented by ((x = s0 ) ∧ ¬q1 ) ∨ ((x = s3 ) ∧ q1 ). This translation increases
the size of the resulting formula, compared to the original mv-formula, much lessthan the Reduction-based algorithm does.
Deﬁnition 6 (Representation of Lattice Values) For an order-n Boolean
algebra L, let h = dlog2 (n)e and q0 , . . . , qh−1 be propositional variables.
– For a natural number i such that 0 ≤ i < n, we deﬁne Qp (i) for 0 ≤ p < hby:{
qp if the p-th bit of i is 1
Qp (i) =¬qp otherwise
and then R(i) is deﬁned as Q0 (i)∧· · ·∧ Qh−1 (i). Note that R(i) is the binary
representation of i in terms of q0 , . . . , qh−1 . For instance, if h = 5, then R(6)is ¬q0 ∧ q1 ∧ q2 ∧ ¬q3 ∧ ¬q4 , which is 00110 as a binary number (note thatq0 corresponds to the least signiﬁcant bit). ∨– For an element ` of L, we deﬁne Rep(`) = i∈One(`) R(i) where One(`) ={i | `’s i-th bit is 1}.
Although the above representation is not quite eﬃcient, we can make useof the Karnaugh map technique to simplify it. Note also that, we need only
dlog2 (n)e propositional variables to represent slices in the order-n Boolean algebra.
Deﬁnition 7 (Direct Algorithm (Step 7)) Let f be a multi-valued propositional formula over the order-n Boolean algebra, and h = dlog2 (n)e.
1. Generate h propositional variables q0 , . . . , qh−1 .
2. Replace any lattice element∧ ` in f by Rep(`).
3. If n < 2h , let f 0 be f ∧ n≤i<2h ¬R(i). If n = 2h , let f 0 be f .
4. Apply the structure-preserving conversion [12, 1] to f 0 .
2Here we assume q0 corresponds to the least signiﬁcant bit.

11

The third step is necessary to exclude spurious slices.
The algorithm above is guaranteed to be correct. For simplicity we assume
that n = 2h for some natural number h.
Theorem 2 (Correctness of Direct Algorithm) Let f be an mv-propositional
formula over the order-n Boolean algebra with n = 2h . If the algorithm for
Step 7 generates a CNF c with q0 , . . . , qh−1 , then f is satisﬁable (in the multivalued sense) if and only if c is satisﬁable for some truth-value assignment for
q0 , . . . , qh−1 .
Proof. We have that f is satisﬁed if and only if its i-th sliced formula issatisﬁed for some i. Since each slice is represented by a truth-value assignmentof qj ’s, this is equivalent to the satisﬁability of the resulting CNF for someassignment of qj ’s.

7

Experimental Results

We have implemented Reduction-based and Direct Algorithms for mvMC, andcompared their performance3 . Our implementation choices are listed below.
– For Reduction-based Algorithm, we compose (fuse) Step 6 and Step 3 into asingle recursive function to gain better performance. At the same time, thefunction simpliﬁes the formula using > ∧ f ↔ f etc., and this choice forces
us to use the bottom-up variant of the prop-to-CNF conversion.
– For Direct Algorithm, we implement the top-down algorithm in Section 6.
Note that not only CNF’s but also the representation of lattice elements arecached and shared, hence they are processed only once.
– For SAT solving, we use MiniSat solver version 1.14 using the DIMACS
format [11] as its input.
We have implemented these algorithms in the programming language OCaml,and executed them on a machine with 1.0GB memory and Intel Celeron (2.8GHz) processor running Linux Operating System.
For the target of this experiment, we take a simple mvKS with m states,
and the order of Boolean algebra is n. The ﬁrst model, Model-1, is illustrated

s0

s1

s2

s(m-1)

Fig. 5. Model-1

in Figure 5, which shows its initial state (s0 only) and the transition relation.
3

In fact, we have implemented many other variants, but here we list only the resultsof the two most eﬃcient algorithms.

12Model-1

CNF gen. SAT solving
CNF sizek n m red. direct red. direct one bit
red. direct result
14 32 16
20 0.0
0.0 5470 11590 6331 unsat.
15 32 16
20 0.0
0.0 5889 12417 6801 sat.
30 64 32 32
0 0.5
0.1 23276 72380 26569 unsat.
31 64 32 40
0 0.2
0.0 24129 74817 27521 sat.
62 128 64 683
7 5.4
0.6 95818 488938 108615 unsat.
63 128 64 715
8 1.0
0.1 97537 496897 110529 sat.
Table 1. Experimental Results for Model-1.

Model-2

CNF gen. SAT solving
CNF sizek n m red. direct red. direct one bit
red. direct result
10 128 64 66
1 4.4
8.2 30826 99466 33483 unsat.
12 128 64 90
2 9.7
11.1 36718 117838 39765 unsat.
14 128 64 113
2 12.514.0 42634 136234 46071 unsat.
16 128 64 145
2 25.412.2 48574 154654 52401 unsat.
18 128 64 184
2 63.722.9 54538 173098 58755 unsat.
20 128 64 226
2 94.428.6 60526 191566 65133 unsat.
22 128 64 281
3 42.814.0 66538 210058 71535 sat.
24 128 64 329
3 60.913.8 72574 228574 77961 sat.
Table 2. Experimental Results for Model-2.

Transitions are essentially two-valued (with the truth values > or ⊥ only) so we
do not write the lattice elements as their values. The valuation function only ismulti-valued:
V(si , p) = #0· · · 010· · · 0
with the i-th bit being 1. Then F p is valid in this model if m ≥ n, and not valid
otherwise, in which case there exists a counterexample of length k = m − 1.
The other two models, Model-2 and Model-3, are small variants of Model-1: inModel-2, R(si , sj ) = > if and only if i < j ≤ ((i + 3) mod m), and in Model-3,
R(si , sj ) = > if and only if i < j ≤ ((i + 8) mod m). In addition, the valuation
function in Model-3 is modiﬁed to: V(si , p) = #0· · · 01· · · 10· · · 0 with the i-th toi + 8-th bits being 1.
Tables 1, 2 and 3 show several experiments for these models. In the table,“red.” means Reduction-based Algorithm and “direct” Direct one. The column“CNF gen.” shows the execution time (in seconds) before SAT solving (Steps 6
and 3 for Reduction-based one and Step 7 for Direct one), and the column “SAT
solving” shows the execution time (in seconds) for SAT solving for their output
CNF’s. The column “CNF size” shows the number of clauses in the generated
CNF4 where the column “one bit” shows the CNF size of one slice. The column
4

The number of propositional variables and the overall size of CNF are almost linear
in the number of clauses in all cases.

13Model-3

CNF gen. SAT solving
CNF sizek n m red. direct red. direct one bit
red. direct result
10 32 128 95
5 20.532.1 142808 138977 138320 unsat.
12 32 128 124
5 25.946.9 164664 169968 165423 unsat.
14 32 128 157
7 35
81.7 191032 197152 191893 unsat.
16 32 128 204
9 22.90.2 217424 224360 218387 sat.
18 32 128 289
13 24.1
29.8 243840 251592 244905 sat.
Table 3. Experimental Results for Model-3.

“result” shows the result of SAT solving where “sat.” means the algorithm ﬁnds
a counterexample for the given bound k, the model with m states and the ordern lattice. It should be noted that our implementations show the correct answers
for all cases.
We can understand the results as follows.
– Eﬃcient implementation of mv-BMC is possible. Compared with the one-bit
case, both algorithms can generate CNF’s whose size is much smaller thann times of the CNF size of one-bit case. For instance, the bottom line of
the ﬁrst table shows that Direct Algorithm generated a CNF with 110,529
clauses which is only 13% larger than that generated by the one-bit slice(note that n = 128 for this experiment).
– For the comparison between Reduction-based and Direct Algorithms, thelatter is better in CNF-generation: its execution time is always much faster(and the diﬀerence becomes huge when the order n becomes larger), and thesize of generated CNF is smaller or roughly the same.
– The execution time of the SAT solver for the generated CNF is not easily
compared between the two methods. Reduction-based one is usually betterfor smaller n’s despite the fact that it generates a bigger CNF. However, thediﬀerence is not very big, and Direct method is sometimes better.
– Since CNF generation phase takes longer time than SAT solving, the total
execution of Direct Algorithm is better than that of Reduction-based one.
Since our experiments are for relatively small models, and our implementation may be suboptimal, we cannot generalize this statement at the moment.
However, these results are surely encouraging.

8

Conclusion and Future Directions

We have explored the possibility to obtain an eﬃcient Multi-valued Bounded
Model Checker, and for this purpose, we have formalized Reduction-based andDirect Algorithms with correctness guarantee. We have implemented these algorithms (together with other ones) and successfully shown that Multi-Valued
Bounded Model Checking is surely possible. Also, we have compared their performance: to the extent we have tested, Direct Algorithm seems to be better
than Reduction-based one, but this last point should be examined further.
14

For future work, we need to introduce into our framework various optimizations found in the context of two-valued BMC. We have already started in investigating some of such optimizations, which are easily integrated to our algorithms.
Another obvious thing to do is to extend the lattice to more general one such as
Quasi-Boolean algebras, which seems not too diﬃcult, after Chechik and others’
work [5]. Experiments with larger, more realistic Kripke structures and ﬁnding
good application areas are also important.
Acknowledgments. We would like to thank the anonymous referees for
insightful comments. The authors were supported in part by JSPS Grant-in-Aid
for Scientiﬁc Research 20650003.

References
1. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without
BDDs. In TACAS’99, volume 1579 of Lecture Notes in Computer Science, pages
193–207, 1999.
2. A. Biere, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using
SAT Procedures Instead of BDDs. In Design Automation Conference, pages 317–
320, 1999.
3. M. Chechik, B. Devereaux, and S. Easterbrook. Implementing a multi-valued
symbolic model checker. In TACAS’01, volume 2031 of Lecture Notes in Computer
Science, pages 404–419. Springer, 2001.
4. M. Chechik, B. Devereaux, S. Easterbrook, and A. Gurﬁnkel. Multi-valued symbolic model-checking. ACM Transaction on Software Engineering and Methodology,
2(4):371–408, 2003.
5. M. Chechik, B. Devereaux, S. Easterbrook, Y. C. Lai, and V. Petrovykh. Eﬃcient multiple-valued model-checking using lattice representations. Lecture Notes
in Computer Science, 2154:441–455, 2001.
6. M. Chechik, A. Gurﬁnkel, B. Devereaux, A. Lai, and S. Easterbrook. Data
structures for symbolic multi-valued model-checking. Form. Methods Syst. Des.,29(3):295–344, 2006.
7. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press,
1999.
8. S. Easterbrook and M. Chechik. A framework for multi-valued reasoning overinconsistent viewpoints. In International Conference on Software Engineering,
pages 411–420, 2001.
9. N. Een and N. Sorensen. The MiniSat homepage, http://minisat.se/.
10. M. C. Fitting. Many-valued modal logics. Fundamenta Informaticae, XV:235–254,
1991.
11. D. S. Johnson and M. A. Trick, editors. Cliques, Coloring and Satisﬁability: Second
DIMACS Implementation Challenge, volume 26 of DIMACS Series In Discrete
Mathematics and Theoretical Computer Science. AMS, 1996.
12. D. Plaisted and S. Greenbaum. A structure-preserving clause form translation.
Journal of Symbolic Computation, 2:293–304, 1986.

15