Rajeev Alur

*Rajeev Alur, Zisman Family Professor of computer and Information Science at the University of
Pennsylvania, has won the 2024 Donald E. Knuth Prize for outstanding contributions to the
foundations of computer science for his introduction of novel models of computation which
provide the theoretical foundations for analysis, design, synthesis, and verification of computer
systems.*

Over the past thirty years, Alur has introduced several novel models of computation that provide the theoretical foundations for analysis, design, synthesis, and verification of computer systems. While rooted in algorithms and logic, his research, with over 52,000 citations, has found applications in control theory, cyber-physical systems, multi-agent systems, and program synthesis. The specific contributions listed below are highlights of his high-impact, seminal contributions to the foundations of computer science, for which he is recognized with the 2024 Knuth Prize.

**Timed Automata:** Classical model checking was developed for the analysis of finite-state
discrete systems. In a ground breaking paper in ICALP 1991, Alur and Dill introduced an
extension of automata with continuous timers. They proposed an algorithm to analyze the
resulting infinite-state systems by introducing a novel notion of time-abstract bisimulation for
algorithmic construction of finite-state quotients. This framework of timed automata has
become the standard formal model for real-time systems inspiring a lot of research in
specification logics, verification algorithms, formal language theory, and control theory. Problems
such as "does a communication protocol deadlock?" and "synthesize the most general controller
to maintain safety", in the presence of timing constraints, can be formulated and solved using
decision problems on timed automata. These algorithms have been implemented in many tools
and applied to debugging real-world examples. Their work on timed automata is one of
the most highly cited papers in theoretical computer science: the TCS’95 journal version has
now over 10K citations. For this work, Alur and Dill were awarded the inaugural Computer-Aided
Verification (CAV) award in 2008 and the inaugural Alonzo Church Award for outstanding
contributions in logic and computation in 2016.

**Real-time Temporal Logics:**
A related line of research concerns extensions of temporal logics
to specify real-time requirements. This work provides a foundational study of different variants
based on the modalities used (branching time versus linear-time), the underlying semantics for
time (dense versus discrete), and the primitives allowed in syntax for expressing timing
constraints. In a sequence of papers, Alur and coauthors identified the syntactic and semantic
restrictions necessary for decidability and developed optimal model-checking algorithms
whenever possible. Important articles in this series include "Model checking of real-time
systems" [Alur, Courcoubetis, Dill; LICS’90 and I&C’93; winner of LICS Test-of-Time Award in
2010]; "A really temporal logic" [Alur and Henzinger; FOCS’89 and JACM’94] and "Benefits of
relaxing punctuality” [Alur, Feder, Henzinger; PODC’91 and JACM’96].

**Hybrid Automata:**
Embedded systems, such as controllers in automotive, medical, and
avionics systems, consist of a collection of interacting software modules reacting to and
controlling an analog environment. The discipline of hybrid systems that combines the discrete
and continuous modeling principles is proving to be crucial in systematic design and analysis of
safety-critical embedded systems. Alur’s work, in collaboration with Henzinger, introducing
"hybrid automata" and symbolic verification algorithms for hybrid automata, was the first to
formalize the computation model for hybrid systems, and led to the development of model
checkers for hybrid systems. This work shows how symbolic algorithms manipulating polyhedra
can be effectively used for analysis of differential equations and inspired a substantial amount of
follow-up research both in the formal methods and control-theory communities. Highly influential
papers include “The algorithmic analysis of hybrid systems" [TCS’95 ], “Automatic symbolic
verification of embedded systems" [TSE’96], and “Discrete abstractions of hybrid systems”
[Proc. IEEE, 2000]. The modeling concepts in hybrid automata have been incorporated in
industrial standard modeling tools such as Simulink, Modelica, and LabVIEW.

**Strategic Reasoning for Multi-agent Systems:**
Alternating-time Temporal Logic (ATL) [Alur,
Henzinger, Kupferman; FOCS’97 and JACM’02] is a strategic-theoretic language for specifying
and reasoning about the objectives of individual agents and teams of agents from a
game-theoretic perspective. This work provides a rigorous analysis of decidability
and complexity for different logical fragments based on the nature of interaction among agents
(synchronous vs asynchronous) and observability. Reactive Modules [Alur and Henzinger;
LICS’96 and FMSD’99] is an executable and compositional modeling formalism to formally
describe the interaction between multiple heterogeneous components supported by
assume-guarantee rules for reasoning. These papers were the catalyst for extensive research
on game-theoretic view for design and analysis of multi-agent systems in formal verification,
control theory, and AI planning. The JACM’02 ATL paper won the AAMAS Influential Paper
Award in 2021.

**Visibly-Pushdown Languages:** Alur and Madhusudan introduced the model of “Nested words"
for representation of data with both a linear order and a hierarchically nested matching of items
[“Visibly pushdown languages'', STOC’04 and JACM’09]. Nested words generalize both words
and ordered trees and allow both word and tree operations. Nested-word automata (also known
as Visibly-Pushdown Automata), are finite-state acceptors defining the class of regular
languages of nested words. This class has most of the appealing theoretical properties
that the classical regular word languages enjoy. For example, deterministic nested word
automata are as expressive as their nondeterministic counterparts; the class is closed under
many operations; membership, emptiness, language inclusion, and language equivalence are
all decidable; and definability in monadic second order logic corresponds exactly to finite-state
recognizability. This theory provides a new basis for algorithmic verification of structured
programs: instead of viewing the program as a context-free language over words, one can view
it as a regular language of nested words, and this allows model checking of many properties
(such as stack inspection) that are not expressible in existing specification logics leading to new
program analysis tools.

**Program Synthesis:**
Alur and collaborators introduced the problem of syntax-guided
synthesis—now known as SyGuS, along with search-based algorithmic solutions, as a unifying
framework for synthesizing program fragments that meet logical specifications [“Syntax Guided
Synthesis”, FMCAD’13]. This paradigm was a core contribution of the NSF Expeditions in
Computing project ExCAPE led by Alur. Search-based program synthesis is now a mainstream
foundational topic in programming languages with an annual competition of
solvers, leading to end-user programming tools being developed at companies such as AWS,
Google, and Microsoft.

**Leadership, Education, and Mentoring:**
Prof. Alur is a senior leader in the areas of formal
methods and logic in computer science and has served as program and/or general chairs of
prominent conferences such as LICS, CAV, and FLoC. He has also played a crucial role in
establishing cyber-physical systems (CPS) as a distinct academic discipline at the intersection
of control theory, embedded software, and formal methods. He (co)chaired early meetings on
this topic — hybrid systems workshop (1995), EMSOFT (2003), and HSCC (2004), and served
as the General Chair of the newly formed ACM Special Interest Group in Embedded Systems
(SIGBED). He is the author of the textbook “Principles of Cyber-physical Systems” [MIT Press,
2015]. Formal methods for CPS have now found acceptance in tools and applications at
industries such as Mathworks and Toyota. Alur has advised 45 doctoral and post-doctoral
students. Notable alumni include S. Bansal (Georgia Tech), P. Černý (TU Vienna), S. Chaudhuri
(UT Austin), L. D’Antoni (Wisconsin), J. Deshmukh (USC), R. Grosu (TU Vienna), K. Mamouras
(Rice), M. Parthasarathy (UIUC), M. Raghothaman (USC), C. Stanford (UC Davis), A. Trivedi
(Colorado), and B.-Y. Wang (Academia Sinica, Taiwan).

Prize Committee:

Edith Cohen (Google/Tel Aviv U.)

David Eppstein (Chair, UC Irvine)

Monika Henzinger (IST Austria)

Kurt Mehlhorn (Max Planck Institute)

Salil Vadhan (Harvard U.)

Moshe Vardi (Rice U.)