@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Symmetry and Induction in Model Checking)
@heading(CMU-CS-96-202)
@center(@b(Somesh Jha))
@center(October 1996 - Ph.D. Thesis)
@center(FTP: Unavailable)
@blankspace(1)
@begin(text,spacing=1)

With the increasing complexity of digital systems, 
testing of digital systems is becoming increasingly important.
Perhaps, the most popular method for testing hardware is simulation.
The incompleteness of simulation based testing methods has spurred the
recent surge in the research on formal verification.  In formal
verification, one builds a precise model of the hardware under
scrutiny and proves that the model satisfies a specification of
interest.  For example, suppose one wants to verify that a router chip
does not deadlock. In this case the user will build a precise model of
the router and the specification will express the property of deadlock
freedom.  The two approaches to formal verification are @i{model
checking} and @i{theorem proving}. In this thesis we will only
discuss model checking.  Most model checking procedures suffer from
the @i{state explosion problem}, i.e., the size of the state space
of the system can be exponential in the number of state variables of
the system.  For certain systems, exploiting the inherent symmetry can
alleviate the state-explosion problem.  We discuss Model Checking
procedures which exploit symmetry. Current model checkers can only
verify a single state-transition system at a time. We also want to
extend the model checking techniques to handle infinite families of
finite-state systems.

In practice, finite state concurrent systems often exhibit
considerable symmetry. We investigate techniques for reducing the
complexity of temporal logic model checking in the presence of
symmetry. In particular, we show that symmetry can frequently be used
to reduce the size of the state space that must be explored during
model checking. We also investigate complexity of various problems
related to exploiting symmetry in model checking. Partial order based
reduction techniques exploit independence of actions. We demonstrate
that partial order and symmetry based reduction techniques can be
applied simultaneously.

The ability to reason automatically about entire families of similar
state-transition systems is an important research goal.  Such families
arise frequently in the design of reactive systems in both hardware
and software.  The infinite family of token rings is a simple example.
More complicated examples are trees of processes consisting of one
root, several internal and leaf nodes, and hierarchical buses with
different numbers of processors and caches. A technique for verifying
entire families of state-transition systems based on network grammars
and process invariants is presented here.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Formal verification, temporal logic, CTL, model checking,
mu-calculus, symmetry, induction, partial order>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(194 pages)])