In this instalment of the Process Algebra Diary, Mickael Randour and I joined forces to interview Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar and Mariëlle Stoelinga, who are some of the recipients of the CONCUR 2022 Test-of-Time award. We hope that you'll enjoy reading the very inspiring and insightful answers provided by the above-mentioned colleagues to our questions.
Note: In what follows, "Luca A." refers to me, whereas "Luca" is Luca de Alfaro.
Luca A. and Mickael: You receive the CONCUR ToT Award 2022 for your paper "The Element of Surprise in Timed Games", which appeared at CONCUR 2003. In that article, you studied concurrent, two-player timed games. A key contribution of your paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise, as they are played “faster”, and the definition of natural concepts of winning conditions for the two players — ensuring that players can win only by playing according to a physically meaningful strategy. In our opinion, this is a great example of how novel concepts and definitions can advance a research field. Could you tell us more about the origin of your model?
All: Mariëlle and Marco were postdocs with Luca at UCSC in that period, Rupak was a student of Tom's, and we were all in close touch, meeting very often to work together. We all had worked much on games, and an extension to timed games was natural for us to consider.
In untimed games, players propose a move, and the moves jointly determine the next game state. In these games there is no notion of real-time. We wanted to study games in which players could decide not only the moves, but also the instant in time when to play them.
In timed automata, there is only one “player” (the automaton), which can take either a transition, or a time step. The natural generalization would be a game in which players could propose either a move, or a time step.
Yet, we were unsatisfied with this model. It seemed to us that it was different to say “Let me wait 14 seconds and reconvene. Then, let me play my King of Spades” or “Let me play my King of Spades in 14 seconds”. In the first, by stopping after 14 seconds, the player is providing a warning that the card might be played. In the second, there is no such warning. In other words, if players propose either a move or a time-step, they cannot take the adversary by surprise with a move at an unanticipated instant. We wanted a model that could capture this element of surprise.
To capture the element of surprise, we came up with a model in which players propose both a move and the delay with which it is played. After this natural insight, the difficulty was to find the appropriate winning condition, so that a player could not win by stopping time.
Tom: Besides the infinite state space (region construction etc.), a second issue that is specific to timed systems is the divergence of time. Technically, divergence is a built-in Büchi condition ("there are infinitely many clock ticks"), so all safety and reachability questions about timed systems are really co-Büchi and Büchi questions, respectively. This observation had been part of my work on timed systems since the early 1990s, but it has particularly subtle consequences for timed games, where no player (and no collaboration of players) should have the power to prevent time from diverging. This had to be kept in mind during the exploration of the modeling space.
All: We came up with many possible winning conditions, and for each we identified some undesirable property, except for the one that we published. This is in fact an aspect that did not receive enough attention in the paper; we presented the chosen winning condition, but we did not discuss in full detail why several other conditions that might have seemed plausible did not work.
In the process of analyzing the winning conditions, we came up with many interesting games, which form the basis of many results, such as the result on lack of determinazation, on the need for memory in reachability games (even when clock values are part of the state), and most famously as it gave the title to the paper, on the power of surprise.
After this fun ride came the hard work, where we had to figure out how to solve these games. We had worked at symbolic approaches to games before, and we followed the approach here, but there were many complex technical adaptations required. When we look at the paper in the distance of time, it has this combination of a natural game model, but also of a fairly sophisticated solution algorithm.
Luca A. and Mickael: Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? If so, which of your subsequent results on (timed) games do you like best? Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising?
Luca: Marco and I built Ticc, which was meant to be a tool for timed interface theories, based largely on the insights in this paper. The idea was to be able to check the compatibility of real-time systems, and automatically infer the requirements that enable two system components to work well together – to be compatible in time. We thought this would be useful for hardware or embedded systems, and especially for control systems, and in fact the application is important: there is now much successful work on the compositionality of StateFlow/Simulink models.
We used MTBDDs as the symbolic engine, and Marco and I invented a language for describing the components and we wrote by pair-programming some absolutely beautiful Ocaml code that compiled real-time component models into MTBDDs (perhaps the nicest code I have ever written). The problem was that we were too optimistic in our approach to state explosion, and we were never able to study any system of realistic size.
After this, I became interested in games more in an economic setting, and from there I veered into incentive systems, and from there to reputation systems and to a three-year period in which I applied reputation systems in practice in industry, thus losing somewhat touch with formal methods work.
Marco: I’ve kept working on games since the award-winning paper, in one way or another. The closest I’ve come to the timed game setting has been with controller synthesis games for hybrid automata. In a series of papers, we had fun designing and implementing symbolic algorithms that manipulate polyhedra to compute the winning region of a linear hybrid game. The experience gained on timed games helped me recognize the many subtleties arising in games played in real time on a continuous state-space.
Mariëlle: I have been working on games for test case generation: One player represents the tester, which chooses inputs to test; the other player represents the System-under-Test, and chooses the outputs of the system. Strategy synthesis algorithms can then compute strategies for the tester that maximize all kinds of objectives, eg reaching certain states, test coverage etc.
A result that I really like is that we were able to show a very close correspondence between the existing testing frameworks and game theoretic frameworks: Specifications act as game arenas; test cases are exactly game strategies, and the conformance relation used in testing (namely ioco) coincides with game refinement (i.e. alternating refinement).
Rupak: In an interesting way, the first paper on games I read was the one by Maler, Pnueli and Sifakis (STACS 95) that had both fixpoint algorithms and timed games (without “surprise”). So the problem of symbolic solutions to games and their applications in synthesis followed me throughout my career. I moved to finding controllers for games with more general (non-linear) dynamics, where we worked on abstraction techniques. We also realized some new ways to look at restricted classes of adversaries. I was always fortunate to have very good collaborators who kept my interest alive with new insights. Very recently, I have gotten interested in games from a more economic perspective, where players can try to signal each other or persuade each other about private information but it’s too early to tell where this will lead.
Luca A. and Mickael: What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?
Mariëlle: Throughout my academic life, I have been working on stochastic analysis --- with Luca and Marco, we worked on stochastic games a lot. First only on theory, but later also on industrial applications, esp in the railroad and high-tech domain. At some point in time, I realized that my work was actually centred around analysing failure probabilities and risk. That is how I moved into risk analysis; the official title of the title of the chair I hold is Risk Management for High Tech Systems.
The nice thing is: this sells much better than Formal Methods! Almost nobody knows what Formal Methods are, and if they know, people think “yes, those difficult people who urge us to specify everything mathematically”. For risk management, this is completely different: everybody understands that this is an important area.
Luca: I am currently working on computational ecology, on ML for networks, and on fairness in data and ML. In computational ecology, we are working on the role of habitat and territory for species viability. We use ML techniques to write “differentiable algorithms”, where we can compute the effect of each input – such as the kind of vegetation in each square-kilometer of territory – on the output. If all goes well, this will enable us to efficiently compute which regions should be prioritized for protection and habitat conservation.
In networks, we have been able to show that reinforcement learning can yield tremendous throughput gains in wireless protocols, and we are now starting to work on routing and congestion control.
And in fairness and ML, we have worked on the automatic detection of anomalous data subgroups (something that can be useful in model diagnostics), and we are now working on the spontaneous inception of discriminatory behavior in agent systems.
While these do not really constitute a coherent research effort, I can certainly say that I am having a grand tour of CS – the kind of joy ride one can afford with tenure!
Rupak: I have veered between practical and theoretical problems. I am working on charting the decidability frontier for infinite-state model checking problems (most recently, for asynchronous programs and context-bounded reachability). I am also working on applying formal methods to the world of cyber-physical systems ---mostly games and synthesis. Finally, I have become very interested in applying formal methods to large scale industrial systems through a collaboration with Amazon Web Services. There is still a large gap between what is theoretically understood and what is practically applicable to these systems; and the problems are a mix of technical and social.
Luca A. and Mickael: You have a very strong track record in developing theoretical results and in applying them to real-life problems. In our, admittedly biased, opinion, your work exemplifies Ben Schneiderman's Twin-Win Model, which propounds the pursuit of "the dual goals of breakthrough theories in published papers and validated solutions that are ready for widespread dissemination." Could you say a few words on your research philosophy? How do you see the interplay between basic and applied research?
Luca: This is very kind for you to say, and a bit funny to hear, because certainly when I was young I had a particular talent for getting lost in useless theoretical problems.
I think two things played in my favor. One is that I am curious. The other is that I have a practical streak: I still love writing code and tinkering with “things”, from IoT to biology to web and more. This tinkering was at the basis of many of the works I did. My work on reputation systems started when I created a wiki on cooking; people were vandalizing it, and I started to think about game theory and incentives for collaboration, which led to my writing much of the code for Wikipedia analysis, and at Google, for Maps edits analysis. My work on networks started with me tinkering with simple reinforcement-learning schemes that might work, and writing the actual code. On the flip side, my curiosity too often had the better of me, so that I have been unable to pay the continuous and devoted attention to a single research field. I am not a specialist in any single thing I do or I have done. I am always learning the ropes of something I don’t quite know yet how to do.
My applied streak probably gave me some insight on which problems might be of more practical relevance, and my frequent field changes have allowed me to bring new perspectives to old problems. There were not many people using RL for wireless networks, there are not many who write ML and GPU code and also avidly read about conservation biology.
Rupak: I must say that Tom and Luca were very strong influencers for me in my research: both in problem selection and in appreciating the joy of research. I remember one comment of Tom, paraphrased as “Life is short. We should write papers that get read.” I spent countless hours in Luca’s office and learnt a lot of things about research, coffee, the ideal way to make pasta, and so on.
Marco: It was an absolute privilege to be part of the group that wrote that paper (my 4th overall, according to DBLP). I’d like to thank my coauthors, and Luca in particular, for guiding me during those crucially formative years.
Mariëlle: I fully agree!
Luca A. and Mickael: Several of you have high-profile leadership roles at your institutions. What advice would you give to a colleague who is about to take up the role of department chair, director of a research centre, dean or president of a university? How can one build a strong research culture, stay research active and live to tell the tale?
Luca: My colleagues may have better advice; my productivity certainly decreased when I was department chair, and is lower even now that I am the vice-chair.
When I was young, I was ambitious enough to think that my scientific work would have the largest impact among the things I was doing. But I soon realized that some of the greatest impact was on others: on my collaborators, on the students I advised, who went on to build great careers and stayed friends, and on all the students I was teaching. This awareness serves to motivate and guide me in my administrative work. The CS department at UCSC is one of the ten largest in the number of students we graduate, and the time I spend on improving its organization and the quality of the education it delivers is surely very impactful. My advice to colleagues is to consider their service not as an impediment to research, but as one of the most impactful things they do.
My way of staying alive is to fence off some days that I only dedicate to research (aside from some unavoidable emergency), and also, to have collaborators that give me such joy in working together that they brighten and energize my whole day.
Luca A. and Mickael: Finally, what advice would you give to a young researcher who is keen to start working on topics related to concurrency theory today?
Luca: Oh that sounds very interesting! And, may I show you this very interesting thing we are doing in Jax to model bird dispersal? We feed in this climate and vegetation data, and then we…
Just kidding. Just kidding. If I come to CONCUR I promise not to lead any of the concurrency yearlings astray. At least I will try.
My main advice would be this: work on principles that allow correct-by-design development. If you look at programming languages and software engineering, the progress in software productivity has not happened because people have become better at writing and debugging code written in machine language or C. It has happened because of the development of languages and software principles that make it easier to build large systems that are correct by construction.
We need the same kind of principles, (modeling) languages, and ideas to build correct concurrent systems. Verification alone is not enough. Work on design tools, ideas to guide design, and design languages.
Tom: In concurrency theory we define formalisms and study their properties. Most papers do the studying, not the defining: they take a formalism that was defined previously, by themselves or by someone else, and study a property of that formalism, usually to answer a question that is inspired by some practical motivation. To me, this omits the most fun part of the exercise, the {\it defining} part. The point I am trying to make is not that we need more formalisms, but that, if one wishes to study a specific question, it is best to study the question on the simplest possible formalism that exhibits exactly the features that make the question meaningful. To do this, one often has to define that formalism. In other words, the formalism should follow the question, not the other way around. This principle has served me well again and again and led to formalisms such as timed games, which try to capture the essence needed to study the power of timing in strategic games played on graphs. So my advice to a young researcher in concurrency theory is: choose your formalism wisely and don't be afraid to define it.
Rupak: Problems have different measures. Some are practically justified (“Is this practically relevant in the near future?”) and some are justified by the foundations they build (“Does this avenue provide new insights and tools?”). Different communities place different values on the two. But both kinds of work are important and one should recognize that one set of values is not universally better than the other.
Mariëlle: As Michael Jordan puts it: Just play. Have fun. Enjoy the game.
