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.
Rajeev Alur and David Dill: A Theory of Timed Automata. Theoretical Computer Science 126(2):183–235, 1994.
Description of the contribution
Rajeev Alur and David Dill being handed over the Church Award by Prakash Panangaden
The nominated 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.
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 Goedel 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).