Wednesday, December 15, 2021

Call for Invited Talk Nominations: 7th Highlights of Algorithms conference (HALG 2022)

On behalf of Keren Censor-Hillel, PC chair for HALG 2022, I am happy to post the call for invited talk nominations for that event. I encourage all members of the algorithms community to submit their nominations. HALG has rapidly become a meeting point for that community in a relaxed workshop-style setting. 

Call for Invited Talk Nominations
7th Highlights of Algorithms conference (HALG 2022)
LSE London, June 1-3, 2022

The HALG 2022 conference seeks high-quality nominations for invited talks that will highlight recent advances in algorithmic research appearing in a paper in 2021 or later.
To nominate, please email the following information in plaintext only:

  • Basic details: title of paper, authors, conference/arxiv links, suggested speaker.
  • Brief justification: Focus on the benefits to the audience, e.g., quality of results, importance/relevance of topic, clarity of talk, speaker’s presentation skills.

Nominations will be reviewed by the Program Committee to select speakers that will be invited to the conference.
Nomination deadline: January 14, 2022
Please go to for general information on HALG and for information about previous HALG meetings.
Keren Censor-Hillel
PC chair for HALG 2022

Tuesday, December 14, 2021

Faculty positions in Computer Science at Reykjavik University

The Department of Computer Science at Reykjavik University invites applications for full-time, permanent faculty positions at any rank in the fields of Software Engineering, and Design and Development of Computer Games. Outstanding candidates in other areas of Computer Science are encouraged to apply as well. 

We are looking for energetic, highly qualified academics with a proven international research record and excellent potential in their field of study. The primary evaluation criterion is scientific quality. We particularly welcome applications from researchers who have a strong network of research collaborators, can strengthen internal collaborations within the department, have the proclivity to improve their academic environment and its culture, and generally have potential to flourish in our environment.

Apart from developing their research career, the successful applicants will play a full part in the teaching and administrative activities of the department, teaching courses and supervising students at both graduate and undergraduate level. Applicants with a demonstrated history of excellence in teaching are preferred. Salary and rank are commensurate with experience. Among other benefits, Reykjavik University offers its research staff the option to take research semesters (sabbaticals) after three years of satisfactory teaching and research activity. The positions are open until filled, with intended starting date in August 2022. Later starting dates can be negotiated. 

The deadline for applications is January 30, 2022. The review of the applications will begin in late January 2022, and will continue until the positions are filled.

See here for full details and information on how to apply. 

Near-Optimal Distributed Degree+1 Colouring

If you are interested in graph colouring, and specifically in distributed algorithms for that classic problem, I strongly recommend the recent paper posted by Magnús M. Halldórsson, Fabian Kuhn, Alexandre Nolin and Tigran Tonoyan. (For the record, three of the authors work, or have worked, in my department at Reykjavik University, so I am biased.) 

The above-mentioned paper addresses the problem of finding a proper colouring of a graph when each node v has a palette of degree(v)+1 colours at its disposal. The paper resolves an open problem in distributed colouring and simplifies known results in doing so. As a byproduct of their results, the authors obtain improved streaming and sub-linear time algorithms. See the paper for much more information on the context for this result and the technical details. 

Congratulations to the authors!

Saturday, December 04, 2021

TheoretiCS: A new open-access journal in Theoretical Computer Science

I am delighted to share with all the readers of this blog the news of the launch of TheoretiCS, a new, top-quality, open-access journal dedicated to the whole of Theoretical Computer Science. The journey leading to the establishment of this new journal has been long and the fact that this path eventually reached its destination is due to the sterling efforts and foresight of a number of people within our community. The seeds of TheoretiCS were sown within the Council of the European Association for Theoretical Computer Science during my two terms as president of that association. At that time, Jos Baeten and Antonin Kucera worked hard to try and set up an open-access journal of the association. That journal never saw the light of day, but the process that eventually led to TheoretiCS was afoot. After some time, Thomas Schwentick took the baton in the relay race and took decisive steps in turning the establishment of this new journal into a true community effort. It is fair to say that the launch of this journal has involved an unprecedented level of cooperation amongst representatives of leading conferences from across the entire Theoretical Computer Science community. I am immensely grateful to everyone who participated in that work for the effort they put into making TheoretiCS a reality and apologise for not mentioning all the colleagues who contributed explicitly in this post. You can find more information on TheoretiCS in the text below, which I received from Jos Baeten, founding member-at-large of the Advisory Board of the Theoretics Foundation. 

So, what can you do to support this new journal? There are at least two things that each of us can do and that I believe are important. 

  1. Help TheoretiCS reach its quality objectives by submitting your best work to it and by encouraging your colleagues to do so too. TheoretiCS aims at publishing articles of a very high quality, and at becoming a reference journal on par with the leading journals in the area. To be accepted, a paper must make a significant contribution of lasting value to a relevant area of TCS, and its presentation must be of high quality. This is elaborated upon in the guiding principles spelled out below. I let you reach your own conclusions about the quality and the breadth of the editorial board of TheoretiCS, which is stellar IMHO.
  2. Spread the news of the launch of TheoretiCS within your networks. Despite its many years of existence and the role it plays within our community, I still meet colleagues (even in Theoretical Computer Science) who do not know that LIPIcs exists and who claim that publishing conference proceedings with commercial publishers is a sign of scientific quality. 

If you happen to be in a position to do so, you can support the TheoretiCS foundation, which is a German not-for-profit organization, by making a donation. 

I look forward to seeing the developments of TheoretiCS. Even though predicting the future is difficult, I have no doubt that the journal will become a coveted outlet, with the help of the community it aims to serve. Welcome to TheoretiCS and good luck!

=== Additional information about the journal ===

---  Guiding principles and objectives  ---

- We believe that our field (and science in general) needs more 'virtuous' open-access journals, a whole eco-system of them, with various levels of specialization and of selectivity. We also believe that, along with the structuring role played by conferences in theoretical computer science, we collectively need to re-develop the practice of journal publications.

- The scope of TheoretiCS is the whole of Theoretical Computer Science, understood in an inclusive meaning (concretely: including, but not restricted to, the Theory of Computing and the Theory of Programming; or equivalently, the so-called TCS-A and TCS-B, reminiscent of Jan van Leeuwen's Handbook of Theoretical Computer Science).

- Our aim is to rapidly become a reference journal and to contribute to the unity of the Theoretical Computer Science global community. In particular, we will seek to publish only papers that make a very significant contribution to their respective fields, that strive to be accessible to a wider audience within theoretical computer science, and that are, generally, of a quality on par with the very best journals in the field.

- TheoretiCS adheres to the principles of 'virtuous' open-access: there is no charge to read the journal, nor to publish in it. The copyright of the papers remains with the authors, under a Creative Commons license.

---  Editorial Board  ---

The inaugural Editors-in-Chief are Javier Esparza (TU München) and Uri Zwick (Tel Aviv U.). The entire Editorial Board can be seen at (see below as well).

---  Organization and a bit of history  ---

The project built on groundwork laid in the Council of the EATCS, and started in 2019 and underwent a long gestation. From the start, we wanted to have a thorough discussion with a wide representation of the community, on how to best implement the guiding principles sketched above. It was deemed essential to make sure that all fields of theoretical computer science would feel at home in this journal, and that it would be recognized as a valid venue for publication all over the world.

This resulted in the creation of an Advisory Board, composed of representatives of most of the main conferences in the field (currently APPROX, CCC, COLT, CONCUR, CSL, FOCS, FoSSaCS, FSCD, FSTTCS, ICALP, ICDT, ITCS, LICS, MFCS, PODC, SoCG, SODA, STACS, STOC, TCC) and of so-called members-at-large. The composition of this Advisory Board, which may still evolve, can be consulted at

---  Logistics and answers to some natural questions  ---

- The journal is published by the TheoretiCS Foundation, a non-profit foundation established under German law.

- TheoretiCS is based on the platform, in the spirit of a so-called overlay journal.

- The Advisory Board, together with the Editors-in-Chief and the Managing Editors, devolved much of their efforts to designing and implementing an efficient 2-phase review system: efficient in terms of the added-value it brings to the published papers and their authors, and of the time it takes. Yet, as this review system relies in an essential fashion on the work and expertise of colleagues (like in all classical reputable journals), we cannot guarantee a fixed duration for the evaluation of the papers submitted to TheoretiCS.

- Being charge-free for authors and readers does not mean that there is no cost to publishing a journal. These costs are supported for the foreseeable future by academic institutions (at the moment, CNRS and Inria, in France; others may join).

- The journal will have an ISSN, and each paper will have a DOI. There will be no print edition.

---  Editorial Board  ---


    Javier Esparza (Technische Universität München, Munich)
    Uri Zwick (Tel Aviv University, Tel Aviv)

Managing  Editors

    Antoine Amarilli (Institut polytechnique de Paris, Télécom Paris)
    Nathanaël Fijalkow (CNRS, Bordeaux, and The Alan Turing Institute of Data Science, London)


    Martin Abadi, Google, USA
    Andris Ambainis, U. of Latvia
    Albert Atserias, UPC, Barcelona
    Haris Aziz, UNSW, Sydney
    David Basin, ETH Zürich
    Patricia Bouyer, CNRS, Paris-Saclay
    Nicolò Cesa-Bianchi, Università di Milano
    Anuj Dawar, Cambridge University
    Luc Devroye,  McGill University, Montreal
    Jacob Fox, Stanford University
    Mohsen Ghaffari, ETH Zürich
    Georg Gottlob, Oxford University
    Anupam Gupta, Carnegie-Mellon University
    Venkatesan Guruswami, Carnegie-Mellon University
    Johan Håstad, KTH, Stockholm
    Ravi Kannan, Microsoft Research India, Bengaluru
    Anna Karlin, University of Washington, Seattle
    Ken-ichi Kawarabayashi, National Institute of Informatics, Tokyo
    Valerie King, University of Victoria
    Robert Kleinberg, Cornell University
    Naoki Kobayashi, University of Tokyo
    Elias Koutsoupias, Oxford University
    Xavier Leroy, Collège de France, Paris
    Katrina Ligett, Hebrew University, Jerusalem
    Rupak Majumdar, MPI-SWS, Kaiserslautern
    Joseph Mitchell, State University of New York at Stony Brook
    Mehryar Mohri, Google and New York University
    David Mount, University of Maryland
    Anca Muscholl, Université de Bordeaux
    Danupon Nanongkai, University of Copenhagen
    Moni Naor, Weizmann Institute, Rehovot
    Catuscia Palamidessi, Inria, Palaiseau
    Michał Pilipczuk, University of Warsaw
    Jean-Francois Raskin, Université Libre de Bruxelles
    Peter Sanders, KIT, Karlsruhe
    Davide Sangiorgi, Università di Bologna
    Nitin Saxena, IIT Kanpur
    Alistair Sinclair, UC Berkeley
    Ola Svensson, EPF Lausanne
    Gregory Valiant, Stanford University
    Stephanie Weirich, University of Pennsylvania
    Virginia V. Williams, Massachusetts Institute of Technology
    James Worrell, Oxford University
    Mihalis Yannakakis, Columbia University, New York

Wednesday, November 24, 2021

Inria Innovation Prize 2021 to Mateescu, Garavel, Lang and Serwe

I just learnt that Radu Mateescu, Hubert Garavel, Frédéric Lang and Wendelin Serwe from the Construction of Verified Concurrent Systems (Convecs) project team at INRIA Grenoble – Rhône-Alpes Centre have been recently awarded the Inria Innovation Prize – Académie des sciences – Dassault Systèmes. Their work contributes to the development of the CADP toolbox for modelling and verifying parallel and distributed systems. The aim of that project is to automatically detect design flaws in highly complex systems. 

Readers of this blog will be as delighted as I am by this news. CADP is one of the tools from the concurrency community that has the longest history, dating back to its early releases in 1989. It has been used to good effect in a variety of applications, is still under continuous development and makes excellent use in practice of classic tools from concurrency theory. By way of example, let me mention the recent successes by the Convecs team in dealing with difficult challenges posed by Bernhard Steffen and his team on the evaluation of CTL and LTL formulae on large products of automata. (See, for instance, the news items here and here.) Traditional model checkers fail on those challenges because the state space of the product automata is too large for them. However, a wise use of bisimulations and congruence results allows CADP to solve many of those challenges. Interested readers might also wish to peruse the slides at 

Congratulations to the whole CADP team and to the concurrency community for this award!

Thursday, September 16, 2021

PhD scholarship in Data Science for sustainability at Reykjavik University

Department of Computer Science, Reykjavik University 

PhD scholarship in Data Science for sustainability by predicting food consumption to reduce food waste 

The Department of Computer Science at Reykjavík University is looking for a PhD student to build, apply and evaluate a global model that predicts future food consumption by geographic area. The goal of the project is twofold: Reduce food waste in restaurants and grocery stores by using global machine learning algorithms. Understand food consumption trends in restaurants and grocery stores by analyzing the global model’s input data and their results. The ideal candidate should possess data science expertise, be passionate about sustainability and enthusiastic about research. The project is a collaboration with GreenBytes and will be carried out in Reykjavik, Iceland.

See for full details and for information on how to apply.

Saturday, August 28, 2021

Interview with CONCUR 2021 ToT Award Recipients: David Janin and Igor Walukiewicz

This is the fourth and last instalment of the series of interviews with the 2021 CONCUR Test-of-Time Award recipients, which I have conducted with Nathalie Bertrand and Nobuko Yoshida's great help. (See here, here and there for the previous ones.) In it, I interviewed David Janin and Igor Walukiewicz

I thank David and Igor for their very stimulating answers to my questions and for painting such a rich picture of the context for their award-winning work and of the subsequent developments related to it. Enjoy!

Note: The interview has been slightly edited for clarity and to correct some small typos. Thanks to Ilaria Castellani for pointing out several typos that had escaped my attention.

Luca: You receive the CONCUR ToT Award 2021 for your paper On the Expressive Completeness of the Propositional mu-Calculus with respect to Monadic Second Order Logic, which appeared at CONCUR 1996. In that article, you showed what I consider to be a fundamental result, namely that the mu-calculus and the bisimulation-invariant fragment of  monadic second-order logic (MSOL) have the same expressiveness over transition systems. Could you tell us how you came to study that question and why do you think that such a natural problem hadn't been answered before your paper?

David and Igor: At that time we were interested in automata characterizations of the expressive power of MSOL and the mu-calculus. In 1988 Damian Niwinski has shown that over binary trees the mu-calculus and MSOL are expressively equivalent. When it appeared, the result was quite surprising, even unexpected. The two logics are not equivalent on unranked trees where the number of children of a node is not fixed. In consequence, the logics are not equivalent over the class of all transition systems. 

In 1983 van Benthem showed that modal logic is equivalent to the bisimulation-invariant fragment of first-order logic. When we have learned about this result we
have realized that our automata models can be used to prove a similar statement
for the mu-calculus.

The method of van Benthem could not be applied to MSOL, the automata based
method looks like the only way to prove the result.

Luca: I am interested in how research collaborations start, as I like to tell "research-life stories" to PhD students and young researchers. Could you tell us how you started your collaboration?

David: I came to meet Igor when he was visiting Bordeaux in fall 93, presenting his first completeness result on a proof system for the mu-calculus (LICS 93). I was myself starting a PhD considering modal logic for specifying (various forms of) nondeterminism in connection with (power)domain theory (FST&TCS 93).

We eventually met again in Auvergnes (center of France) for the Logic Colloquium in summer 94. There, spending time in the park nearby the conference venue or walking around the volcanoes, we elaborated a notion of nondeterministic automata for the modal mu-calculus. This result can be seen as extending the notion of "disjunctive" normal form from propositional logic to the modal mu-calculus. I remember that Igor later used this result for his second completeness result for Kozen’s proposed proof system for the mu-calculus (LICS 95). Thanks to Igor, this was for me the occasion to learn in depth the link between mu-calculus and tree automata.

Incidentally, Johan van Benthem was also attending this Logic Colloquium and we both attend his lecture about the bisimulation-invariant fragment of FO. Although we did not yet realize we could generalize his result to MSO, this surely increased our own understanding of logic.

Our first result (Automata for the mu-calculus) was presented at MFCS in 95 in Prague, where Igor and I met again. It could have been there, or a little later, that we eventually postulated our bisimulation-invariance result. However, proof arguments were only found later while exchanging emails. It was a bit amazing for me that we could discuss that way across Europe: email started to be heavily used only in the late 80's. In my head, Poland was far, far away from France.

Yet our collaboration was eventually in the line of an  ongoing collaboration
between Warsaw and Bordeaux, involving researcher like Arnold (my supervisor)
and Niwinski (Igor's mentor), both major specialists in the area of automata and
logics. Somehow, as a followup, together with Aachen (Grädel and Thomas) and
many other sites, the GAMES European network was later created, and, almost at
the same time, Igor came to Bordeaux as a CNRS researcher.

Luca: As you mentioned earlier, van Bentham has shown that modal logic has the same expressive power as the bisimulation-invariant fragment of first-order logic. In some sense, one may consider your main result as the extension of van Bentham's theorem to a setting with fixed-points. Could you briefly describe at a high level the challenges that fixed-points created in your work? To your mind, what was the main technical achievement or technique in your paper?

David and Igor: Sure our result is similar to van Benthem's, and, as mentioned
above, his own presentation in 93 was very inspiring. However, his proof relies
on compactness of first-order logic and cannot be adapted to monadic
second-order logic. In our proof, we have used automata-theoretic techniques.

In our previous works we had developed automata models for MSOL and the
mu-calculus on unranked trees. Every transition system is bisimulation invariant
to a tree obtained by the unfolding of the transition system. Crucially for our
result, it is also equivalent to a tree where every subtree is duplicated
infinitely many times. A short pumping argument shows that on such trees the two automata models are equivalent.

Luca: Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? Is there any result obtained by other researchers that builds on your work and that you like in particular?

David and Igor: Around that time Marco Hollenberg and Giovana D'Agostino used our automata-theoretic methods to show the uniform interpolation property for the mu-calculus.

In collaboration with Giacomo Lenzi (postdoc in Bordeaux from Pisa), David
considered the bisimulation-invariant fragment of various levels of the monadic
quantifier alternation hierarchy. It turns out that monadic Sigma_1 corresponds to reachability properties and monadic Sigma_2 corresponds to Büchi properties, respectively the first and second levels of the mu-calculus hierarchy.

It could be the case that all mu-calculus can be translated into monadic
Sigma_3 formulas -- this is true when restricting to deterministic transition
systems. However, with nondeterminism, such a result seems difficult to achieve.

Incidentally, Giacomo and David also proved that adding limited counting capacity
to modalities yields a fixed-point calculus equivalent to the unraveling invariant
fragment of MSO (LICS 2001). 

In 1999, in collaboration with Erich Grädel, Igor has used similar techniques to define and study guarded fixed-point logic. Subsequently, several other fixed-point logics of this kind were proposed with the most expressive one probably being guarded negation logic with fixed points of Bárány, ten Cate, and Segoufin from 2015.  These works all use automata-theoretic methods to some extent.

Luca: Your paper was written while Igor was at BRICS at the University of Aarhus. Igor, what was it like to be at BRICS@Aarhus at that time? What role do
you think centres like BRICS played and can play in the development of theoretical computer science? Do you think that your stay at BRICS had a
positive impact on your future career?

Igor: My stay at BRICS had definitively a beneficial impact on me. At that time BRICS was one of the most active centers world wide in theoretical computer science. Being able to see and talk to so many different people, being exposed
to so many different ideas, was very enriching. BRICS was a meeting place
allowing scientists to have a better and larger vision of our field. BRICS contributed to the development of many people involved, as well as to the excellence of Aarhus, and even Denmark as a whole, in our field.

Luca: I have been brought up in the concurrency-theory tradition and I feel that bisimulation-invariant properties are the interesting ones over transition systems. Do you think that we actually "need" logics that allow one to specify properties of transition systems that are not bisimulation invariant?

David: That was the idea indeed and the mu-calculus is the good logic for that. From a mathematical perspective, bisimulation is a fairly natural definition. In some sense, bisimulation equivalence is a greatest co-congruence.

However, I always suspected that bisimulation is too fine grained as an equivalence for concurrency. When modeling realistic systems, nondeterminism arises either as controllable (angelic) or uncontrollable (demonic) choice. In this case, the right equivalence to be considered is simulation equivalence.

The funny thing is that David Park, who "invented" bisimulation, was actually studying equivalence of J.R. Büchi's deterministic string automata where, because of determinism, bisimulation turns out to be equivalent to simulation equivalence. It is only after Matthew Hennessy and Robin Milner's work in concurrency that bisimulation was applied to nondeterministic behaviors.

Igor: In the context of XML and semistructured data, bisimulation is not relevant. One of the prominent queries in XPATH is whether a value appears twice -- that is clearly not a bisimulation-invariant property. So while XPATH looks very close to PDL or the mu-calculus, many techniques and questions are very different. The other context that comes to mind is controller synthesis, where we ask for a
transition system of a specific shape, for example, with self-loops on certain actions. Such self loops represent invisibility of the action to the controller.

Luca: 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?

David: In Logic for Computer Science, there have always been two kinds of approaches: model theory that eventually led to model checking and proof theory that eventually led to typed programming languages.

Twenty years later, aiming at designing and implementing real concurrent systems, especially for interactive arts, I realized that the latter approach was
(at least for me) a lot more effective. Building concurrent systems by synchronizing arbitrary sub-systems sounded for me like unstructured programming; it was essentially unmaintainable. Monads and linear types, among
many other approaches in typed functional programming, surely offered interesting
alternatives to process calculi approaches.

Igor: In the context of the paper we discuss here, I am surprised by developments around the model-checking problem for the mu-calculus. After some years of relative calm, Calude, Jain, Khoussainov, Li and Stephan have made an important breakthrough in 2017. Yet, despite big activity after this result, the research on the problem seems to have hit one more barrier. Another old prominent problem is decidability of the alternation hierarchy for the mu-calculus. The problem is: given a formula and a number of alternations between the least and the greatest fixed-points, decide if there is an  equivalent formula with this number of alternations. Even when the number of alternations is fixed we do not know the answer. Among others, Thomas Colcombet and Christof Loeding have done very interesting work on this subject.

Luca: What advice would you give to a young researcher who is keen to start working on topics related to automata theory and logic in computer science?

David: From the distance, our result sounds to me as a combination of both technique and imagination. Technique for mastering known results and imagination for finding original open problems, especially between research fields that are not (yet) known to be deeply related. As a matter of fact, I felt lucky finding such a fresh open problem that was (probably) a lot easier to solve than many other well-known hard problems.

Technique comes from hard work. It is obviously essential but somehow easy to teach and evaluate in academia. Imagination comes from curiosity. It is still essential but a lot more difficult to teach. So young researchers must develop by themselves their own imagination and curiosity.

In the automata-theory branch of logic in computer science, the remaining open
problems seem fairly hard, so I believe that it is the imagination of young researchers that will make the difference for setting up new interesting directions of research, especially those who are ready to look aside, towards other areas of
logic in computer science and, because it can be a considerable source of
motivation, funny applications.

Igor: Naturally, the field is much broader these days than it was 25 years ago. It is
crucial to master some techniques. For this, working on variations of already solved problems is a good method. Yet, I think it is important to escape
the cycle of constant modifications of existing problems and their solutions.
I would suggest that, at some moment, one should find an important open
problem that one is passionate about and should spend a considerable effort on
it. I admit that this is a matter of a taste, personality, and having a sufficiently
comfortable situation to afford such a risk. Another good option is to look at frontiers with other areas: distributed computing, semantics, control theory, security.

Monday, August 23, 2021

Interview with CONCUR 2021 ToT Award Recipients: Ahmed Bouajjani and Javier Esparza

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.