home · mobile · calendar · defenses · 2001-2002 · 

Thesis Defense - Bloem

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.

Committee: Fabio Somenzi, Department of Electrical and Computer Engineering (Chair)
Andrzej Ehrenfeucht, Professor
Harold (Hal) Gabow, Professor
Gary Hachtel, Department of Electrical and Computer Engineering
Orna Kupferman, Hebrew University
Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:20)