IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 2012

1355

PAPER

Special Section on Formal ApproachEﬃcient Multi-Valued Bounded Model Checking for LTL overQuasi-Boolean Algebras∗
Jeﬀerson O. ANDRADE†a) and Yukiyoshi KAMEYAMA††b) , Members

SUMMARY
Multi-valued Model Checking extends classical, twovalued model checking to multi-valued logic such as Quasi-Boolean logic.
The added expressivity is useful in dealing with such concepts as incompleteness and uncertainty in target systems, while it comes with the costof time and space. Chechik and others proposed an eﬃcient reduction
from multi-valued model checking problems to two-valued ones, but to theauthors’ knowledge, no study was done for multi-valued bounded model
checking. In this paper, we propose a novel, eﬃcient algorithm for multivalued bounded model checking. A notable feature of our algorithm isthat it is not based on reduction of multi-values into two-values; instead, it
generates a single formula which represents multi-valuedness by a suitableencoding, and asks a standard SAT solver to check its satisfiability. Our
experimental results show a significant improvement in the number of variables and clauses and also in execution time compared with the reductionbased one.
key words: multi-valued model checking, bounded model checking, quasiboolean logic

1.

Introduction

Model Checking is an automatic technique for verifying
temporal properties of finite transition systems [2]. Multivalued model checking extends it by using multi-valued
logic [3], [4] instead of two-valued one. Multi-valuedness
gives us a more natural way to express such concepts asincompleteness, uncertainty, authenticity, capability, andmany others, and has been proved useful in various fields
of verification.
This extra expressivity, however, comes at the cost of
performance and/or space, and many researchers have investigated this problem. Among others, Chechik et al. [5] proposed (1) an embedding of Quasi-Boolean algebra (QuasiBoolean logic) into Boolean algebra, and (2) Multi-valued
Decision Diagrams (MDD) as an extension of Binary Decision Diagrams (BDD) [6]. By combining them, theyobtained an eﬃcient symbolic model checker for QuasiBoolean logics. Nakajima [7] applied their technique to verify a non-trivial real-world software specification.
This paper investigates Bounded Model Checking
Manuscript received July 18, 2011.
Manuscript revised November 13, 2011.
†
The author is with the Department of Informatics, Campus
Serra, Federal Institute of Espı́rito Santo, Brazil.
††
The author is with the Department of Computer Science, University of Tsukuba, Tsukuba-shi, 305–8573 Japan.
∗
This paper is a revised and extended version of the paper presented at International Symposium on Automated Technology for
Verification and Analysis, October 20–23, 2008, Seoul, Korea [1].
a) E-mail: joandrade@ifes.edu.brb) E-mail: kameyama@acm.org
DOI: 10.1587/transinf.E95.D.1355(BMC) [8] for multi-valued logic. In particular, we propose
a novel algorithm for multi-valued BMC problems where
both models and specifications are defined over QuasiBoolean algebras.
The fundamental problem to build such an algorithm
is that the standard reduction method is quite ineﬃcient,where reduction means a way to represent a multi-valued
formula by many two-valued ones (which are called slices).
Intead of generating many slices, our algorithm generates asingle two-valued formula that represents these slices withclever encoding. Based on our prototype implemenetation,
our algorithm shows a significant improvement in the number of variables and clauses and also in runtime comparedwith reduction-based one.
The rest of this paper is organized as follows. Section 2
introduces a motivating example, and Sect. 3 introduces basic concepts. Section 4 describes our algorithms, and Sect. 5shows our experiments with a prototype implementation. Finally, Sect. 6 provides our conclusion.
2.

ExampleAs a motivating example, we introduce a simple message
relay system inspired by Nakajima’s example [7]. Figure 1
shows our model for the system, where IDLE etc. are states,
received=F etc. are the values of the variables in eachstate. The model is similar to a Kripke structure, however

Fig. 1A multi-valued model for a simple message relay system.

c 2012 The Institute of Electronics, Information and Communication Engineers
Copyright IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 20121356

some transitions and values are annotated with an elementof Quasi-Boolean algebra such as T (true), S (should), N(should not), and F (false). Unannotated transitions are assumed to have T as its annotation.
Let us explain the model. Initially, the system is IDLE.
It can remain IDLE or transit to RECEIVING. After the message has been RECEIVED, the system starts SENDING. After transmission is completed, the system returns to IDLE.
The system should not present any DELAY on the transmission, but it is possible (not prohibited) that DELAY occurs inexceptional situations. If there is a delay, the system should
eventually resume transmission, but we cannot say it mustresume transmission, since the environment may not allow
it. The system should not lose the received data, but it is
not impossible that an ERROR occurs. After data loss, thesystem should return to IDLE.
We want to specify the following properties on this system using Linear-time Temporal Logic (LTL):
1. All messages received must be sent eventually.
G(received → F sent)
2. The system must always resume from an error.
G(error → F(¬error ∧ ¬received ∧ ¬sent))
3. The system should not begin a transmission unless amessage has been received.
G((¬received ∧ ¬sent) ∨ F(received R ¬sent))
Note that the truth values of the formulas above may
be N or S, and therefore they are actually formulas of multivalued logic† .
The method in this paper allows one to verify theseproperties even if the model is expressed over a QuasiBoolean Algebra.
3.

Basic Definitions and Results

Classical model checking algorithms are defined for Kripke
structures and specifications written as temporal logic formulas. In multi-valued model checking, Kripke structures
and temporal logic are extended so that the domain of truth
values is a multi-valued one. Fitting [3], [4] showed thatmany of the desired properties in multi-valued logic are obtained if the truth values form a complete lattice. In addition, to preserve the relationship between logic operatorsand their meaning, we require the domain to satisfy the distributivity laws (for conjunction and disjunction) and De
Morgan’s laws (for complement). Boolean Algebra satisfies these conditions, but they are too restrictive for practical purposes. Quasi-Boolean Algebra is a minimal structurethat satisfies these conditions, and is widely used in various
areas which need multi-valued logic.
In this section, we review its definition and application
to multi-valued model checking.
3.1 Quasi-Boolean Algebra
A lattice L = L,  is a partially ordered set in which any
two elements x and y have a least upper bound (join, denotedby x y), and a greatest lower bound (meet, denoted byx y). In this paper, we consider only finite lattices, namely,
the set L of elements should be finite. A finite lattice has
the greatest element (denoted by ) and the least element(denoted by ⊥).
Alternatively, a lattice may be defined as an algebraic
structure with the underlying set L and operations and ,i.e., L = L, , .
Definition 1 (Distributive Lattices). We say a lattice L =L,  is a distributive lattice iﬀ the following properties holdfor all x, y, z ∈ L.
x
x

(y
(y

z) = (xz) = (x

y)
y)

(x
(x

z)
z)

Distributivity

It is easy to see that every finite distributive lattice is acomplete lattice, that is, the least upper bound and the greatest lower bound for any set of elements exist.
Definition 2 (Quasi-Boolean Algebra). Given a finite distributive lattice L = L, , , Quasi-Boolean algebra(QBA) is a tuple QL = L, , , ¬ , where ¬ is a unary operator called quasi-boolean complement for which the following properties hold for all x, y ∈ L.
¬(x¬(xy) = ¬x ¬yy) = ¬x ¬y¬¬a = ax  y iﬀ ¬y  ¬x

De Morgan laws
Involution
Anti-monotonicity

Figure 2 shows some QBA of practical interest. Figure 2 (a) shows a 3-valued logic with truth values F (false),
U (unknown) and T (true), where the negation of U is U itself. Figure 2 (b) extends it to n + 1 values with a total order.
Figures 2 (c) and 2 (d) are QBAs obtained by the products
L2 × L2 and L3 × L3 , resp. Figure 2 (e) shows a QBA usedin the example of the previous section. It has six truth values T, F, N (“should not”), DK (“don’t know”), DC (“don’tcare”), and S (“should”). It is interesting to note that negation of S is N, while negation of DK is DK itself.
All Boolean Algebras (BA) are QBAs. Figure 2 (c) and
Fig. 2 (f) are Boolean algebras with 22 elements, and 23 elements, resp, called order-2 and order-3 Boolean Algebras.
Chechik et al. [5] embeds QBAs into BAs using the notion of join-irreducible elements defined below.
Definition 3 (Join-Irreducible Element). Let Q = L, ,, ¬ be a QBA. An element j of L is join-irreducible iﬀ
j is not the least element ⊥, and for any a, b ∈ L, a b = j
implies a = j or b = j.
Definition 4 (Embedding of QBA). Let Q = L, , , ¬ bea QBA, and JQ be the set of join-irreducible elements in Q.
The embedding em : L → 2JQ is defined by em() = { j ∈JQ | j  }.
†
The multi-valued logic used here will be later shown in
Fig. 2 (e).

ANDRADE and KAMEYAMA: MULTI-VALUED BOUNDED MODEL CHECKING

1357• S is a finite set of states.
• I : S → L gives the initial states.
• R : S × S → L gives the transition relation.
• AP is a finite set of atomic propositions.
• V : S × AP → L is the valuation function for an atom
at a state.
(a) L3(c) L2,2 = L2 × L2(b) Ln+1(d) L3,3 = L3 × L3

Note that the codomain of I, R and V is L by which
multi-valuedness may be introduced. For instance, I(s0 ) =U means that it is undefined (unspecified) that s0 is an initial
state or not. We say anmvKS M is total if ( s∈S I(s)) = ,
and, for all s ∈ S , ( s ∈S R(s, s )) = . Following [2],[8], [9], we assume that every mvKS is total throughout thepresent paper.
Definition 6 (Path). A path over a mvKS is a mapping π :N → S where N is the set of natural numbers. The suﬃx π jof a path π denotes the path such that π j (i) = π(i + j) fori ≥ 0.
To express specifications of systems, we use mvLTL,
a multi-valued extension of Linear-time Temporal Logic,
which was first introduced in [10].
Definition 7 (Formulas of mvLTL). Given a mvKS M basedon a QBA Q, a formula in mvLTL is defined as follows:(e) Q6(f) B3 = 2 J3 , ⊆ , J3 = {1, 2, 3}

φ, ψ ::=  | p | ¬φ | φ ∧ ψ | φ ∨ ψ | X φ | F φ | φ U ψFig. 2 Examples of lattices of practical interest. The gray nodes denotejoin-irreducible elements of each lattice.

where  ∈ L (an element of QBA), and p ∈ AP (an atomic
proposition in M).

For instance, in the 3-valued lattice L3 , em maps F, U,
and T, to {} {U}, and {U, T}, resp.
The embedding em is injective, and preserves thegreatest and least elements, meet, and join where we regard
2JQ as a Boolean Algebra ordered by set inclusion. The embedding is not necessarily surjective, and may not preserve
negation. For L3 , negation of U is U, but the complement of{U} in 2JQ is { }, which is not in the image of em.
The embedding gives us a way of representing an element of QBA as a bit sequence. Let j1 , . . . , jn be an enumeration of JQ (we fix the order of these elements.) We
represent  ∈ L by a bit-sequence of length n, where theith bit of the bit-sequence is 1 iﬀ ji  , for 1 ≤ i ≤ n. The
bit-sequence is written as, for instance, 110.

We may introduce other temporal operators such as G
and R using X, F, and U.

3.2 Multi-Valued Model Checking
To perform multi-valued model checking (mvMC) based on
QBA, we need to extend Kripke structures and LTL to theirmulti-valued counterparts.
Let Q = L, , , ¬ be a QBA throughout this subsection. Multi-valued Kripke structures [3] extend 2-valued one
as follows.
Definition 5 (Multi-Valued Kripke Structure).
A multi-valued Kripke structure (mvKS) over Q is a tuple
M = S , I, R, AP, V such that:

Definition 8 (Semantics of mvLTL). Let M be a mvKS overQ as before, π be a path on M, and φ be a mvLTL formula.
We define the interpretation of φ w.r.t. π in M (written π |= φ)as an element of Q as follows:
π |= 

def=

 for  ∈ L

π |= pdef=

V(π(0), p) for p ∈ AP

π |= ¬φdef=¬(π |= φ)π |= φ ∧ ψ

def=(π |= φ)(π |= ψ)π |= φ ∨ ψ

def=(π |= φ)(π |= ψ)π |= X φdef=

π1 |= φπ |= F φ

def=(π |= φ)π |= φ U ψ

def(π |= ψ)=(π1 |= F φ)(π |= φ) (π1 |= φ U ψ)

Note that the interpretation does not necessarily givea boolean value to each mvLTL formula. Rather, it gives atruth value as an element of Q, as indicated by the use of
and in the right-hand side of the definition.
The interpretation above is a straightforward extensionof the standard, boolean semantics of LTL formulas except
one point: the “definition” for F and U may be circular when
π1 is identical to π. This circularity can be easily avoided by

IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 20121358

using the least fixpoint† , since the right-hand sides of the“definitions” are monotone, and the least fixpoints exist forany set of elements, as our domain is a complete lattice.
A counter-intuitive fact about the QBA-based multivalued logic is that logical equivalence is not the same as
equality. As an example, in the three-valued logic L3 , thevalue of U ↔ U (under the standard definition of ↔ in termsof etc.) is not T, but U.
We define the semantics of a mvLTL formula φ w.r.t.
M by:

def
(¬W(π) (π |= φ))
M |= φ =π∈N→S

where W is defined by:def

W(π) = I(π(0))(

is embedded into order-5 BA (with 25 elements), and ¬ ismapped to the bit sequence 10100 by this embedding. To
check v  ¬, we only have to check if at least one of the
2nd , 4th and 5th bits of v is 1, which can be represented by
disjunction.
In summary, we can cope with the generalized queries
with no extra cost, and hence we will ignore the generalized
queries in the subsequent sections.
4.

This section discusses several possible algorithms for multivalued bounded model checking, and present our algorithm.
4.1

R(π(i), π(i + 1)))i≥0W(π) is the “weight” of the path π, which represents the degree of “being a path in M”. In the definition, we explicitly
take the greatest lower bound.
Finally we state the Multi-Valued Model Checking
problem.
Definition 9 (mvMC problem). The multi-valued model
checking problem is to decide if (M |= φ) =holds. If
it holds, we say that φ is valid in M.
It immediately follows that, to check the validity of
φ, we only have to check if there exists a path π (a counterexample of φ) such that the value of (¬W(π)) (π |= φ)is not . By taking negation of both sides, we check if
W(π) (π |= ¬φ) is not ⊥. The last check can be doneusing the bit-sequence representation of QBA elements explained earlier; we only have to check if there is 1 in the bit
sequence, which can be represented by disjunction of all thebits.
In the next section, we present an algorithm to perform
such a check in the context of bounded model checking.
3.3 Generalized Queries
In some applications, we need to check, for  ∈ L, a moregeneral form (M |= φ)  . For instance, the specification
G(received → F sent) of the example in Sect. 2 does notalways hold since the transmission may be delayed infinitely
in some exceptional case. However, the specification should
hold for normal cases, and we would like, then, to check if:

Algorithms

Review of Classical Bounded Model Checking

Figure 3 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 abound k > 0, it generates a propositional formula f(with state variables x0 , x1 , . . . , xk ) which expresses a kbounded model of ¬φ. More precisely, f (x0 , x1 , . . . , xk )holds if and only if x0 , x1 , . . . , xk is either a finite pathor a 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.
3. Finally a SAT solver decides if the CNF is satisfiable
or not. If it is satisfiable, there is a counterexampleof length k. Otherwise, k is incremented and the sameprocedure is repeated.
We have to iterate this process only finitely many times,
up to the completeness threshold: if there is no counterexample until then, we can conclude that the given specification is verified [11].
4.2

Overview of Multi-Valued BMC

The goal of the algorithms is to encode a multi-valued
bounded model checking problem as a boolean satisfiability problem, which can be solved by the state-of-the-art(M |= G(received → F sent))  S
We can cope with the generalized form as follows. A
counterexample of the query (M |= φ)   is a path π such
that
(W(π)

(π |= ¬φ))  ¬It is easy to check if a certain value v is not equal to or
smaller than ¬. For instance, suppose the underlying QBA

Fig. 3

Diagram for classical Bounded Model Checking.

†If we directly define the semantics of G, we should use thegreatest fixpoint.

ANDRADE and KAMEYAMA: MULTI-VALUED BOUNDED MODEL CHECKING

1359

SAT solver. We must convert multi-valued entities (models and formulas) to two-valued ones at some point of ouralgorithm, and the embedding of QBA into BA in the previous section makes such a conversion possible. The questionis when we convert multi-valued ones to two-valued ones,
and we have several possibilities as follows. (They are illustrated in Fig. 4.)
1. Naı̈ve algorithm — route 1 → 3 → 6 → 7 — Thismethod converts the mvKS and mvLTL specification ton 2-valued ones, and then solves the corresponding n
instances of 2-valued BMC problems separately. Thismethod is the easiest way, but is applicable only when
the QBA is a BA, in which case each bit in the bit sequence has no dependency.
2. Reduction-based algorithm — route 2 → 4 → 6 → 7— This method encodes the mvBMC problem as amulti-valued propositional formula θ and then reduces
the formula θ to n 2-valued propositional formulas representing each bit of θ. We then take the conjunctionof the n 2v-propositional formulas as the translation of
the original mvBMC model and proceed with the BMC
procedure as we would do in classical BMC. This approach was investigated for multi-valued boolean logicin [10] where we reported results of some experiments.
3. Direct algorithm — route 2 → 5 → 7 — This method
is similar to the reduction-based one, except that it does
not actually convert (or reduce) QBA to BA, whichtakes time and space. Rather, we generate a single
formula which represents the conversion, and the sizeof the generated formula has comparative length as theformula for each bit, rather than the conjunction of all

such formulas.
There is yet another possible algorithm; we translate
the encoded mvBMC problem (i.e. θ) to a multi-valued
clause form, mvCNF, and then pass it to a multi-valued SAT
solver such as CAMA [12] and CMV-SAT-1 [13]. However,these multi-valued SAT solvers rely on the assumption thatthe set of logic values is totally ordered, which is not generally the case for QBA. Therefore, we do not consider thisalgorithm in this paper.
Naı̈ve conversion was studied in the context of multivalued CTL symbolic model checking [10], [14], but it ismuch less eﬃcient than the others, and therefore we concentrate on the reduction-based and direct algorithms.
We note that while the embedding of QBA to BA does
not preserve negation, it is not a problem in our development, since we first convert, using De Morgan laws, every
multi-valued formulas to the formulas in Negation Normal
Form (NNF), in which negation may appear only in front of
atomic propositions. This point will be explained later.
Both algorithms for mvBMC, reduction-based and direct, share the first step, step 2 in Fig. 4, also referenced
as bounded model generation. Our algorithm for boundedmodel generation is an extension of the 2-valued case [8]and is the same one that we previously published for BA [1].
To illustrate the general idea of the bounded model generation algorithm we present a simple example of its application below.
Example 1. Let M be the model presented in Fig. 1, overthe logic Q6 , the bound k = 2 and also let the negation of thespecification, already in NNF, be ψ = Fsent. We represent
the transition relation of the model M by R(xi , x j )† . So,
following the definitions given in [1], the bounded model
generation outputs the following multi-valued formula:[[M, ψ]]2 = [[M]]2 ∧ [[Fsent]]2[[M]]2 = I (x0 ) ∧

1


(1)

R (xi , xi+1 )i=0= I (x0 ) ∧ R (x0 , x1 ) ∧ R (x1 , x2 )
⎞
⎛ ⎛ 2
⎞
⎟⎟⎟
⎜⎜⎜ ⎜⎜⎜⎟⎟⎟[[Fsent]]2 = ⎜⎜⎜⎝¬ ⎜⎜⎜⎝ R (x2 , xl )⎟⎟⎟⎠ ∧ [[Fsent]]02 ⎟⎟⎟⎠
l=0
⎞
⎛ 2
⎜⎜⎜ 
⎟⎟⎟

0
R (x2 , xl ) ∧ l [[Fsent]]2 ⎟⎟⎠⎟∨ ⎜⎜⎝⎜
l=0
⎞⎞
⎞ ⎛ 2
⎛ ⎛ 2
⎟⎟⎟⎟⎟⎟⎟⎟⎟ ⎜⎜⎜⎜⎜⎜ ⎜⎜⎜⎟⎜⎜⎜= ⎜⎜⎝¬ ⎜⎜⎝ R (x2 , xl )⎟⎟⎠ ∧ ⎜⎜⎝ sent j ⎟⎟⎟⎠⎟⎟⎟⎠
l=0

j=0

⎞⎞
⎛ 2 ⎛
2
⎟⎟⎟⎟⎟⎟⎜⎜⎜ ⎜⎜⎜
⎜⎜sent j ⎟⎟⎟⎠⎟⎟⎟⎠∨ ⎜⎜⎝ ⎜⎜⎝R (x2 , xl ) ∧l=0

Fig. 4 The possible paths to the mvBMC depicted as an extended
flowchart diagram. Q is a QBA, M is the given model, φ is the mvLTL
specification to verify and k is the bound. The numbers in the processes arefor identification purpose only.

(2)

(3)

j=0

In the above set of equations, I and R are mvpropositional formulas that encode the set of initial states
†

tion.

Due to space constraints, we do not unroll the transition rela-

IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 2012

1360

and the transition relation of model M resp. Equation (1)is the general form of the encoding for the bounded model
checking problem. Equation (2) is the encoding for themodel and its transition relation. Equation (3) is the encoding for the given specification. We used sent j as a shorthandfor V (x j , sent), i.e., the valuation of the atomic proposition
sent in the state x j .
We have not specified how we represent I , R , andV , which depends on how we encode state variables
x0 , x1 , · · · , xk . For this, we take a simple method that encodes each state by a binary encoding as follows: let m be
the smallest integer not smaller than log2 |S | (where |S | is thenumber of states). We introduce two-valued propositionalvariables y0 , y1 , · · · , ym−1 , and represent each state by conjunction of positive or negative literals for these variables.
For instance, the state 3 is represented by y0 ∧ y1 ∧ ¬y2 ∧· · · ∧ ¬ym−1 . There are more eﬃcient ways for this encodingin the case of the two-valued BMC, for instance, representing a state by a conjunction of atomic propositions. However, it may not work for some multi-valued models, so wetake this simple encoding. In summary, the formula output
by BMC generation contains two-valued propositional variables y0 , y1 , · · · , ym−1 , which we also call state variables.


4.3 Reduction-Based Algorithm
The Reduction-based Algorithm takes the route 2 → 4 →6 → 7 in Fig. 4 and we explain steps 4 and 6 in this section.
Algorithm 1 shows a top-level description of the
reduction-based mvBMC procedure. The call to function
boundedModel, generates a multi-valued propositional formula which expresses a bounded model of length k. It
slightly extends the classical algorithm in the literature [8]for two-valued bounded model checking. The resulting formula [[M, ¬φ]]k contains state variables x0 , x1 , . . . , xk , andexpresses that x0 , x1 , . . . , xk forms a counterexample of thegiven specification. We have proved that our mvBMC algorithm is correct for an arbitrary finite Boolean algebra [10].

Algorithm 1 Reduction-based mvBMC
1: function redMvBmc(Q,M,φ,k)2:k ← 03:
while k < k do
4:k ← k + 1
5:
ψ ← nnf(¬φ)
6:
θ ← boundedModel(Q, M, ψ, k )7:n ← |JQ |8:θ ← ni=0 θ(i)9:cnf ← boolToCnf(θ )10:S ← satSolver(cnf)11:
if S  ∅ then12:
return false, S
13:
end if14:
end while
15:
return true, ∅16: end function

4.3.1

Reduce mv-Prop Formula to n 2v-Prop Formulas(Step 4)

Line 8 is central in Algorithm 1, since it is where the reduction from mv-propositional to 2v-propositional is performed.
Each formula θ(i) represents one bit (or one layer) of theoriginal mv-formula, i.e., the mv-formula θ being reducedwith respect to a single join-irreducible element of Q.
The process of obtaining θ(i) is not straightforward asin the BA case [10], since the embedding does not preserve
negation. Table 1 shows an example for the negation in QBA
L3 .
Since the variables in the formula we are treating are
two-valued variables only, we can take each slice (each bit)of the formula as follows.
Definition 10 (mv-Propositional Slicing). Given an
mv-propositional formula θ over a QBA Q, we define the2-valued propositional formula θ(i) inductively as follows:
⎧
def
⎪
⎪
= bi (l)
l(i)
⎪
⎪
⎪
⎪
def
⎪
(i)
⎪ (¬l)= bi (¬l)⎨
For literals:
⎪
def
⎪
(i)
⎪
⎪
= y
y
⎪
⎪
⎪
⎪
⎩ (¬y)(i) def
= ¬y
⎧
def
⎪
(i)
⎪
For composite ⎨ (◦ φ)= ◦(φ(i) )⎪def⎪formulas:⎩ (φ ◦ ψ)(i) = φ(i) ◦ ψ(i)where y is a two-valued propositional variable (state variable), bi : L → {0, 1} is a function that maps a lattice value
to its “bit” of order i, assuming a binary encoding for latticevalues. The symbol ◦ is used as a placeholder for logicaloperators such as conjunction.
4.3.2

Convert 2v-Prop Formula to CNF (Step 6)

The call to boolToCnf in Algorithm 1 represents the conversion from 2v-propositional to CNF. In order to generate as
small CNFs as possible, we apply the structure-preserving
CNF conversion [15] to share as many subformulas as possible.
Although sharing subformulas is performed in the laststep, the space-complexity of Reduction-based Algorithm is
not very good, since we generate n formulas corresponding
to n bits (which again corresponds to each join-irreducible
elements), and take the disjunction of them.
4.3.3

Correctness of Reduction-Based Algorithm θ is a 2v-prop. formula.

Theorem 1. The reduction-based algorithm is sound andcomplete, namely, given a mvMC problem Q, M, φ and Found a counterexample.

Table 1 Bitmap representation of lattice values for QBA L3 and theirrespective negations.

 Property φ holds.

Lattice Value
F
U
T

Repr.
00
10
11

Negation
T
U
F

Neg. Repr.
11
10
00

ANDRADE and KAMEYAMA: MULTI-VALUED BOUNDED MODEL CHECKING

1361

a bound k, the algorithm generates a counterexample oflength up to k if and only if M |= φ has a counterexample oflength up to k.
Proof. The proof of this theorem consists of verification ofeach part of the algorithm. Each step is rather straightforward and can be proved by simple reasoning, and thus omitted.

It is easy to see that, even for Multi-Valued Model
Checking, there is a completeness threshold c in the senseof [11], for instance, the “diameter” of mvKS can be such athreshold. It follows that, by repeating the reduction-basedalgorithm for k = 1, 2, · · · , c, we can verify the given specification.
4.4 Direct Algorithm
We now come to Direct Algorithm which we think is thebest among the algorithms. It takes route 2 → 5 → 7. In
this section we cover step 5.
The Direct Algorithm has been developed based on
Reduction-based Algorithm with one additional idea: rather
than generating all the sliced formulas, we introduce propositional variables to represent each slice (bit), and leave thedecision to the SAT solver, as to which slice must actually begenerated. Besides this point, Direct Algorithm is the sameas Reduction-based one; we use negQ (p, i) for negation of
atomic propositions, and we share as many sub-expressions
as possible during the CNF generation.
To understand the key idea, let us first see an example.
Example 2. Consider algebra B3 (Fig. 2 (f)). We introduce
two propositional variables q0 and q1 to represent each slice
number as a binary number. Actually we only have 3 slices(one for each join-irreducible element of B3 ), so we will not
use all possible combinations of q0 and q1 . For instance,the 0th slice is (¬q0 ∧ ¬q1 ), the 1st is (q0 ∧ ¬q1 ) and so on† .
A lattice element 110 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 ) ∧ 110 is representedby (x = s0 ) ∧ ¬q1 . This translation increases the size ofthe resulting formula, compared to the original mv-formula,much less than the Reduction-based algorithm does.
Note that the CNF generation is done without any reduction from mv-propositional formulas to 2-valued ones.

Algorithm 2 Direct Algorithm for mvBMC
1: function mvbmc(Q,M,φ,k)2:k ← 03:
while k < k do
4:k ← k + 1
5:
ψ ← nnf(¬φ)
6:
θ ← boundedModel(Q, M, ψ, k )7:
cnf ← mvPropToCnf(Q, θ)
8:S ← satSolver(cnf)9:if S  ∅ then10:
return false, S
11:
end if12:
end while
13:
return true, ∅14: end function

 Found a counterexample.

 Property φ holds.

Definition 11 (Representation of Lattice Values).
For a QBA Q where n = |JQ |, let h = log2 (n) and
q0 , . . . , qh−1 be propositional variables.
• For a natural number i such that 0 ≤ i < n, we define
Q p (i) for 0 ≤ p < h by:qp
if the pth bit of i is 1
Q p (i) =¬q p otherwise
and then R(i) is defined as Q0 (i) ∧ · · · ∧ Qh−1 (i). Notethat 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.
• For an element  of Q, we define
Rep() =R(i)i∈Ones()where Ones() = {i | ’s ith bit is 1}.
It is possible to use circuit minimization techniques tosimplify the above representation†† . Note also that, we need
only log2 (n) propositional variables to represent the bits,
where n = |JQ |.
Definition 12 (Direct CNF Conversion). Let f be a multivalued propositional formula over a QBA Q, and h =log2 (n), where n = |JQ |.
1. Generate h propositional variables q0 , . . . , qh−1 .
2. Replace any lattice element
  in f by Rep().
3. If n < 2h , let f  be f ∧ n≤i<2h ¬R(i). If n = 2h , let f 
be f . (exclude spurious bits)
4. Apply the structure-preserving conversion to f  .

4.4.1 Convert mv-Prop Formula to CNF (Step 5)
4.4.2
A high level description of our approach to mvBMC is presented in Algorithm 2. This algorithm diﬀers from thereduction-based one in the call to function mvPropToCnf,
which converts a multi-valued propositional formula to a 2valued CNF, which is key to the algorithm’s eﬃciency andis described in Definition 12.

Correctness of Direct Algorithm

The algorithm above is guaranteed to be correct [10]. For
simplicity we assume that n = 2h for some natural number
h where n = |JQ |.
†q0 corresponds to the least significant bit.
Our prototype implements the Quine-McCluskey minimization algorithm.
††

IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 2012

1362

Theorem 2. The direct algorithm is also sound and complete.
Proof. We can prove this theorem by reducing it to the previous theorem as follows: Suppose Direct Algorithm generates the formula ψ in CNF. Then, by definition, for each iless than n, the formula:ψ ∧ Q0 (i) ∧ Q1 (i) ∧ · · · ∧ Qh−1 (i)is equivalent to the i-th sliced formula generated by
Reduction-based Algorithm.
Hence, for some truthassignment for q0 , q1 , · · · , qh−1 , ψ is satisfiable iﬀ the disjunction of all the sliced formulas generated by Reductionbased Algorithm is satisfiable. It follows that, soundness and completeness of Reduction-based Algorithm imply
those of Direct Algorithm.
(a) Loop model L4 .

Since Direct Algorithm is designed as a refinementof Reduction-based Algorithm, we can naturally expect theformer’s performance is better than the latter’s. We will confirm this observation in the next section.
5.

Experiments and Discussion

We have built a prototype that implements both the
reduction-based algorithm and the direct algorithm in
Sect. 4. We implemented the prototype in the Scala programming language over the Java Virtual Machine version
1.6. Algorithm 2 shows the direct mvBMC algorithm, andAlgorithm 1 shows the reduction-based version. Note that
not only CNFs but also the representation of lattice elements are cached and shared, hence they are processed only
once. For SAT solving, we used SAT4J [16] as an embedded
SAT solver. We have executed the tests on a machine with
4.0 GiB of RAM and an Intel Core i5 M430 (2.27 GHz) processor running Ubuntu Linux 10.04 operating system.
The models used in our experiments belong to four different groups.
1. Systems modeled after “real world” examples, takenfrom the literature:a. The coﬀee machine system (CMS) [17].
b. The message relay system (MRS) [7].
2. Systems that form a simple loop, that we called Ln systems. All Ln systems have exactly n states and n variables on each state. Figure 5 (a) shows the graphic representation for the L4 system. Transitions are 2-valued,
with the truth values or ⊥ only. The valuation function is given by V(si , x j ) = tord(Q, i + j), where tord isa selection function that obeys an arbitrary total order
over the elements of Q. Then F xi is valid in this model
if |Q| ≥ n, and not valid otherwise, in which case there
exists a counterexample of length k ≤ |Q| − 1.
3. System that form a completed connected graph, i.e.,
where we have transitions from each state to all theother states in the system, that we called T n systems.

(b) Total model T 5 .
Fig. 5 Example of the artificial test models used to collect statistics ofthe prototype.

All T n systems have exactly n variables on every state
and the weight of every transition is assigned according
to an arbitrary order from the QB algebra over which
the system is defined. Figure 5 (b) shows the T 5 system.
The reason we introduced the artificial systems, Ln and
T n , is that we needed models that could scale on a parameter.
As can be seem by their description the two artificial models
we presented are scalable in the parameter n what makes
possible to obtain the statistical data we needed.
We have run tests with both algorithms for a number of
Ln and T n instances. Of course, due to space limitations we
can not show all these experimental results here, but we selected one instance of each of these systems to illustrate their
behavior. Since we want to compare the two real world systems, CMS and MRS, with the two artificial ones we choose
instances L7 and T 7 since their size is approximately equal
to the size of the coﬀee machine and message relay systems.
Figure 6 shows the evolution of the four selected systems number of CNF variables as a function of k for bothalgorithms, and Fig. 7 shows the number of CNF clauses
also as a function of k. As can be seen, for all systems thegrowth of the curves for the direct algorithm is much slower
than the growth for the reduction-based algorithm, with amuch more accentuated reduction for the number of CNF
clauses. We call attention to the fact that even if the reduction in the number of variables is approximately linear, theabsolute value of this reduction can be significant, with amaximum of more than 104 variables for model MRS in the

ANDRADE and KAMEYAMA: MULTI-VALUED BOUNDED MODEL CHECKING

1363

Fig. 6

Average number of CNF variables.

Fig. 7

Average number of CNF clauses.

data shown. Even more impressive was the reduction in thenumber of CNF clauses. Where the maximum diﬀerence between the reduction-based and the direct algorithm reachedabout 6.5 million clauses.
Maybe of greater interest is the behavior of both algorithms regarding their running time. For that matter, since
the bounded model generation phase is common to bothalgorithms, we concentrated on the CNF conversion time.
Figure 8 show the CNF conversion CPU time of the example model for both algorithms. As can be seen, the runtime
evolution it is much less consistent than that of the numberof CNF variables or clauses, but it is still clearly visible thatthe direct algorithm has a much lower runtime cost than the
reduction-based one. Possible explanations for the inconsistency of the evolution of the CNF conversion runtime are
the fact that the number of shared sub-expressions is not linear in k and the action of the garbage collector of the Java
Virtual Machine which we could not isolate during the collection of data.
Figure 9 shows the SAT solver CPU running time forthe selected models. As we observed for CNF conversion,
the SAT solver running time does not express a consistentbehavior when compared to the number of CNF variables
or CNF clauses. This is a known issue and we do not elab-

Fig. 8Average mv-prop→CNF conversion runtime.

Fig. 9Average SAT solver runtime.

orate on the topic. What we do want to call attention foris the fact that, regardless of the inconsistency of the SAT
solver runtime evolution, in all tested models, the running
time for the direct version of was much smaller than that for
the reduction based version.
Since our experiments are for relatively small models
and our implementation may be sub-optimal we cannot generalize this results at the moment. But we consider theseresults very encouraging.
6.

Conclusion

In this article we presented an extension of classical LTL
model-checking to reasoning with quasi-boolean algebras
and described the notion of multi-valued Kripke structures.
We also presented a translation of the LTL mvBMC problem
over quasi-boolean algebras to a SAT problem. We then presented two algorithms for LTL mvBMC based on this translation, namely the reduction-based algorithm and the direct
algorithm.
As part of our experiments we built a prototype that
implements both algorithms, and our experiments confirm
our claims that for the direct algorithm the number of CNF
variables and clauses generated by the translation is linear in

IEICE TRANS. INF. & SYST., VOL.E95–D, NO.5 MAY 20121364

the size of the problem instance. We also observed a significant reduction in the runtime for the CNF conversion phasein favor of the direct algorithm. This behavior is much more
eﬃcient than the one presented by the reduction-based algorithm in both runtime and space.
As for continuing our research, we expect the method
described here to be useful for dealing with model abstraction. Also in this line of research, we have already started
some theoretical work on the generalization of queries for
multi-valued bounded model checking. We foresee that thisgeneralization technique will also be useful in the context
of model abstraction, so we surely hope to conduct investigations in this area. One other path of future work is toinvestigate the impact of optimization techniques known forclassical bounded model checking for the multi-valued case.
References[1] J.O. Andrade and Y. Kameyama, “A direct algorithm for multivalued bounded model checking,” ATVA 2008: 6th International
Symposium on Automated Technology for Verification and Analysis, Lect. Notes Comput. Sci., pp.80–94, Springer-Verlag, 2008.
[2] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, The
MIT Press, 1999.
[3] M.C. Fitting, “Many-valued modal logics,” Fundamenta Informaticae, vol.XV, pp.235–254, 1991.
[4] M.C. Fitting, “Many-valued modal logics II,” Proc. LFCS’92,
Springer-Verlag, 1992.
[5] M. Chechik, B. Devereaux, S. Easterbrook, Y.C. Lai, and V.
Petrovykh, “Eﬃcient multiple-valued model-checking using latticerepresentations,” Lect. Notes Comput. Sci., vol.2154, pp.441–455,
2001.
[6] D.M. Miller, “Multiple-valued logic design tools,” Proc. 23rd
International Symposium on Multiple-Valued Logic, pp.2–11,
Sacramento, CA, USA, IEEE Computer Society, May 1993.
[7] S. Nakajima, “Behavioural analysis of component framework withmulti-valued transition system,” APSEC ’02, p.217, Washington,
DC, USA, IEEE Computer Society, 2002.
[8] A. Biere, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model
checking using SAT procedures instead of BDDs,” Design Automation Conference, pp.317–320, 1999.
[9] M. Chechik, B. Devereaux, S. Easterbrook, and A. Gurfinkel,“Multi-valued symbolic model-checking,” ACM Trans. Softw. Eng.
Methodol., vol.2, no.4, pp.371–408, 2003.
[10] J.O. Andrade and Y. Kameyama, “An algorithm for bounded multivalued model checking,” Proc. 4th Symposium on Science and Technology for System Verification (DSW 2007), pp.11–20, Nagoya,Japan, Japan Society for Software Science and Technology, 2007.
[11] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” TACAS’99, Lect. Notes Comput. Sci., vol.1579,
pp.193–207, 1999.
[12] C. Liu, A. Kuehlmann, and M.W. Moskewicz, “CAMA: A multivalued satisfiability solver,” Proc. 2003 IEEE/ACM International
Conference on Computer-Aided Design, ICCAD ’03, pp.326–333,
Washington, DC, USA, IEEE Computer Society, 2003.
[13] S. Jain, E. O’Mahony, and M. Sellmann, “A complete multi-valued
SAT solver,” Proc. 16th International Conference on Principles andPractice of Constraint Programming, CP’10, pp.281–296, Berlin,
Heidelberg, Springer-Verlag, 2010.
[14] A. Gurfinkel and M. Chechik, “Multi-valued model checking via
classical model checking,” CONCUR 2003 – Concurrency Theory,
14th International Conference, ed. R.M. Armadio and D. Lugiez,
Lect. Notes Comput. Sci., vol.2761, pp.263–277, Marseille, France,
Springer, Sept. 2003.

[15] D. Plaisted and S. Greenbaum, “A structure-preserving clause form
translation,” J. Symbolic Computation, vol.2, pp.293–304, 1986.
[16] D. Le Berre and A. Parrain, “The SAT4J library, release 2.2,” JSAT
Journal on Satisfiability, Boolean Modeling and Computation, vol.7,
pp.59–64, 2010.
[17] M. Chechik, B. Devereaux, and S. Easterbrook, “Implementing
a multi-valued symbolic model checker,” TACAS’01, Lect. Notes
Comput. Sci., vol.2031, pp.404–419, Springer, 2001.

Jeﬀerson O. Andrade
received the Diploma
of Engineer in Computer Engineering and Master of Informatics degrees from the Federal University of Espirito Santo, Brazil, in 1995 and2001, resp. He is currently pursuing the Ph.D.
in Engineering at the Graduate School of Systems and Information Engineering in the University of Tsukuba. He worked with softwaredevelopment companies in Brazil from 1995 to2003 and he is a lecturer at the Federal Institute of Education, Science and Technology of
Espirito Santo since 2003. His research interests include formal methods
in software engineering, verification and validation of software and logicalmethods in artificial intelligence. He is a member of ACM and SBC.

Yukiyoshi Kameyama
received the B.Sc.
and M.Sc. degrees from the University of Tokyoin 1985 and 1987, resp, and the Ph.D. degreefrom Kyoto University in 1996. He worked asa faculty at Tohoku University and Kyoto University from 1987 to 2001, and he is a professor
at the University of Tsukuba. His research interests include programming logic and software
verification. He is a member of ACM, JSSST
and IPSJ.