Rajeev Alur and David Dill receive the 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation

I am happy to inform the reders of this blog that the 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given to Rajeev Alur and David Dill for their invention of timed automata, a decidable model of real-time systems, which combines a novel, elegant, deep theory with widespread practical impact. Congratulations to David and Rajeev!

David and Rajeev are honoured, in particular, for their paper:

Rajeev Alur and David Dill: A theory of timed automata. Theoretical Computer Science 126(2):183–235, 1994. Fundamental study.

That paper proposes a variation on classical finite automata to model the behaviour of real-time systems. The resulting notion of timed automata provides a strikingly simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. The fundamental study by Alur and Dill developed the model of timed automata as a formalism for accepting languages of timed words, studied the model from the perspective of formal language theory by considering closure properties and decision problems for the full model and some of its sub-classes, mapped the decidability boundary for the considered decision problems, and – as the main tool – introduced a fundamental abstraction, the so-called region graph, that has since found application in virtually every decidability result for models of real-time and hybrid systems, and that is at the heart of coarser abstractions that are embodied in the verification engines of several industrial-strength tools for automatic verification of real-time systems.

In the twenty plus years since their invention, timed automata have become the
standard model for the analysis of continuous-time systems, which underlies thousands of papers, dozens of tools, and several textbooks. This is a remarkable achievement for any formalism. It is all the more remarkable that this achievement was accompanied by an elegant theory that was already put down, in its most essential elements, in the very first paper by Alur and Dill, where they identified timed automata as one of the cases where finite-state reasoning can be extended to infinite-state systems.

As a sign of the impact of the work by David and Rajeev, it suffices to note that, according to Google Scholar,  the journal paper for which they receive the Alonzo Church Award, which was published in 1994, has so far received over 6,500 citations, whereas the ICALP 1990 on which it was based has been cited over 1,250 times. Moreover, a Google Scholar query also reveals that at least 135 publications citing their landmark TCS paper have more than 135 citations themselves.

Alur and Dill will receive the award at the 31st Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS), which will be held on July 5-8, 2016, at Columbia University, New York City, USA.

The Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or small group of papers within the past 25 years; this is the first such award. The Award Committee consisted of Catuscia Palamidessi, Gordon Plotkin, Wolfgang Thomas, and Moshe Vardi (chair).