Monday, January 14, 2019

One postdoc position available at Reykjavik University

Open Problems in the Equational Logic of Processes

School of Computer Science, Reykjavik University

One Postdoc Position

Applications are invited for one post-doctoral position at the School of Computer Science, Reykjavik University.  The position is part of a three-year research project funded by the Icelandic Research Fund, under the direction of Luca Aceto (Gran Sasso Science Institute and Reykjavik Universityand Anna Ingolfsdottir (Reykjavik University) in cooperation with Bas Luttik (TU Eindhoven) and Alexandra Silva (University College London). The overarching goal of this project is to solve some of the challenging open problems in the equational axiomatization of behavioural equivalences over process calculi. Interested applicants can contact Luca Aceto (email: for further details on the research proposal.

The successful candidate will benefit from, and contribute to, the research environment at the Icelandic Centre of Excellence in Theoretical Computer Science (ICE-TCS). For information about ICE-TCS and its activities, see

Moreover, she/he will cooperate with Bas Luttik and Alexandra Silva  during the project work and will benefit from the interaction with their research groups at TU Eindhoven and University College London. The postdoc will also have a chance to interact with Clemens Grabmayer and the CS group at the Gran Sasso Science Institute (, L'Aquila, Italy. 

Qualification requirements
Applicants for the postdoctoral position should have, or be about to hold, a PhD degree in Computer Science or closely related fields. Previous knowledge of at least one of concurrency theory, process calculi, (structural) operational semantics and logic in computer science is highly desirable.

The wage for the postdoctoral position is 
530,000 ISK (roughly 3,830  € at the present exchange rate) per month before taxes. (See for information on what the wage will be after taxes.) The position is for two years, starting as soon as possible, and is renewable for another year, based on good performance and mutual satisfaction.

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.

Luca Aceto

Anna Ingolfsdottir

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

Tuesday, January 01, 2019

Thirty-five years of "Testing Equivalences for Processes" (TCS edition)

Thirty-five years ago, Rocco De Nicola and Matthew Hennessy published the archival paper introducing the notions of testing equivalence over concurrent processes in the journal Theoretical Computer Science. These testing equivalences embody in a natural and mathematically elegant way the intuitive idea that two processes should be equated unless they behave differently when subjected to some ‘experiment’ or ‘test’. The origin of this notion of equivalence can be traced back to Gottfried Wilhelm Leibniz (1646–1716), who stated that two mathematical objects are equal if there is no test to distinguish them. In the semantics of programming languages, its earliest precursor is, to the best of my  knowledge, the notion of contextual equivalence proposed by Morris in his doctoral dissertation.

In general, given a set of processes, a set of tests and a relation between processes and tests that describes when a process passes a test, one can apply Leibniz’s motto and declare two processes to be equivalent if if they pass exactly the same set of tests. In the work of De Nicola and Hennessy, processes are states in some labelled transition system. A test is itself a process, which interacts with a concurrent system under observation by hand-shake synchronisation and uses a distinguished action to report success in its observation. Since both processes and tests may be nondeterministic, the interaction between a process and a test may lead to different outcomes depending on how the two systems resolve their nondeterministic choices in the course of a computation. This led De Nicola and Hennessy to define three notions of testing semantics, which are naturally expressed in terms of preorders over processes.

In the so-called may semantics, a process q is at least as good as some process p if the set of tests that p may pass is included in the set of tests that q may pass. In may semantics, possible failure under a test is immaterial and therefore nondeterminism is angelic. On the other hand, one may take the view that failure in the testing effort is catastrophic, in the sense that a process that may fail some test is just as bad as one that always fails it. The notion of testing semantics that captures this viewpoint is the so-called must semantics, according to which a process q is at  least as good as some process p if the set of tests that p must pass is included in the set of tests that q must pass. Finally, a third testing preorder over processes is obtained as the intersection of the may and must preorders described above. According to this more refined view of process behaviour, a process that always fails a test is worse than one that may pass that test, which in turn is worse than one that always passes it.

De Nicola and Hennessy explored the rich theory of the testing semantics in their seminal TCS paper (see this monograph for a classic, book-length treatment), where each of these semantics is given operational, denotational and axiomatic accounts that are in agreement one with the other. Their ideas and the accompanying technical results have had an enormous impact on further research, as witnessed, among other things, by the 1,640 citations to the TCS paper published in 1984 (source: Google Scholar today).

Happy 2019 to everyone.