Information Technology Reference
In-Depth Information
In [3] a solution to the first problem, and partially to the second problem, was pre-
sented, by replacing BDDs by SAT (propositional satisfiability checking procedures).
In this paper we propose a solution to the second and third problems of symbolic model
checking. Our main contribution is a new model checking algorithm that generalizes
the tableau construction [2] of local model checking for LTL and enables the use of
BDDs. It is based on a mixed DFS and BFS strategy and traverses the state space in a
forward oriented manner.
Our research is motivated by the success of forward model checking [17, 18]. For-
ward model checking is a variant of symbolic model checking in which only forward
image computations are used. Thus it mimics the
on-the-fly
nature of explicit and local
model checking in visiting only reachable states. Note that [18] presented a technique
for the combination of the BFS, used in BDD based approaches, with the DFS of ex-
plicit state model checkers. It was shown that especially this feature enables forward
model checking to find counterexamples much faster. However, only a restricted class
of properties, i.e. path expressions, can be handled by the algorithms of [17, 18].
Henzinger et. al. in [15] partially filled this gap by proving that all properties spec-
ified by Buchi Automata, or equivalently all
-regular properties, can be processed by
forward model checking. In particular, they define a forward oriented version of the
modal
µ
-calculus [20], called
post
-
µ
, and translate the model checking problem of a
ω
-
regular property into a
post
-
µ
model checking problem. Because LTL (linear temporal
logic) properties can be formulated as
ω
-regular properties [29], their result implies that
all LTL properties can be checked by forward model checking.
The fact, that LTL can be checked by forward model checking, can also be derived
by applying the techniques of [17] to the tableau construction of [7]. However, this
construction and also [15] do not allow the mixture of DFS and BFS, as in the layered
approach of [18]. In addition, DFS was identified as a major reason that explicit state
model checking is able to outperform symbolic model checking on certain examples.
The contribution of our paper is the following. First we present a new model check-
ing algorithm that operates directly on LTL formulae. For example [15] requires two
translations, from LTL to Buchi Automata and then to
post
-
µ
. A similar argument ap-
plies to [7, 10]. Second it connects the local model checking paradigm of [2] with
symbolic model checking in a natural way, thus combining BDD based with on-the-fly
model checking. For the modal
µ
-calculus this connection has already been made in [4].
However, a direct application of [4] to the tableau construction of [2], our multiple state
tableau construction, results in a tableau that is exponential in the size of the model.
Only the introduction of a split rule in combination with efficient splitting heuristics al-
lows us to keep the tableau linear in the size of the model. Finally our approach shows,
that the idea of mixing DFS with BFS can be lifted from path expressions [18] to LTL.
Our paper is organized as follows. In the next section our notation is introduced.
Section 3 presents a variation of the single state tableau construction of [2], on which
our multiple state tableau construction, introduced in Section 4, is based. The following
section discusses implementation details of the algorithm. In Section 6 we investigate
heuristics to generate small tableau. An important optimization is presented in Sec-
tion 7. The technical part ends with a discussion of the complexity and comparison
with related work in Section 8. Finally we address open issues.
ω
Search WWH ::
Custom Search