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?
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.