E. Allen Emerson

Initial Work

Working in North America in the early 1980's, Emerson, in collaboration with Edmund Clarke, originated the technical concepts of an automated quality assurance method that checks if a nominally finite state concurrent system provides a model of (i.e., satisfies) its specification. They also coined the now ubiquitous term Model Checking for the method. Working in Europe, Joseph Sifakis independently discovered a similar idea. This model checking method had several desirable characteristics:

1. it was fully automatable and algorithmic, since it entailed a systematic search of the program's state space;
2. it was precise and expressive, with a formally defined specification logic, Computation Tree Logic (CTL), that could capture a wide variety of correctness properties of interest;
3. it was efficient, having running time that is polynomial in the sizes of both the input system and the specification, partly owing to this particular logic;
4. it was very appropriate for reasoning about concurrent programs, for which traditional quality assurance methods had proven largely ineffective;
5. it was conceived from the beginning to provide a practical basis for a practical verification method.

Later Work

Emerson’s path-breaking contributions to the development of model checking include the formulation of widely used logics for flexible and expressive specifications as well as associated model checking algorithms. The expressiveness of powerful computation tree logics, as well as fixpoint logics are fundamental in both theory and practice. Arguably, expressiveness is even more basic than the efficiency for reasoning methods: if the important correctness properties cannot even be expressed, the logics are not useful for program verification. Much of the logical machinery developed by Emerson is central to most industrial specification logics and related model checking tools. As a result, the logics have been incorporated into several prominent commercial frameworks (e.g. IBM Sugar) and engineering standards for specification (e.g. Accellera-IEEE Property Specification Logic, IBM Property Specification Logic/Sugar).

The original paper [2] described the basic principles of model checking. However, it and all subsequent model checkers must contend with efficiency issues. Intuitively, the problem is that small programs can have an extremely large number of states, i.e. configurations of program variables including data values and location counters. Early model checkers typically computed every possible state of the program. This could lead to a combinatorial blowup in the size of the system state graph known by the term state explosion. For example, a concurrent system with 50 similar processes each having just 10 local states might have an astronomical 10**50 global states. As the field progressed, a number of powerful techniques were devised to ameliorate state explosion, often based on simplifying or shrinking the representation of the state graph. Consequently, the size of systems amenable to model checking has increased enormously over the years. While state explosion has not been completely vanquished, it has been largely tamed for many applications.

Interestingly, there can also be a combinatorial explosion in the size of the specification for some logics. In most cases the system size dominates, and even the exponential blow-up for a small specification in linear temporal logic might be tolerable. But in other cases the specification is large, resulting in a substantial (exponential or worse) blow-up that is not workable. Emerson's work addresses efficiency in both the system size and the specification size. An advantage of using logics such as CTL is that the cost of model checking is linear in the size of the specification.

Another line of Emerson's work has been an examination of a key component of some model checking approaches. This involved applying fixpoint logics to check non-emptiness of automata on infinite objects and calculate winning strategies for games between an open system and its environment. These have applications to model checking multi-agent systems. Work at the Weizmann Institute similarly employed computation tree logics for automatic program design, and more recently for compositional reasoning.

Emerson has also made highly innovative and influential advances in techniques for limiting state explosion. One technique exploits the redundancy that results from the symmetry inherent in systems comprised of many copies of similar sub-components. This allows large systems to be converted into much smaller systems, permitting dramatic increases in the speed and capacity of model checkers. Symmetry reduction permits reasoning about a large model using an exponentially reduced model. Many model checking tools incorporate symmetry reduction, including Rulebase from IBM. Emerson has also been a pioneer in combining reductions with other means of combating state explosion, such as symmetry reduction with symbolic model representations, or symmetry reduction with partial order reduction.

Another approach solves many important cases of the parameterized model checking problem, where one must establish correctness for systems comprised of n sub-components, for all n. Emerson has used these techniques to algorithmically verify an unboundedly long automotive data protocol for Motorola, and to verify arbitrarily large systems of common cache protocols.