Amazon Scholar Rupak Majumdar recently won the 2022 International Conference on Concurrency Theory (CONCUR) Test-of-Time Award for his 2003 paper, “The Element of Surprise in Timed Games.”
The award recognizes outstanding papers published at the CONCUR conference. This year’s awards were selected from papers written between 1998 and 2003 that have made continual contributions to research in a specific area of concurrent programming.
Majumdar’s paper was coauthored with Luca de Alfaro, professor of computer science and engineering at UC Santa Cruz; Marco Faella, associate professor of electrical engineering and information technologies at University of Naples; Thomas A. Henzinger, president of the Institute of Science and Technology in Austria; and Mariëlle Stoelinga, a full professor at Universiteit Twente. It introduced a model that accounts for timing constraints in concurrent two-person games. This model and its analysis algorithm have become standard in formal analysis of cyber-physical systems.
“Part of our contribution was to come up with a game model where we pick times and actions together,” said Majumdar. “The second part was: Given that you have this game model, how do you actually analyze these games? So those were the two parts of the paper: the game model and an analysis algorithm.”
We both developed the model and figured out a way to get this kind of symbolic algorithm that rules out undesirable ways of winning. This became very standard in the analysis of time systems.
The paper was among the first to provide a way to solve a fundamental problem in compositional reasoning at the time: the creation of a two-person game model that cleanly incorporates the notion of time constraints. The algorithm the coauthors developed accounted for Zeno phenomena, a method of winning that involves an infinite number of moves in a finite time interval.
“One of the crucial points of the algorithm was to ensure that we rule out these kinds of Zeno behaviors,” Majumdar said. “So we both developed the model and figured out a way to get this kind of symbolic algorithm that rules out undesirable ways of winning. This became very standard in the analysis of time systems.”
Majumdar received his bachelor’s in computer science from the Indian Institute of Technology at Kampur before moving to the United States to pursue his PhD in computer science. At the University of California at Berkeley, he collaborated on the CONCUR paper with his advisor Henzinger, as well as de Alfaro, Faella, and Stoelinga, who were at the University of California, Santa Cruz, at the time.
Majumdar earned his PhD in 2003 and worked as an assistant professor at UCLA for six years. In 2009, he was named a scientific director at the Max Planck Institute for Software Systems in Kaiserslautern, Germany. Now in his 13th year at the Max Planck Institute, Majumdar has been continuing his work on formal analysis of cyber-physical systems.
“For example, we are trying to formally verify or synthesize code that ensures a robot reaches a certain point without bumping into any obstacles,” said Majumdar. “And the kind of work that we are doing is bringing together ideas from computer science, like abstraction or solving two-player games on graphs, and applying it to this world of cyber-physical systems.”
In October 2021, Majumdar was recruited as an Amazon Scholar by Byron Cook, Amazon Web Services (AWS) Automated Reasoning Group vice president and distinguished scientist. As part of the Automated Reasoning Group, Majumdar works on building automated tools that verify implementations of AWS software.
“This was a very nice opportunity to see how well these algorithms that I’ve been working on fare in the real world,” said Majumdar. “When we design these algorithms, at the back of our minds, we always want them to be useful.”
