Guest Post by Rance Cleavland, professor at University of Maryland
at College Park, who works in Model Checking.
Earlier this week, the ACM
announced
the winners of the 2007 ACM Turing
Award (awarded in 2008, for reasons that elude me).
They are Edmund
Clarke (CMU), Allan Emerson (U. Texas) and Joseph Sifakis (Verimag, in
France).
The award statement honors the contributions of these three to
the theory and practice of model checking, which refers to an array of
techniques for automatically determining whether models of system
behavior satisfy properties typically given in temporal logic.
After first blanching at the application of an
adjective ("temporal") to
a term ("logic") that is usually left unqualified, a Gentle Reader may
wonder what all the fuss is about. Is model checking really so
interesting and important that its discoverers and popularizers deserve
a Turing Award?
The glib answer is
of course, because the selection committee must have
a fine sense of judgment.
My aim is to convince you of a less glib
response, which is that model checking is the most fundamental advance
in formal methods for program verification since Hoare coined the term
in the 60s.
What is "model checking"?
In mathematical logic, a model is a structure
(more terminology) that makes a logical formula true. So "model
checking" would refer to checking whether a structure is indeed a model
for a given formula. In fact, this is exactly what model checking is,
although in the Clarke-Emerson-Sifakis meaning of the term, the
structures - models - are finite-state Kripke structures
(= finite-state machines, except with labels on state rather than
transitions and no accepting states), and the logical formulas
are drawn from propositional temporal logic
(= proposition logic extended with modalities for
expressing
always in the future and
eventually in the future").
The Clarke-Emerson-Sifakis algorithmic innovation was to notice
that for
certain flavors of temporal logic (
pure branching time),
model
checking could be decided in polynomial time; this is the gist of the
papers written independently in 1981 by Clarke and Emerson on the one
hand, and Sifakis and Queille on the other.
Subsequently, these results
were improved to show that model checking for pure branching-time logic
is proportional to the product of the size of the Kripke structure and
the size of the formula (often, maybe misleadingly,
called "linear time"
in the model-checking community, since the size of the model dominates
the product).
Of course, a linear-time algorithm (OK, I'm in the model-checking
community!) is only of passing interest unless it has real application.
This comment involves two questions.
-
Is the general problem one people want solved?
-
Can the algorithm produce results on the instances of the problem
people want solved?
The answer to 1 is "YES YES YES". The ability automatically to check
the correctness of a program/hardware design/communications protocol
would offer incalculable benefits to developers of these systems.
Early on, the answer to 2 for model checking was in doubt, however, for
the simple reason that the size of Kripke structure is typically
exponential in the size of the
program used to define it.
(State = assignment of values to variables, so
num-of-states is exponential in num-of-variables, etc.)
Throughout the 80s and 90s, the three winners worked
on many techniques for overcoming the
state-explosion problem:
compositional techniques, symmetry reductions, etc. One of
the most successful was
symbolic model checking:
the use of
logic formulas, rather than linked lists, etc., in the model-checking
process to represent large sets of states. While none of these
techniques proved uniformly applicable, symbolic model checking found a
home in the hardware-design community, and model-checkers are now
standard parts of the design flow of microprocessor design and
incorporated routinely in the design tools produced by companies like
Cadence, Synopsys and The MathWorks.
So what to make of the Turing Award? I would say that the algorithmic
innovation was deep and insightful, but not the source of the award.
Rather, the combination of the initial insight, together with the
persistence of the award winners in identifying engineering advances
to further the state of the practice, is what earned them their,
in my view well-deserved and maybe even over-due, prize.
