Search techniques and automata for symbolic model checking

Model checking addresses correctness of finite-state systems by formal methods. It automatically either proves the user-defined properties of the system correct, or refutes them. The algorithms involve searching very large graphs and are memory and time intensive. In our application, we use BDD-based symbolic methods that consider sets of nodes at a time; Checking whether a model satisfies a Linear-Time Logic (LTL) formula proceeds as follows. The formula is translated into a Büchi automaton, then the product of the automaton and the model under scrutiny is taken, and finally it is tested whether the language of the automaton is empty or not. From the latter check it is determined whether the formula is correct, and if not, a counterexample is produced.; We address the size of the Büchi 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 optimizations of the automaton. The resulting automaton is significantly smaller than the automata produces by previously known methods. Using boolean optimization, we present a translation methods that is optimal within a broad class of algorithms.; We improve the language-emptiness cheek 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 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 Büchi automata. Using simultaneous forward and backward searches, 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 directly addressing the efficiency of the representation. By selectively searching parts of the system it can obtain the correct answer without ever having to represent difficult subsets.