Computer Science PhD Candidate

8/3/2001

1:00pm-3:00pm

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(n^{2}) 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, ProfessorHarold (Hal) Gabow, ProfessorGary Hachtel, Department of Electrical and Computer EngineeringOrna Kupferman, Hebrew University |

Department of Computer Science

University of Colorado Boulder

Boulder, CO 80309-0430 USA

webmaster@cs.colorado.edu

University of Colorado Boulder

Boulder, CO 80309-0430 USA

webmaster@cs.colorado.edu