This years Turing Award: Model Checking

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.

1. Is the general problem one people want solved?
2. 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.