Rajeev Alur

Last updated

Rajeev Alur Rajeev Alur FLoC 2006.jpg
Rajeev Alur

Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata (Alur and Dill, 1994) and nested words (Alur and Madhusudan, 2004).

Contents

Prof. Alur was born in Pune. He obtained his bachelor's degree in computer science from the Indian Institute of Technology Kanpur in 1987, and his Ph.D. in computer science from Stanford University in 1991. Before joining the University of Pennsylvania in 1997, he was with the Computing Science Research Center at Bell Laboratories. His research has included formal modeling and analysis of reactive systems, hybrid systems, model checking, software verification, design automation for embedded software, and program synthesis. He is a Fellow of the ACM, [1] a Fellow of the IEEE, and has served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems). He holds the title of Zisman Family Professor at UPenn since 2003. [2]


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).Knuth Prize

Awards and honors

Related Research Articles

<span class="mw-page-title-main">Finite-state machine</span> Mathematical model of computation

A finite-state machine (FSM) or finite-state automaton, finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition. Finite-state machines are of two types—deterministic finite-state machines and non-deterministic finite-state machines. For any non-deterministic finite-state machine, an equivalent deterministic one can be constructed.

In computational complexity theory, EXPSPACE is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in space, where is a polynomial function of . Some authors restrict to be a linear function, but most authors instead call the resulting class ESPACE. If we use a nondeterministic machine instead, we get the class NEXPSPACE, which is equal to EXPSPACE by Savitch's theorem.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

<span class="mw-page-title-main">Theoretical computer science</span> Subfield of computer science and mathematics

Theoretical computer science is a subfield of computer science and mathematics that focuses on the abstract and mathematical foundations of computation.

A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow and jump. Often, the term "hybrid dynamical system" is used instead of "hybrid system", to distinguish from other usages of "hybrid system", such as the combination neural nets and fuzzy logic, or of electrical and mechanical drivelines. A hybrid system has the benefit of encompassing a larger class of systems within its structure, allowing for more flexibility in modeling dynamic phenomena.

In automata theory, a hybrid automaton is a mathematical model for precisely describing hybrid systems, for instance systems in which digital computational processes interact with analog physical processes. A hybrid automaton is a finite state machine with a finite set of continuous variables whose values are described by a set of ordinary differential equations. This combined specification of discrete and continuous behaviors enables dynamic systems that comprise both digital and analog components to be modeled and analyzed.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

<span class="mw-page-title-main">Joseph Sifakis</span> Greek-French computer scientist

Joseph Sifakis is a Greek-French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking.

Dexter Campbell Kozen is an American theoretical computer scientist. He is Professor Emeritus and Joseph Newton Pew, Jr. Professor in Engineering at Cornell University.

In computer science, alternating-time temporal logic, or ATL, is a branching-time temporal logic that extends computation tree logic (CTL) to multiple players. ATL naturally describes computations of multi-agent systems and concurrent games. Quantification in ATL is over program-paths that are possible outcomes of games. ATL uses alternating-time formulas to construct model-checkers in order to address problems such as receptiveness, realizability, and controllability.

In computer science, more specifically in automata and formal language theory, nested words are a concept proposed by Alur and Madhusudan as a joint generalization of words, as traditionally used for modelling linearly ordered structures, and of ordered unranked trees, as traditionally used for modelling hierarchical structures. Finite-state acceptors for nested words, so-called nested word automata, then give a more expressive generalization of finite automata on words. The linear encodings of languages accepted by finite nested word automata gives the class of visibly pushdown languages. The latter language class lies properly between the regular languages and the deterministic context-free languages. Since their introduction in 2004, these concepts have triggered much research in that area.

<span class="mw-page-title-main">Weighted automaton</span> Finite-state machine where edges carry weights

In theoretical computer science and formal language theory, a weighted automaton or weighted finite-state machine is a generalization of a finite-state machine in which the edges have weights, for example real numbers or integers. Finite-state machines are only capable of answering decision problems; they take as input a string and produce a Boolean output, i.e. either "accept" or "reject". In contrast, weighted automata produce a quantitative output, for example a count of how many answers are possible on a given input string, or a probability of how likely the input string is according to a probability distribution. They are one of the simplest studied models of quantitative automata.

ACM SIGLOG or SIGLOG is the Association for Computing Machinery Special Interest Group on Logic and Computation. It publishes a news magazine, and has the annual ACM–IEEE Symposium on Logic in Computer Science (LICS) as its flagship conference. In addition, it publishes an online newsletter, the SIGLOG Monthly Bulletin, and "maintains close ties" with the related academic journal ACM Transactions on Computational Logic.

David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.

<span class="mw-page-title-main">Orna Kupferman</span> Israeli computer scientist

Orna Kupferman is a Professor of Computer Science and former Vice Rector at the Hebrew University of Jerusalem. She was elected to the Academia Europaea in 2016.

References

  1. "Rajeev Alur". ACM Fellows. ACM. 2007. Retrieved 23 January 2010. For contributions to the specification and verification of reactive and hybrid systems.
  2. "Zisman Family Professor of CIS: Rajeev Alur". University of Pennsylvania Almanac. Almanac, Vol. 50, No. 12, November 11, 2003. Retrieved 16 October 2021.
  3. "CAREER: Computer-Aided Verification of Reactive Systems". NSF Award Search, Award #9734115. National Science Foundation. Retrieved 16 October 2021.
  4. "The 2008 CAV Award". CAV 2008: 20th International Conference on Computer-Aided Verification . Princeton University. Retrieved 16 October 2021.
  5. "LICS Test-of-Time award". For the pioneer work in the model checking of real-time systems.
  6. "The 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation". SIGLOG . ACM Special Interest Group on Logic and Computation. Retrieved 16 October 2021.
  7. "2024 Knuth Prize: Rajeev Alur". ACM Special Interest Group on Algorithms and Computation Theory. Retrieved 8 August 2024.