|
Search Techniques and Automata for Symbolic Model Checking
Computer Science PhD Candidate
Model checking addresses the correctness of finite-state systems by
automatically proving or refuting user-defined properties. The algorithms
search very large graphs and are memory and time intensive. In our application,
we use symbolic methods, based on binary decision diagrams, that consider sets
of nodes without enumerating their elements.
Checking whether a model satisfies a Linear-Time Logic (LTL) formula proceeds
by translating the formula into a Buechi automaton, taking the product of the
automaton and the model under scrutiny, and testing whether the language of the
product is empty or not. From the latter check it is determined whether the
property holds.
We address the size of the Buechi automaton, an important factor in efficiency,
by improving the translation. We propose a three-stage process consisting of
rewriting, translation using Boolean optimization methods, and simulation-based
optimization. The resulting automata are significantly smaller than the
automata produced by previously known methods.
We improve the language-emptiness check for automata in three ways. First, we
base the choice of algorithm on a classification of the automata into strong,
weak, and terminal automata. We show that this choice improves the efficiency
for certain cases both in theory and in practice.
Second, we present a symbolic SCC-decomposition algorithm that can be used to
decide emptiness of Streett and Buechi automata. It is the first symbolic
algorithm to compute SCC-decompositions and language emptiness in
O(n log n) rather than O(n2) symbolic steps.
Third, we consider BDD-based methods to increase the efficiency of search.
We extend guided search to LTL and CTL model checking by describing how it can
be used for greatest fixpoints and nested fixpoints. Guided search improves the
efficiency of search by selectively searching parts of the system, hence
obtaining the correct answer without ever having to represent difficult subsets.
Overall, we have improved the efficiency of LTL model checking in both
theory and practice, using a variety of methods.
|
