% abstract.tex
% Author: James Ezick
% Revised: 19 April 2004
Model checking based on validating temporal logic formulas has proven
practical and effective for numerous software engineering applications. As
systems based on this approach have become more mainstream, a need has
arisen to deal effectively with large batches of formulas over a common
model. Presently, most systems validate formulas one at a time, with
little or no interaction between validation of separate formulas. This is
the case despite the fact that, for a wide range of applications, a certain
level of redundancy between domain-related formulas can be anticipated.
This paper presents an optimizing compiler for batches of temporal logic
formulas. A component of the Carnauba model checking system, this compiler
addresses the need to handle batches of temporal logic formulas by
leveraging the framework common to optimizing programming language
compilers. Just as traditional optimizing compilers attempt to exploit
redundancy and other solvable properties in a program to reduce the demand
on a runtime system, this compiler exploits similar properties in groups of
formulas to reduce the demand on a model checking engine. Optimizations
are performed via a set of distinct, interchangeable optimization passes
operating on a common intermediate representation. The intermediate
representation captures the full modal mu-calculus, and the optimization
techniques are applicable to any temporal logic subsumed by that logic.
The compiler offers a unified framework for expressing some well understood
single-formula optimizations as well as numerous inter-formula
optimizations that capitalize on redundancy, logical implication, and,
optionally, model-specific knowledge. It is capable of working either in
place of, or as a preprocessor for, other optimization algorithms. The
result is a system that, when applied to a potentially heterogeneous
collection of formulas over a common problem domain, is able to measurably
reduce the time and space requirements of the subsequent model checking
engine.