I am delighted to post Nathalie Bertrand's splendid interview with CONCUR 2021 Test-of-Time Award recipients Ahmed Bouajjani and Javier Esparza. (Ahmed and Javier receive the award for a paper their co-authored with the late Oded Maler.)
Thanks to Ahmed and Javier for their answers and to Nathalie for conducting such an interesting interview, which is rich in information on the technical context for, and impact of, their work as well as on their research collaborations over the years. I now leave the floor to Nathalie and her interviewees. Enjoy!
This post is devoted to the interview I was honored to conduct with Ahmed Bouajjani and Javier Esparza for their paper with Oded Maler on reachability in pushdown automata.
Nathalie: You receive the CONCUR ToT Award 2021 for your paper with Oded Maler Reachability Analysis of Pushdown Automata: Application to Model-Checking, which appeared at CONCUR 1997. In that article, you develop symbolic techniques to represent and manipulate sets of configurations of pushdown automata, or even of the broader class of alternating pushdown systems. The data structure you define to represent potentially infinite sets of configurations is coined alternating multi-automata, and you provide algorithms to compute the
set of predecessors (pre*) of a given set of configurations. Could you briefly explain to our readers what alternating multi-automata are?
Ahmed: The paper is based on two ideas. The first one is to use finite automata as a data structure to represent infinite sets of configurations of the pushdown automaton. We called them multi-automata because they have multiple initial states, one per control state of the pushdown automaton, but there is nothing deep there. The second idea is that this representation is closed under the operation of computing predecessors, immediate or not. So, given a multi-automaton representing a set of configurations, we can compute another multi-automaton representing all their predecessors. If you compute first the immediate predecessors, then their immediate predecessors, and so on, you don't converge, because your automata grow bigger and bigger. The surprising fact is that you can compute all predecessors in one go by just adding transitions to the original
automaton, without adding any new states. This guarantees termination. Later we called this process ``saturation''.
Once you can compute predecessors, it is not too difficult to obtain a model-checking algorithm for LTL model checking. But for branching-time logics you must also be able to compute intersections of sets of configurations. That's where alternation kicks in, we use it to represent intersections without having to add new states.
Nathalie: Could you also tell us how you came to study the question addressed in your award-winning article? Which of the results in your paper did you find most surprising or challenging?
Javier: In the late 80s and early 90s many people were working on symbolic model-checking, the idea of using data structures to compactly represent sets of configurations. BBDs for finite-state model-checking were a hot topic, and for quite a few years dominated CAV. BDDs can be seen as acyclic automata, and so it was natural to investigate general finite automata as data structure for infinite-state systems. Pierre Wolper and his group also did very good work on that.
About your second question, when I joined the team Ahmed and Oded had already been working on the topic for a while, and they had already developed the saturation algorithm. When they showed it to me I was blown away, it was so beautiful. A big surprise.
Nathalie: In contrast to most previous work, your approach applied to model checking of pushdown systems treats in a uniform way linear-time and branching time logics. Did you apply this objective in other contributions?
Javier: I didn't. The reason is that I was interested in concurrency, and when you bring together concurrency and procedures even tiny fragments of branching-time logics become undecidable. So I kind of stuck to the linear-time case. Did you work on branching-time, Ahmed?
Ahmed: Somehow yes (although it is not precisely about linear vs. branching time properties), in the context of Regular Model Checking, a uniform framework for symbolic analysis of infinite-state systems using automata-based data structures. There, we worked on two versions, one based on word automata for systems where configurations can be encoded as words or vectors of words, such as stacks, queues, etc., and another one based on tree automata for configurations of a larger class of systems like heap manipulating programs, parametrized systems with tree-like architectures, etc. The techniques we developed for both cases are based on the same principles.
Nathalie: As it is often the case, the paper leaves some open questions. For instance, I believe, the precise complexity of verification of pushdown systems against CTL specifications is PSPACE-hard and in EXPTIME. Did you or others close this gap since? Did your techniques help to establish the precise complexity?
Ahmed: In our paper we showed that model checking the alternating modal
mu-calculus is EXPTIME-hard. CTL is less expressive, and it was the most popular logic in the verification community at the time, so it was natural to ask if it had lower complexity.
Javier: Yes, as a first step in the paper we showed that a fragment of CTL, called EF, had PSPACE complexity. But I made a mistake in the proof, which was later found by Igor Walukiewicz. Igor cracked the problem in a paper at FSTTCS'00. It turns out that EF is indeed PSPACE-complete (so at least we got the result right!), and full CTL is EXPTIME-complete. I wish Igor had used our technique, but he
didn't, he applied the ideas of his beautiful CAV'96 paper on parity pushdown games.
Nathalie: It is often interesting to understand how research collaborations start as it can be inspiring to PhD students or colleagues. Could you tell us how you started your collaboration on the award-winning paper? Did you continue working together (on a similar topic or on something totally different) after 1997?
Ahmed: Javier and I first met in Liege for CAV 95. French universities have this program that allows us to bring foreign colleagues to France for a month as invited professors, and I invited Javier to Grenoble in 96.
Javier: It was great fun; Verimag was a fantastic place to do verification, we both liked cinema, Ahmed knew all restaurants, and the Alps were beautiful. Ahmed invited me again to Grenoble in 97. This time I came with my wife, and we again had a great time.
When I arrived in Grenoble in 96 Ahmed and Oded had already written most of the work that went into the paper. My contribution was not big, I only extended the result to the alternation-free mu-calculus, which was easy, and proved a matching lower bound. I think that my main contribution came after this paper. Ahmed and Oded were too modest, they thought the result was not so important, but I found it not only beautiful, I thought it'd be great implement the LTL part,
and build a model checker for programs with procedures. We could do that thanks to Stefan Schwoon, who started his PhD in Munich around this time--he is now at Paris-Saclay---and was as good a theoretician as a tool builder. Around 2000 he implemented a symbolic version of the algorithms in MOPED, which was quite successful.
Ahmed: In 99 I moved to LIAFA in Paris, and I remember your kids were born.
Javier: Yes, you sent my wife beautiful flowers!
Ahmed: But we kept in touch, and we wrote a paper together in POPL'03 with my PhD student Tayssir Touili, now professor in Paris. We extended the ideas of the CONCUR paper to programs with both procedures and concurrency. Other papers came, the last in 2008.
Javier: And Ahmed is visiting Munich next year, pandemic permitting, so I hope there'll be more.
Nathalie: How would you say this award-winning paper influenced your later work? Did any of your subsequent research build explicitly on it?
Ahmed: This paper was the first of many I have co-authored on verification of infinite-state systems using automata. All of them use various automata classes to represent sets of configurations, and compute reachable configurations by iterative application of automata operations. We call these procedures accelerations; instead of computing a fixed point of a function by repeated iteration, you "jump" to the fixed point after finitely many steps, or at least converge faster. Accelerations were implicitly present in the CONCUR'97 paper. They have been also used by many other authors, for example Bernard Boigelot and Pierre Wolper.
My first paper on accelerations was with Peter Habermehl, my PhD student at the time and now at IRIF. We worked on the verification of systems communicating through queues, using finite automata with Presburger constraints as data structure. Then came several works on communicating systems with my student Aurore Annichini and Parosh Abdulla and Bengt Jonsson from Uppsala. As a natural continuation, with the Uppsala group and my student Tayssir Touili we developed the framework of Regular Model Checking. And then, with Peter Habermehl, Tomas Vojnar and Adam Rogalewicz from TU Brno, we extended Regular Model Checking to Abstract Regular Model Checking, which proved
suitable and quite effective for the analysis of heap manipulating programs.
We also applied the CONCUR'97 results to the analysis of concurrent programs. The first work was a POPL'03 paper with Javier, Tayssir, and me on an abstraction framework. Two years later, Shaz Qadeer and Jakob Rehof proposed bounded-context switch analysis for bug detection. That paper created a line of research, and we contributed to it in many ways, together with Shaz, Mohamed Faouzi Atig, who was my student then, and is now Professor at Uppsala, and others.
Javier: The CONCUR'97 paper was very important for my career. As I said before, it directly led to MOPED, and later to jMOPED, a version of MOPED for Java programs developed by Stefan Schwoon and Dejvuth Suwimonteerabuth. Then, Tony Kucera, Richard Mayr, and I asked ourselves if it was possible to extend probabilistic verification to pushdown systems, and wrote some papers on the topic, the first in LICS'04. This was just the right moment, because at the same time Kousha Etessami and Mihalis Yannakakis started to write brilliant papers on recursive Markov chains, an equivalent model. The POPL'03 paper with Ahmed and Tayssir also came, and it triggered my work on Newtonian program analysis with two very talented PhD students, Stefan Kiefer, now in Oxford, and Michael Luttenberger, now my colleague at TUM. So the CONCUR'97 paper was at the root of a large part of my work of the next 15 years.
Nathalie: Is there any result obtained by other researchers that builds on your work and that you like in particular or found surprising?
Javier: After implementing MOPED, Stefan worked with Tom Reps on an extension to weighted pushdown automata, the Weighted Pushdown Library. Tom and Somesh Jha also found beautiful applications to security. This was great work. I was also very impressed by the work of Luke Ong and his student Matthew Hague. In 97 Ahmed and I tried to apply the saturation method to the full mu-calculus but failed, we thought it couldn't be done. But first Thierry Cachat gave a saturation algorithm for Büchi pushdown games, then Luke, Matthew cracked the mu-calculus problem, and then they even extended it to
higher-order pushdown automata, together with Arnaud Carayol, Olivier Serre, and others. That was really surprising.
Ahmed: I agree. I'd also mention Qadeer and Rehof's TACAS'05 paper. They built on our results to prove that context-bounded analysis of concurrent programs is decidable. They initiated a whole line of research.
Nathalie: 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?
Javier: Ten years ago I've had said the complexity of the reachability problem for Petri nets and of solving parity games, but now the first one is solved and the second almost solved! Now I don't have a specific problem, but in the last years I've been working on parameterized systems with an arbitrary number of agents, and many aspects of the theory are still very unsatisfactory. Automatically proving a mutual exclusion algorithm correct for a few processes was already routine 20 years ago, but proving it for an arbitrary number is still very much an open problem.
Ahmed: I think that invariant and procedure summary synthesis will remain hard and challenging problems that we need to investigate with new approaches and techniques. It is hard to discover the right level of abstraction at which the invariant must be expressed, which parts of the state are involved and how they are related. Of course the problem is unsolvable in general but finding good methodologies on how to tackle it depending on the class of programs is an important issue. I think that the recent emergence of data-driven approaches is
promising. The problem is to develop well principled methods combining data-driven techniques and formal analysis that are efficient and that offer well understood guarantees.
Nathalie: Would you have an anecdote or a tip from a well-established researcher to share to PhD students and young researchers?
Javier: Getting this award reminded me of the conference dinner at CAV 12 in St. Petersburg. I ended up at a table with some young people I didn't know. The acoustics was pretty bad. When the CAV Award was being announced, somebody at the table asked "What's going on?", and somebody else answered "Not much, some senior guys getting some award". Never take yourself very seriously ...
Nathalie: Oded Maler passed away almost 3 years ago. Do you have any memory of him to share with our readers?
Ahmed: Oded was very amused by the number of citations. He used to say "Look at all the damage we've done."
Javier: Yes, Oded had a wonderful sense of humor, very dry and deadpan. When I arrived in Grenoble it took me a few days to learn how to handle it! I miss it very much.
No comments:
Post a Comment