The detectEr runtime-verification tool for Erlang programs

Thanks to the huge amount of excellent work done by Duncan Paul Attard and Adrian Francalanza, we now have a tutorial on detectEr that some of you might want to check out. See this web page for all the material, tool download and links to the videos of the tutorial Duncan delivered at the DisCoTec 2021 Tutorial Day. 

detectEr is a runtime verification tool for asynchronous component systems that run on the Erlang Virtual Machine. It also supports monitoring systems that can execute outside of the EVM, so long as these can produce traces that are formatted in a way that is parsable by detectEr. The tool itself is developed in Erlang, and is the product of five years of theoretical and practical development. (Erlang is a programming language used to build massively scalable soft real-time systems with requirements on high availability.)  

Enjoy!

Interview with CONCUR 2021 ToT Award recipients, Part 1: Rajeev Alur, Thomas Henzinger, Orna Kupferman and Moshe Vardi

Last year, the CONCUR conference series inaugurated its Test-of-Time Award, whose purpose is to recognise important achievements in Concurrency Theory that were published at the CONCUR conference and have stood the test of time. This year, the following four papers were chosen to receive the CONCUR Test-of-Time Awards for the periods 1994–1997 and 1996–1999 by a jury consisting of Rob van Glabbeek (chair), Luca de Alfaro, Nathalie Bertrand, Catuscia Palamidessi, and Nobuko Yoshida: 

• David Janin and Igor Walukiewicz. On the Expressive Completeness of the Propositional mu-Calculus with respect to Monadic Second Order Logic. 
• Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings.
• Ahmed Bouajjani, Javier Esparza, and the late Oded Maler. Reachability Analysis of Pushdown Automata: Application to Model-checking.
• Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating Refinement Relations.
  

Last year, I interviewed the CONCUR 2020 Test-of-Time Award recipients and was asked by Javier Esparza (chair of the CONCUR SC) and Ilaria Castellani (outgoing chair of the IFIP WG 1.8 on Concurrency Theory) to do the same with the current batch of awardees. (In passing, let me thank Nathalie Bertrand and Nobuko Yoshida for their kind help with the interviews!)

This post is devoted to the interview I conducted via email with Rajeev Alur, Thomas A. Henzinger, Orna Kupferman and Moshe Y. Vardi. Reading the answers I received from that dream team of colleagues was like a masterclass for me and I trust that their thoughts on their award-winning paper will be of interest to many of the readers of this blog. Enjoy!

Luca: You receive the CONCUR ToT Award 2021 for your paper Alternating Refinement Relations, which appeared at CONCUR 1998. In that article, you gave what I consider to be a fundamental contribution, namely the introduction of refinement relations for alternating transition systems. Could you briefly explain to our readers what alternating transition systems are? Could you also tell us how you came to study the question addressed in your award-winning article and why you focused on simulation- and trace-based refinement relations? Which of the results in your paper did you find most surprising or challenging? 

Answer: When we model a system by a graph, our model abstracts away some details of the system. In particular, even when systems are deterministic, states in the model may have several successors. The nondeterminism introduced in the model often corresponds to different actions taken by the system when it responds to different inputs from its environment. Indeed, a transition in a graph that models a composite system corresponds to a step of the system that may involve some components. Alternating transition systems (ATSs) enable us to model composite systems in more detail. In an ATS, each transition corresponds to a possible move in a game between the components, which are called agents. In each move of the game, all agents choose actions, and the successor state is deterministically determined by all actions. Consequently, ATSs can distinguish between collaborative and adversarial relationships among components in a composite system. For example, the environment is typically viewed adversarially, meaning that a component may be required to meet its specification no matter how the environment behaves.

In an earlier paper, some of us introduced ATSs and Alternating Temporal Logics, which can specify properties of agents in a composite system. The CONCUR 1998 paper provided refinement relations between ATSs which correspond to alternating temporal logics. Refinement is a central issue in a formal approach to the design and analysis of reactive systems. The relation “I refines S '' intuitively means that system S has more behaviors than system I. It is useful to think about S being a specification and I an implementation. Now, if we consider a composite implementation I||E and specification S||E and we want to check that the component I refines the component S, then the traditional refinement preorders are inappropriate, as they allow I to achieve refinement of I||E with respect to S||E by constraining its environment E. Alternating refinement relations are defined with respect to ATSs that model the interaction among the underlying components, and they enable us to check, for example, that component I has fewer behaviors than component S no matter how component E behaves. They are called “alternating” because refinement may restrict implementation actions but must not restrict environment actions. In other words, refinement may admit fewer system actions but, at the same time, more environment actions. 

It was nice to see how theoretical properties of preorders in the traditional setting are carried over to the game setting, and so are the results known then about the computational price of moving to a game setting. First, the efficiency of the local preorder of simulation with respect to the global preorder of trace containment is maintained. As in the traditional setting, alternating simulation can be checked in polynomial time, whereas alternating trace-containment is much more complex. Second, the branching vs. linear characterizations of the two preorders is preserved: alternating simulation implies alternating trace containment, and the logical characterization of simulation and trace-containment by CTL and LTL, respectively, is carried over to their alternating temporal logics counterparts. The doubly-exponential complexity of alternating trace containment, as opposed to the PSPACE complexity of trace containment, is nicely related to the doubly-exponential complexity of LTL synthesis, as opposed to its PSPACE model-checking complexity,

Luca: In your paper, you give logical characterisations of your alternating refinement relations in terms of fragments of alternating temporal logic. Logical characterisations of refinement relations are classic results in our field and I find them very satisfying. Since I teach a number of those results in my courses, I'd be interested in hearing how you would motivate their interest and usefulness to a student or a colleague. What would your "sales pitch" be? 

Answer: There is extensive research on the expressive power of different formalisms. Logical characterization of refinement relations tells us something about the distinguishing power of formalisms. For example, while the temporal logic CTL* is more expressive than the temporal logic CTL, the two logics have the same distinguishing power: if you have two systems and can distinguish between them with a CTL* formula (that is, your formula is satisfied only in one of the systems), then you should be able to distinguish between the two systems also with a CTL formula. Moreover, while CTL is not more expressive than LTL, we know that CTL is “more distinguishing” than LTL. These results have to do with the logical characterizations of trace containment and simulation. The distinguishing power of a specification formalism is useful when we compare systems, in particular an implementation and its abstraction: if we know that the properties we care about are specified in some formalism L, and our system refines the abstraction according to a refinement relation in which the satisfaction of specifications in L is preserved, then we can perform verification on the abstraction.

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

Answer: Subsets of us were already collaborating on other topics related to reactive models and model checking, and all of us shared a common belief that the field was in need to move from the limited setting of closed systems to a more general setting of open systems, that is, systems that interact with an environment. Open systems occur not only when the environment is fully or partly unknown, but also when a closed system is decomposed into multiple components, each of them representing an open system. To build “openness” into models and specifications as first-class citizens quickly leads to the game-theoretic (or “alternating”) setting. It was this realization and the joint wish to provide a principled and systematic foundation for the modeling and verification of open systems which naturally led to this collaboration.

Luca: Did any of your subsequent research build explicitly on the results and the techniques you developed in your award-winning paper? Which of your subsequent results on alternating transition systems and their refinement relations 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? 

Answer: Various subsets of us pursued multiple research directions that developed the game-theoretic setting for modeling and verification further, and much remains to be done. Here are two examples. First, the game-theoretic setting and the alternating nature of inputs and outputs are now generally accepted as providing the proper semantic foundation for interface and contract formalisms for component-based design. Second, studying strategic behavior in multi-player games quickly leads to the importance of probabilistic behavior, say in the form of randomized decisions and strategies, of equilibria, when players have non-complementary objectives, and of auctions, when players need to spend resources for decisions. All of these are still very active topics of research in computer-aided verification, and they also form a bridge to the algorithmic game theory community.

Luca: One can view your work as a bridge between concurrency theory and multi-agent systems. What impact do you think that your work has had on the multi-agent-system community? And what has our community learnt from the work done in the field of multi-agent systems? To your mind, what are the main differences and points of contact in the work done within those communities? 

Answer: Modeling interaction in multi-agent systems is of natural interest to planning problems studied in the AI community. In 2002, the International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS) was formed and the annual International Conference on Autonomous Agents and Multiagent Systems (AAMAS) was launched. The models, logics, and algorithms developed in the concurrency and formal methods communities have had a strong influence on research presented at AAMAS conferences over the past twenty years. Coincidentally, this year our paper on Alternating-Time Temporal Logic was chosen for the IFAAMAS Influential Paper Award.

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?

Answer: Research on formal verification and synthesis, including our paper, assumes that the model of the system is known. Reinforcement learning has emerged as a promising approach to the design of policies in scenarios where the model is not known and has to be learned by agents by exploration. This leads to an opportunity for research at the intersection of reactive synthesis and reinforcement learning. A potentially promising direction is to consider reinforcement learning for systems with multiple agents with both cooperative and adversarial interactions.

The realization that reactive systems have to satisfy their specifications in all environments has led to extensive research relating formal methods with game theory. Our paper added alternation to refinement relations. The transition from one to multiple players has been studied in computer science in several other contexts. For the basic problem of reachability in graphs, it amounts to moving from reachability to alternating reachability. We recently studied this shift in other fundamental graph problems, like the generation of weighted spanning trees, flows in networks, vertex covers, and more. In all these extensions, we consider a game between two players that take turns in jointly generating the outcome. One player aims at maximizing the value of the outcome (e.g., maximize the weight of the spanning tree, the amount of flow that travels in the network, or the size of the vertex cover), whereas the second aims at minimizing the value. It is interesting to see how some fundamental properties of graph algorithms are lost in the alternating setting. For example, following a greedy strategy is not beneficial in alternating spanning trees, optimal strategies in alternating flow networks may use fractional flows, and while the vertex-cover problem is NP-complete, an optimal strategy for the maximizer player can be found in polynomial time. Many more questions in this setting are still open. 

Luca: What advice would you give to a young researcher who is keen to start working on topics related to alternating transition systems and logics?

Answer: One important piece of advice to young researchers is to question the orthodoxy. Sometimes it is necessary to learn everything that is known about a topic but then take a step back, look at the bigger picture, reexamine some of the fundamental assumptions behind the established ways of thinking, change the models that everyone has been using, and go beyond the incremental improvement of previous results. This is particularly true in formal methods, where no single model or approach fits everything. And young researchers stand a much better chance of having a really fresh new thought than those who have been at it for many years.

Frank P. Ramsey on research and publication rates

Spurred by the excellent 1978 radio programme 'Better than the Stars' by D. H. Mellor about Frank Ramsey and by the Philosophy Bites interview with Cheryl Misak on Frank Ramsey and Ludwig Wittgenstein, I started reading Cheryl Misak's biography of Frank Ramsey. (FWIW, I strongly recommend the radio programme, the podcast and the book.)

The following quote from pages 169-170 of Cheryl Misak's book describes Ramsey's views on publications and research, as stated in a letter to his father Arthur:

Arthur tried a different tack, suggesting that Frank was going to be in trouble for wasting all this time on analysis, rather than on his career. On 24 September, in what seems to be his last letter home before he left Vienna, Frank wrote:

I don’t see how there can be any such inquisition into my conduct in Vienna as you suppose seem to want to guard against.... No one can suppose that you can’t research for six months without having a paper ready by the end. If everyone wrote a paper every six months the amount of trivial literature would swell beyond all bounds. Given time I shall produce a good paper. But if I hurry it will be ill written and unintelligible and unconvincing.

It seems to me perfectly proper to spend a scholarship being analysed, as it is likely to make me cleverer in the future, and discoveries of importance are made by remarkable people not by remarkable diligence.

While it may not be persuasive that psychoanalysis makes one cleverer, Frank was prescient that the numbers of journal articles would eventually swell and he was right that diligence isn't enough to produce discoveries of importance.

 

Of course, academia has changed since those times and I do value "remarkable diligence". However, I will try to remember Ramsey's words next time someone proposes to make academic hirings and promotions conditional to having a certain number of papers or citations or whatever per year on average.

Course on Ethics and Accountability in Computer Science

About one year ago, I became aware of the course "Ethics and Accountability in Computer Science" designed and taught by Rodrigo Ferreira and Moshe Y. Vardi at Rice University. The goals and high-level structure of the course, as well as its context, are described in an informative and thoughtful paper by Moshe and Rodrigo that appears in the Proceedings of the 52nd ACM Technical Symposium on Computer Science Education (SIGCSE ’21), which I strongly recommend. You can also read a journal paper reporting on one of their course assignments, which was designed to make students focus on practising "deep attention" in the sense of artist and academic Jenny Odell.

I was smitten by the underlying tenet for their course, namely that "social justice is the single most important issue confronting computer science students today." That tenet is also very much in line with a reflection on the impact that digital technology has on social justice that the Scientific Advisory Board of the Gran Sasso Science Institute asked the Computer Science group at that institute to undertake. Therefore, after having invited Rodrigo to deliver a webinar on the course at the ICE-TCS+GSSI webinar series, I decided that, as an experiment, I would offer a version of the Rice University course to master students in computer science, language technology and software engineering at Reykjavik University during our spring semester 2021. 

Mine was a foolhardy decision for a variety of reasons. However, I have always believed that computer scientists should strive to be the 21st century Renaissance men and women, and bridge the gap between C. P. Snow's "two cultures". Indeed, to quote Edward A. Lee freely, to my mind technologists ought to be amongst the greatest humanists of our age. Despite my other commitments, offering a version of the Ferreira-Vardi course at Reykjavik University felt like the right thing to do at this time. 

I taught the course over twelve weeks to a varied group of eight students, in cooperation with Claudio Pedica. Thanks to the constant support I received from Rodrigo Ferreira, I lived to tell the tale and I hope that I managed to do some justice to the truly excellent course that Moshe and Rodrigo put together. Having a dream team of students with a variety of cultural backgrounds made the course extremely interesting and a learning experience for me. I had to refresh my memory of the philosophy I studied at high school in Italy in a previous life, learn some modern moral philosophy I had not met at school (such as the work by Elisabeth Anscombe and Philippa Foot, amongst others), read a substantial amount of new material (some of it fresh off the press as the course was unfolding) and broaden my horizons. I could not have asked for a better intellectual experience and the students in the course, from Denmark, France, Germany, Iceland and the Netherlands taught me well, kept me on my toes and stimulated me to keep reading material related to ethics even now that the course is over.

Teaching the course reinforced my belief that a course on ethics and on the impact that our field has on social justice should be required for all students in computer science. If you plan to run such a course, I strongly recommend that you consider the Ferreira-Vardi course as a blueprint.

PolyConc: Online collaboration to improve on a result on the equational theory of CCS modulo bisimilarity

The aim of this post is to try and start an online collaboration to improve the solution to a problem in the equational logic of processes that I posed in a survey paper in 2003, namely

Can one obtain a finite axiomatisation of the parallel composition operator in bisimulation semantics by adding only one binary operator to the signature of (recursion, restriction, and relabelling free) CCS?

Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, Bas Luttik and I published a partial, negative answer to the above question in a paper at CSL 2021. (See the arXiv version for details and for the historical context for the above question.) Our solution is based on three simplifying assumptions that are described in detail in Section 3 of the above-mentioned paper. We'd be very interested in hearing whether any member of the research community in process algebra, universal algebra and equational logic can relax or remove any of our simplifying assumptions. In particular, one can start with assumptions 3 and 2. 

We would also welcome any comments and suggestions on whether some version of that problem can be solved using existing results from equational logic and universal algebra. In particular, are there any general results guaranteeing that, under certain conditions, the reduct of a finitely based algebra is also finitely based? Or, conversely, that if some algebra is not finitely based, then so its expansion with a new operator?

To start with, add any contributions you might have as comments to this post. If ever we make substantial enough progress on the above question, anyone who has played a positive role in extending our results will be a co-author of the resulting paper. 

Let PolyConc begin!

Article by Sergey Kitaev and Anthony Mendes in Jeff Remmel's memory

Sergey Kitaev just shared with me an article he wrote with Anthony Mendes in Jeff Remmel's memory. Jeff Remmel was a distinguished mathematician with a very successful career in both logic and combinatorics. 

The short biography at the start of the article paints a vivid picture of Jeff Remmel's  personality, and will be of interest and inspiration to many readers. His hiring as "an Assistant Professor in the Department of Mathematics at UC San Diego at age 25, without officially finishing his Ph.D. and without having published a single paper" was, in Jeff Remmel's own words, a "fluke that will never happen again."

I had the pleasure of making Jeff Remmel's acquaintance when he visited Sergey in Reykjavik and thoroughly enjoyed talking to him about a variety of subjects. He was truly a larger-than-life academic.

Whence do research collaborations (in TCS) arise?

About ten days ago, I gave a talk to my colleagues at the Department of Computer Science at Reykjavik University, introducing my personal (and admittedly very biased) view of the past, present and future of ICE-TCS. 

After my presenta­tion, a colleague asked me how she could engage mathematicians and theoretical computer scientists in joint research. I gave her an answer off the top of my head, but it was clear that she was unconvinc­ed and felt that I was avoid­ing answering her question. (For the record, I basically told her that she should knock on our door, discuss with us the problems she was interested in solving and hope that they are of interest to us. I feel that many research collaborations arise from serendipity and that there is no recipe that is guaranteed to work.) 

The thought that she felt that I might have dodged her question prompted me to look back at my own research collabo­rations and how they came about. The rest of this post is the result of that quick-and-dirty reflection. Let me state right away that my list isn't meant to be exhausti­ve and that I won't mention many of the collaborations in which I have been lucky to be involved and that I have played a crucial role in shaping my academic development. 

Reading papers. One of my long-term research collaborations arose from reading a paper written by a colleague. His paper prompted my companion and me to ask ourselves whether we could prove a similar result to the one our colleague had shown in a different setting. We succeeded and sent him our paper. Subsequently, we invited him to visit us in Aalborg. That visit marked the start of a collaboration and friendship that has lasted for over 20 years.

Approaching a colleague via email for help in solving a problem. At some point, my companion and I were thinking about a research problem that had frustrated us for a while. I remembered reading a number of papers by a colleague on related topics, so I wrote to him, describing the problem, our attempts at solving it and where we had hit a brick wall. I asked him whether he would be interested in working with us on solving it. He did and that was one of the lucky breaks I have had in my research career. Once more, that collaboration offer via email led to mutual visits, other joint papers and, IMHO even more importantly, a long-term friendship that extended beyond work.
 

Available funding and building on one's mistakes. One day in 2009, an email in my mailbox alerted me to the availability of substantial funding for research collabo­ration between universities in country X and those locat­ed in Norway, Iceland and Lichtenstein. This opportunity was enticing, as I had never visited country X, so I asked myself: "Is there anyone there we might conceivably work with?'' Mulling over that question, I recalled that a colleague from country X had spotted an imprecision in a paper I had coauthored. 

I wrote to him, we applied for that funding jointly and got it. That successful grant application provided the funds for many research visits involving several people in our research groups. Those visits resulted in joint papers, another successful grant application and a number of friendships.

Coffee breaks at conferences. I have at least two exhibits under this heading. The first belongs to a previous geologic­al era (1991). I was attend­ing a conference at CMU and asked a colleague what he was working on. He told me
about a problem he was tackling, which I knew was also on the radar of a fellow researcher and on which I had started working independently. Eventually, after some email exchanges, that chat over coffee turned into a three-way collaboration that, thanks to my coauthors, produced one of my best papers.

Fast forward to 2017 and I'm in Rome to deliver an invited talk at a small conference. During the coffee break follow­ing my presentation, I was approached by a young research­er, with whom I had a number of pleasant conversations during the conference. Some time later, she sent me a draft paper dealing with a topic related to the content of my invited talk. I invited her to visit our research group in Reykjavik and to join the team working on a research project for which we had funding at the time. Those coffee-break conversations led to a collaboration and friendship that I hope will last for a long time. Meeting that colleague has been another of my lucky breaks.
 

Reading groups. Last, but by no means least, let me mention that my first research collaboration that did not involve my thesis supervisors arose when I read Gordon Plotkin's famous "Pisa Notes (On Domain Theory)" with a fellow PhD student. Reading that work led to our first joint paper in 1991 and a companionship that has lasted to this day. I heard Orna Kupferman give the following, tongue-in-cheek advice to young researchers: "Write papers with your twin-sister!" Mine might be: "Write papers with your companion in life!" 

Let me conclude by saying that serendipity and an actual friendship that extends beyond the confines of scientific work were the key aspects in my most pleasant and enduring collaborations. I apologise to the colleagues from whom I have learnt much over the years (former students and postdocs, as well as others) who were the prime movers in research collaborations I did not mention in this post. 

 I guess that this note provides much more information than my colleague was intending to receive, but I thought I should put it out for the benefit of the young researchers at Reykjavik University and at the Gran Sasso Science Institute, and of any reader I might have. 

How did your research collaborations arise? If you have anything to add to what I wrote above, and I am sure you do, add your contributions as comments to this post.

Support research in the Foundations of Computing at the University of Leicester!

In an ideal world, university administrators would support the work of the top-class academics employed by their institution, especially if they attract students, have a high research standing within their communities and bring in substantial funding from competitive research funds. After all, to quote Isidor Isaac Rabi, "the faculty are the university" and the most valuable currency for an academic institution is reputation. 

Unfortunately, university administrations the world over repeatedly surprise me by making structural changes that affect some of their very best academics and actually reduce the reputation of their institutions in the eyes of the community at large.

The latest example comes from the University of Leicester, where, as stated here,

[the] University VC proposes to merge Informatics and Mathematics into a combined school focussed exclusively on AI, data science, computational modelling and "digitalisation". This includes the proposal to cease research in Foundations of Computer Science (FoCo) where research is "highly theoretical and not directly linked with applications", retaining staff only if the research they have published in the past (!) aligns well with the new desired focus on foundations of AI, computational modelling, data science and digitalisation. Staff have been given no opportunity to alter their research to fit with the proposed new direction. The plan is to make redundant (in the middle of a pandemic) all (up to 10) staff in foundations of computer science whose past research is deemed not to be a good enough fit with the new strategic priorities.

See also this statement by the University and College Union of the University of Leicester. 

I might be biased, but I find it inconceivable that one can think of building a world-class research programme in AI, data science and computational modelling without building on existing strengths in the Foundations of Computer Science and Mathematics. What my crystal ball tells me is that the strong Leicester academics who might be affected by the planned restructuring will find positions elsewhere and that the University of Leicester is shooting itself in the foot. Which high-profile academic would be enticed to join a university that has shown so little consideration for its existing areas of strength and where one's job might be in danger when the buzzwords du jour change, as they undoubtedly will? 

I encourage you to sign the petition in support of our Leicester colleagues. Kudos to Isobel Armstrong, FBA, for returning her honorary doctorate to the University of Leicester upon hearing of their plans!

Two PhD positions at the Department of Computer Science, Reykjavik University: Model-driven SE for blockchain and smart contracts

The Software and Emerging Technology Lab at the Department of Computer Science, Reykjavik University, is looking for two PhD candidates to work on an ongoing research project on the application of Model Driven Software Engineering principles, methodologies, technologies and abstractions to Blockchain and Smart Contracts. While both positions require strong software development skills and familiarity with the model-driven software engineering approach, the first position will focus on domain analysis and code generation, while the second position is concerned with contract safety and validity and requires knowledge in model verification and validation. The project is based in Iceland. It will be directed by Mohammad Hamdaqa in collaboration with Luca Aceto and Gísli Hjálmtýsson and in close collaboration with Polytechnique Montréal in Canada. The positions are fully funded and include full tuition waiver and a salary in accordance with the Icelandic Research Fund guidelines. Particularly the funding is covering full tuition as well as a stipend of 383,000 ISK per month before taxes for a minimum of three years. 

If you are interested to apply, please send the documents below to the following email addresses: mhamdaqa@ru.is; luca@ru.is; gisli@ru.is

• A copy of your CV and research interests
• A copy of all your transcripts
• A sample publication
• A maximum of one page research statement of your plans for research in your PhD.
• Your intended starting date / and if you need a visa
• For more information about the position and the research topics, do not hesitate to send your enquiries to any of the project collaborators.

Mohammad Hamdaqa  (https://en.ru.is/cress/)
mhamdaqa@ru.is

Luca Aceto (http://icetcs.ru.is/)
email: luca@ru.is

Gísli Hjálmtýsson (https://en.ru.is/fintech/)
email: gisli@ru.is

Informal inquiries about the project and the conditions of work are very welcome. We will start reviewing applications as soon as they arrive and will continue to accept applications until each position is filled. We strongly encourage interested applicants to send their applications as soon as possible and no later than 28 February 2021.

One PhD and one postdoc position at Reykjavik University

Mode(l)s of Verification and Monitorability

Department of Computer Science, Reykjavik University

One PhD and one postdoc position

We invite applications for a total of two positions: one PhD position and one postdoc position, at the Department of Computer Science of Reykjavik University.

The position is part of a research project funded by the Icelandic Research Fund, under the direction of Antonis Achilleos (Reykjavik University), Luca Aceto (Reykjavik University), and Anna Ingolfsdottir (Reykjavik University) in cooperation with Adrian Francalanza (University of Malta) and Karoliina Lehtinen (LIS, Aix-Marseille).

The project continues previous work in the theoretical foundations of runtime verification and its overarching goal is to better understand the properties and push the limits of monitorability in different settings. For more information on the project, please visit

https://sites.google.com/view/antonisachilleos/movemnt 

or contact Antonis Achilleos (email: antonios@ru.is)

The successful candidates will benefit from, and contribute to, the
research environment at the Icelandic Centre of Excellence in
Theoretical Computer Science (ICE-TCS), with research groups on
concurrency, logic and semantics, algorithms, combinatorics. For
information about ICE-TCS and its activities, see

http://icetcs.ru.is/ .

Moreover, they will cooperate with Adrian Francalanza and Karoliina 

Lehtinen during the project work and will benefit from the interaction 

with their research groups at the University of Malta and LIS, Aix-Marseille.

*Qualification requirements*

Applicants for the postdoctoral position should have, or be about to
defend, a PhD degree in computer science or a closely related
field. Moreover, previous knowledge in logic, concurrency theory, or any 

of the project's related areas, and mathematical competence are desirable.

Applicants for the PhD fellowship should have, or be about to obtain, an 

MSc degree in Computer Science, or closely related fields. Some 

background in logic, concurrency theory, or some other of the project's 

related areas, and mathematical competence are desirable.

*Remuneration*

The PhD position provides a stipend of 383,000 ISK per month before 

taxes, and the salary for the postdoc position is 460,000 ISK per month 

before taxes.

*Start date and duration*

The PhD position is for three years, to start as soon as possible.

The postdoc position is for one year, to start in July or August 2021 (the start date is negotiable), and can be renewed for one more year, based on mutual agreement.

*Application details*

Interested applicants should send their CV, including a list of publications, in PDF to all the addresses below, together with a statement outlining their suitability for the project and the names of at least two referees.

Antonis Achilleos
email: antonios@ru.is

Luca Aceto
email: luca@ru.is

Anna Ingolfsdottir
email: annai@ru.is

Adrian Francalanza
email: adrian.francalanza@um.edu.mt

Karoliina Lehtinen
email: lehtinen@lis-lab.fr

Informal inquiries about the project and the conditions of work are very welcome.

We will start reviewing applications as soon as they arrive and will continue to accept applications until each position is filled. We strongly encourage interested applicants to send their applications as soon as possible and no later than 20 February 2021.

Faculty positions at the Department of Computer Science, Reykjavik University

The Department of Computer Science at Reykjavik University is hiring and invites applications for faculty positions at any rank. 

We are looking for energetic, highly qualified academics with a proven international research record.  We particularly welcome applications from researchers who have a strong network of research collaborators, can strengthen internal collaborations within the department, and generally have potential to flourish in our setting. 

We have just posted three separate calls for applications.

• If you are interested in applying for one of the faculty positions in the fields of Data Science, Machine Learning, Software Engineering, and Computer Security, please follow this link for more information on the positions and on how to apply. 
• If you are interested in applying for the faculty position in Game Design and Development, see here for more information on the position and on how to apply.
  
• We also have a call for faculty positions in any area of Computer Science. You can find further information on those positions here. 

Addendum dated 19 November 2020: Scientists coming to Iceland from abroad for work can apply for a tax relief for the first three years of their employment. If the application is successful, 25% of their salary is tax free.

Department of Computer Science at Reykjavik University

The Department of Computer Science at Reykjavik University has about 650 full-time-equivalent students and 22 faculty members. It provides an excellent working environment that encourages and supports independence in academic endeavors, and in which a motivated academic can have impact at all levels. The department offers undergraduate and graduate programs in computer science and software engineering, as well as a combined undergraduate program in discrete mathematics and computer science. The department is home to several research centers producing high-quality collaborative research in areas such as artificial intelligence, financial technology, language technology, software systems, and theoretical computer science, among others; for more information on those research centers, see https://en.ru.is/research/units/.

Reykjavík University 

On the Times Higher Education rankings for 2021, Reykjavík University is ranked in first place along with eight other universities for the average number of citations per faculty. Overall, RU is ranked among the 350 best universities world-wide, 59th of all universities established fewer than 50 years ago, and first among Icelandic universities. Reykjavík University has around 3.700 students and 250 faculty and employees in addition to numerous adjunct faculty in two schools: Technology and Social Sciences. We offer a welcoming and stimulating environment in which to work and live. The University is centrally located in Reykjavík, the capital city of Iceland. The role of Reykjavik University is to create and disseminate knowledge to enhance the competitiveness and quality of life for individuals and society, guided by good ethics, sustainability and responsibility. Education and research at RU are based on strong ties with industry and society. We emphasize interdisciplinary collaboration, international relations and entrepreneurship. 

Iceland 

Iceland is well known for breathtaking natural beauty, with volcanoes, hot springs, lava fields and glaciers offering a dramatic landscape. It consistently ranks as one of the best places in the world to live. It offers a high quality of life, is one of the safest places in the world, has high gender equality, and strong health-care and social-support systems. It is in fourth position in the 2020 UN World Happiness Report, which correlates with various life factors.

An interview with Jos Baeten, outgoing director of the CWI

After nine years, Jos Baeten will step down as general director of CWI on 30 September 2020 and there will be a retirement symposium in his honour on 1 October 2020. (Jos Baeten's successor will be Tom de Kok. You can read the CWI news item related to Tom de Kok's appointment here. Tom de Kok, just like Jos Baeten before him, joins CWI from Eindhoven University of Technology.) 

Jos Baeten has been one of the prime movers in the development of process algebra since 1987, and has been the driving force behind the CONCUR conference series and the CONCUR Basic Research Actions in the late 1980s and the early 1990s. Apart from being general director of CWI, he has served the TCS community in a variety of roles and organisations, and has helped to connect the work of the concurrency-theory community with that done in control and mechanical engineering. He has also supervised more than 30 PhD theses. 

I asked Jos a few questions via email and I am happy to share his answers with the readers of this blog. Thanks to Jos for all the contributions he has given to the research community throughout his career, and for sharing his opinions and reminiscences with us!

The interview 

Luca: Let's start from the beginning. If I remember correctly, your background was in model theory. Could you tell us what prompted you to move to doing research in computer science? 

Jos: I have a Master in logic and foundations of mathematics (with a minor in philosophy) from Utrecht University, with a Master’s thesis on lambda calculus, and a PhD in logic and foundations of mathematics from the University of Minnesota, with a PhD thesis on definability theory (a cross between recursion theory and set theory) entitled "Filters and ultrafilters over definable subsets of admissible ordinals". Returning from the US, I got a job teaching undergraduate maths at Delft University. But I wanted getting into research, and meeting Jan Bergstra he said there were lots of opportunities in computer science research, not in maths. Writing a paper with him and Jan Willem Klop on term rewriting systems would qualify me, he said. So it happened, and I got a postdoc at CWI in the framework of the ESPRIT I project. I kept on doing maths, but it was called computer science. 

Luca: I have heard that you were recruited by Jan Bergstra and Jan Willem Klop to work within their group at the CWI, and that Rob van Glabbeek joined the team soon after you. Could you tell us about the environment at the CWI at that time? It must have been a very exciting place to be with all the activity related to work on ACP and related topics.

Jos: It was a heady period. The group of Jan and Jan Willem was expanding rapidly on EU money, with me, Rob van Glabbeek and Frits Vaandrager. I really liked ACP and doing universal algebra. 

Luca: What was your first paper in CS about? Which paper from your initial period at the CWI are you most proud of? 

Jos: My first paper was "On term rewriting, Term rewriting systems with priorities". I am most proud of my first ACP paper, "Syntax and defining equations for an interrupt mechanism in process algebra". This is about adding the priority operator. For axiomatisation, it needed an auxiliary operator that later turned out to be almost optimal. I came up with an axiomatisation, and Jan Bergstra forced me to prove it correct by doing all the critical pairs. I found a small error in pair 101 (of the 102 pairs), corrected it and proved the result correct. This all in a couple of weeks. 

Luca: Let's move on to the CONCUR project: How did it come about and what was its legacy? I recall that you came to visit Matthew Hennessy at the University of Sussex when I was a PhD student there to discuss the CONCUR proposal. How did you become involved in leading such a large and high profile group of researchers so early in your career at the CWI? What was it like to lead the CONCUR project? 

Jos: This is again due to Jan Bergstra: he believes in delegating responsibilities quickly. When the new instrument of Basic Research Action came up in the EU, he wanted a BRA with Hoare, Milner and Hennessy. I got the assignment and made a trip to the UK visiting all three, and got all of them on board. The idea of the project was unification, but that did not come about, everyone kept doing their own thing. We did, however, produce excellent papers, including the curious 

J.C.M. Baeten, J.A. Bergstra, C.A.R. Hoare, R. Milner, J. Parrow & R. de Simone, The variety of process algebra. Deliverable ESPRIT Basic Research Action 3006, CONCUR, University of Edinburgh 1991

Luca: How would you summarize the history of the conference CONCUR? Can it be split into different periods, and if so, what characterizes them?

Jos: CONCUR 90, which was the first CONCUR conference, was organised by BRA CONCUR, but with speakers from all 5 BRA’s in the area of concurrency; in 1991 Milner did not want such a conference to occur in Edinburgh, so Jan Bergstra and I did it again in Amsterdam. Then, we involved Scott Smolka for 1992 and after that, it was established, with a steering committee comprised of representatives from the 5 BRAs and Scott. As of 1993, it was firmly established, we found a niche and time period (end of August, beginning of September). All branches of concurrency were involved from the start, and over the years, it shows fashion clearly, for instance in certain years there was a lot of pi-calculus.

Luca: In the 80s and the 90s there were three "schools" in process algebra,  the ACP, CCS, and CSP schools. With the benefit of hindsight, which were heir main contributions? To which extent have they converged? Is this classification still important for current research?

Jos: I refer to my paper 

J.C.M. Baeten, A brief history of process algebra. Theoretical Computer Science 335 (2/3), 2005, pp. 131-146. 

I do a comparison in there. In my opinion, the book 

J.C.M. Baeten, T. Basten and M.A. Reniers, Process Algebra: Equational Theories for Communicating Processes. Cambridge Tract in Theoretical Computer Science 50, Cambridge University Press 2010 

has the unification, presenting all three in the same framework. However, process algebra is out of fashion, so who cares?

Luca:  When did you become interested in supervisory control? What motivated you to apply techniques from process algebra in that research field? Looking at the outcome of that work, both in theory and in practice, that was a very good move! Could you tell us about the position you had in Mechanical Engineering? How did it come about and what was it like to work in that department? 

Jos: More than 20 years in the department of computer science, having been dean twice, I got to know the university very well indeed. Koos Rooda, professor of systems engineering at Mechanical Engineering, requested my assistance to get more software engineering into systems engineering, to replace his cooperation with Martin Rem, who became rector. In particular, he was interested in the combination of discrete event reasoning (i.e., process algebra) with the continuous mathematics of systems and control. Having done process algebra with timing and probabilities, I was willing to take up this challenge. Upon his retirement, with the vigorous backing of the dean of Mechanical Engineering at the time, I took over his position. At mid-life, I was ready for a change. I liked the hands-on attitude of mechanical engineering students, who are no good at theory or proofs, but are very good in using mathematics and trying out software tools. But then, I was asked to apply to the vacancy of director of CWI. This was the job I had always wanted. I had enjoyed being dean and doing research management, and CWI is a very prestigious institute with (at that time) very independent management. 

 

Luca: Back at CWI: What skills do you think one needs to be the director of such a high-profile institute? What was your vision for the CWI and how much of it did you manage to achieve? What role do you think the CWI can/should have in the coming decade and beyond? 

Jos: The most important skill is hiring those early career scientists that grow out to become top scientists. Internally, you have to manage your key personnel, operating by consensus and compromise. Externally, you have to find your way in national science politics and always justify your existence. The growing tension between Dutch universities and Dutch extra-university research institutes has almost defeated me, but I managed to complete my term until retirement, and leave CWI in good shape, to my opinion. I managed to keep the excellent reputation of the institute, and also managed to bring in dynamics, rejuvenation and new subjects. What I did not achieve, is that CWI again becomes a publisher, and publishes diamond journals. 

Luca: You have played a role in organizations such as the EATCS, ERCIM and IFIP. Do you think that such societies still play a role today? How do think they should evolve to fulfill their mission? 

Jos: I do, but they have to keep evolving if they want to stay relevant. It is a pity that the EATCS could not take a role in the open access movement (you certainly made a very good effort!). I think ERCIM is doing ok, but not great. IFIP, I think, has become irrelevant. 

Luca: You have been a strong supporter of open access. What is your opinion of the state of play in open access and what do you think we could do to move forward? 

Jos: Progress is slow but exists. I am a strong advocate of Plan S, that has really set some things in motion. A key point is that it looks like we can achieve immediate green, and still allow all researchers to submit articles wherever they want. I do not like the way it is going with transformative agreements, you'd think that by now, publishers would be putting all their efforts to become sellers of data analytics services.

Acknowledgements: I thank Javier Esparza, the chair of the CONCUR Steering Committee, for contributing some the questions to Jos. 

An interview with Hans Hüttel, CONCUR Test-of-Time Award recipient

This post is devoted to the fourth, and last, interview with the colleagues who were selected for the first edition of the CONCUR Test-of-Time Award. (See here for the interview with Davide Sangiorgi,  here for the interview with Nancy Lynch and Roberto Segala, and here for the interview with Rob van Glabbeek.) In keeping with my previous interviews, I asked  Hans  Hüttel (Aalborg University, Denmak) a few questions via email and you can find his answers below. 

Hans receives the award for his paper "Bisimulation Equivalence is Decidable for all Context-Free Processes", which he wrote  with Søren Christensen and Colin Stirling. Søren moved to industry after finishing his PhD. Colin is now retired. 

Luca: You receive one of the two CONCUR ToT Awards for the period 1990-1993 for the paper  "Bisimulation Equivalence is Decidable for all Context-Free Processes" you published with Søren Christensen and Colin Stirling at CONCUR 1992. Could you tell us briefly what the context for that work was and how it came about?

Hans: I was working on my PhD which was on the topic of decidability of behavioural equivalences for process calculi that allow processes to have infinite state spaces. Baeten, Bergstra and Klop had proved that strong bisimilarity is in fact decidable for the BPA calculus even though the class of trace languages for BPA is exactly the class of context-free languages. The result only held for normed BPA processes, that is, processes that could always terminate. Colin was my supervisor in Edinburgh, and he suggested that I try to find a simpler proof of that result (much can be said about the original proof, but simple it was not!). This turned out to be really interesting; I met Didier Caucal from IRISA who had found a nice, much shorter proof that relied on finite characterizations and I was able to use his notion of self-bisimilarity to prove that a tableau system for bisimilarity was sound and complete wrt. bisimilary. Jan Friso Groote, who was a PhD student at the CWI at the time, and myself proved that all other known equivalences are undecidable for normed BPA (and therefore a fortiori also for full, unnormed BPA). But one problem that Colin and I were never able to solve was if the decidability result also held for the full BPA calculus.

Søren arrived in Edinburgh in 1990 and we shared a flat there, in St Leonards Bank just across from Holyrood Park. We hung out with the same people in the LFCS, many of whom were clever Italians such as Davide Sangiorgi and clever quasi-Italians such as Marcelo Fiore. It is no surprise that Søren and I often discussed our work or that he, given that Colin was also his supervisor, moved on to study decidability problems as well, the only difference being that Søren was mostly interested in the BPP calculus that has parallel composition instead of sequential composition.

When I left Edinburgh at the end of August of 1991, Colin and I had managed to make some progress on the decidability problem for unnormed BPA. We realised that a finite characterization of the maximal bisimulation á la Caucal was the way ahead but the actual characterization escaped us. When I returned for my viva in December, Søren had found an important lemma on finite characterizations and everything fell into place. The decidability result relied on proving that bisimilarity is semi-decidable using the finite characterization; non-bisimilarity was already known to be semi-decidable.

Luca: Both Søren Christensen and you wrote the award-winning paper as PhD students in Edinburgh. Could you tell us about the research environment in Edinburgh at that time, and the influence it had on you then and in the rest of your career?

Hans: The LFCS in Edinburgh was a great place to be at the time. Robin Milner was still around and busy working on the pi-calculus together with Davide Sangiorgi, who was his student at the time. Watching them at the blackboard was interesting, even though the rest of us often could not follow their discussions! Gordon Plotkin was there (and still is, fortunately). Rod Burstall was still active, and so was Mike Fourman. Plus many, many others. There was always someone to talk to, and it was perfectly legitimate to have an interest in basic research. Unlike the other professors, Colin had no background in maths – he was originally a philosopher! – and maybe that was why he was trying to avoid heavy mathematical lingo, trying to be simple and precise in his writing at the same time. I learned a lot from him, also in that respect.

After Søren returned to Denmark, he left academia and got a job in the private sector. He still lives near Aarhus. Sadly we lost touch with each other, in all likelihood because our lives turned out so different. We got back in touch recently, when we were told about the reward and we look forward to finally meeting each other again. Colin retired recently, and I really hope to see him again, when I am able to travel to Scotland again some day.

Luca: How much of your later work has built on your award-winning paper? What follow-up results of yours are you most proud of and why?

Hans: I worked on decidability issues for another few years after that but there was no-one to talk to in Aalborg, or rather, there was no-one there that shared my interest in the area at the time. What is more, the open problems that remained were major challenges. Some were only solved much later (such as the decidability of bisimilarity for pushdown automata, a result due to Sénizergues, the proof later greatly simplified by Colin) or remain open (such as the decidability of weak bisimilarity for BPA). Eventually I drifted down the slippery slope and became interested in other, related topics, and focused somewhat more directly on program properties. The follow-up result that most directly relates to my paper with Søren and Colin is the result from 1994 that bisimilarity is also the only equivalence that is decidable for BPP. This is a result that I am also quite proud of. It grew out of discussions with Javier Esparza and Yoram Hirshfeld, when I was back in Edinburgh for a while in 1993. Ironically, there was a subtle flaw in the proof that Naoki Kobayashi discovered many years later. Naoki and one of his student found out how to repair the proof, and the three of us co-authored the journal version that came out many years later. The reason why Naoki became interested in BPP was that he was trying to use the calculus as a behavioural type system for a pi-calculus. As it happened, this was also the route that I had taken.

Those of my later results that I am most proud of have to do with this area: My work on type systems for psi-calculus (CONCUR 2011 and later) and a session type system for bounded name use in the pi-calculus (Acta Informatica 2019). The latter paper also has a CONCUR connection; it grew out of attending a talk by Roland Meyer at CONCUR 2013 and wondering why they were not trying to characterize notions of name-boundedness in the pi-calculus by means of a type system. It turned out that Meyer et al. were not familiar with type systems at all. It took me an awful long time to work out a type-based characterization (using session types), as you can probably tell.

As you can tell, I have not worked on bisimulation for quite some time. Not that there is anything wrong with bisimulation, of course, but if one wants results that are applicable for automated reasoning about program behaviour, decidability is important. One can then either choose to go for a less expressive model of computation (which is what researchers in the model checking community do) or keep the model of computation and go for sound, but incomplete characterizations of program properties (which is what researchers interested in type systems and related static analysis methods do). I ended up in the latter camp.

Luca: To your mind, what are the most interesting or unexpected uses in the literature of the notions and techniques you developed in "Bisimulation Equivalence is Decidable for all Context-Free Processes"?

Hans: BPA, BPP and similar process calculi can be used as the basis of behavioural type systems, and I am thrilled that my old research interests and my current research interests are so directly related.

In 2018 I discovered that Vasco Vasconcelos and Peter Thiemann had devised a session type system for a functional programming language in which session types were not regular expressions (which is essentially what they are in the original work by Honda, Kubo and Vasconcelos) but BPA processes. Vasco and Peter knew that type equivalence should be decidable but they were not so familiar with our results from the early 1990s. At POPL 2019 I attended a talk by Andreia Mordido, one of Vasco’s collaborators, and she mentioned our paper from CONCUR 1992! Later that day, I ended up talking to Andreia and Vasco about my work on BPA from all those years ago.

Luca: The last forty years have seen a huge amount of work on process algebra and process calculi. However, the emphasis on that field of research within concurrency theory seems to have diminished over the last few years, even in Europe. What advice would you give to a young researcher interested in working on process calculi today?

Hans: That they should still work on process calculi! There remains a lot of interesting work to be done. One reason why research topics drift in and out of focus is simply that researchers lose interest; it is hardly ever the case that a topic runs out of interesting research questions. Another reason is rather grim: Basic research is nowhere near as well-respected as it used to be. If you look at the funding schemes that we have today, only the very successful few can get funding for basic research; I am not among them and it does get frustrating quite often. Most topics these days deal with applied research. There is nothing wrong with applied research per se; some of what I do is on that side of things, but there has to be more to research than that.

Luca: What are the research topics that currently excite you the most?

Hans: I have slowly become more and more interested in programming language theory, and some of my current collaborators have taken a similar route, beginning in concurrency theory, drifting into the world of behavioural type systems and finally wanting to apply all of their skills to actual programming languages. Right now Mario Bravetti, Adrian Francalanza, António Ravara and myself are involved in working on a behavioural type system related to the Mungo tool for a subset of Java. I am fortunately enough to have had three exceptionally clever and productive MSc students involved as well, and this has been extremely helpful. Mungo is in many ways the work of Simon Gay and Ornela Dardha at Glasgow University, and they, too, began their careers working on process calculi.

Luca: You have a keen interest in teaching at university level. Is there anything you think we should do better in conveying the beauty and usefulness of theoretical computer science in general, and concurrency theory in particular, to our students today? Do you have any thoughts you'd like to share with us on how to combine digital resources and in-person meetings in the teaching of subjects in the theory of computing?

Hans: Personally I think there is a tendency to present any academic topic – and in particular topics in the mathematical sciences, broadly speaking – in such a way that the definitions and theorems appear as if they fell from the heavens, fully formed. As any researcher will know, that is certainly not how they came about. In this way, we focus a lot on what Imre Lakatos and Karl Popper called the context of justification. A well-honed presentation of a theory may appear to be beautiful, but in my opinion the actual beauty is the one that one experiences when one has finally understood the theory and understands why the definitions and theorem turned out the way they did – that is, one must understand the context of discovery. I think problem-based learning (which is something that we talk about a lot at Aalborg University and at Roskilde University) is the key here, because it puts the focus on student-centered active learning.

I have lectured a lot over the years but since 2013 I have drifted away from traditional lectures towards flipped teaching in which I use pre-recorded podcasts (of my own making) that students can watch whenever they want; I then use the plenary sessions for activities that focus on active learning. I by far prefer having a dialogue with students that focuses on the problems that they encounter to the monologue style of a lecture. All my teaching activities are now flipped and I am happy to say that some of my colleagues are now thinking along similar lines. It is always good to have someone to talk to.