Open Problems in the equational Logic of Processes
Icelandic Research Fund Project nr. 196050-051 (2019-to date)
Status: Ongoing

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. In particular, the project aims at

obtaining complete equational axiomatizations of various notions of bisimilarity over terms (possibly including variables) in the recursion-free fragment of Milner's Calculus of Communicating Systems (CCS), using suitable auxiliary operators,
extending classic nonfinite axiomatizability results for strong bisimilarity over CCS to the setting of equivalences abstracting from internal steps in computations, and
developing general techniques for transferring positive and negative results on the existence of finite equational axiomatizations of process equivalences between languages and between versions of behavioural equivalences that differ in their treatment of internal steps in process behaviours.

Despite over thirty years of work in the field of algebraic process theory, those problems have not been completely solved in the literature. Thus, the results obtained within this project will lead to an improved understanding of the power of the classic logic of equations in describing and reasoning about a ubiquitous class of computing systems, and will have impact on future work on algebraic methods in concurrency theory. Moreover, the techniques used to achieve them will expand the toolbox of the working concurrency theorist and will be applied to specific, unsolved axiomatic questions that are within the scope of the project. The axiomatizations obtained within the project may also be applied in the computer-assisted analysis of concurrent systems using theorem-proving technology. Last, but not least, apart from the intrinsic scientific interest of the proposed work, building on the successful Polymath experience, the project will be the first one in concurrency theory (and perhaps in computer science as a whole) that uses large-scale on-line collaboration to solve problems in that field, thus providing a blueprint for future research cooperation.

Researchers

The research team includes Luca Aceto (PI, Reykjavik University and Gran Sasso Science Institute), Elli Anastasiadi (PhD student at Reykjavik University), Valentina Castiglioni (postdoctoral researcher at Reykjavik University, from the 15th of May 2019), Clemens Grabmayer (Gran Sasso Science Institute), Anna Ingolfsdottir (co-PI, Reykjavik University), Bas Luttik (co-proposer, TU Eindhoven, NL), Mathias Ruggaard Pedersen (postdoctoral researcher at Reykjavik University, 1 May 2019-20 May 2020), and Alexandra Silva (co-proposer, University College London, UK).

Project-related key events and news

12-16 August 2019: Bas Luttik (TU Eindhoven) visits ICE-TCS.
12-15 August 2019: Jurriaan Rot (Radboud University Nijmegen and University College London) and Tobias Kappé (University College London) visit ICE-TCS.

Publications

Accepted and published papers

Journal papers

L. Aceto, V. Castiglioni, W. Fokkink, A. Ingolfsdottir and B. Luttik. Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition? . ACM Transactions on Computational Logic, 2022. [Official publisher version (DOI)]
L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik and M. R. Pedersen. On the axiomatisability of parallel composition . Logical Methods in Computer Science 18(1), 2022. [Official publisher version (DOI)]
L. Aceto, I. Fabregas, C. Gregorio-Rodriguez and A. Ingolfsdottir. Logical characterisations and compositionality of input-output conformance simulation. Journal of Logical and Algebraic Methods in Programming 106:78-106, Elsevier, August 2019. [Official publisher version (DOI)]
L. Aceto, E. Anastasiadi, V. Castiglioni, A. Ingolfsdottir, B. Luttik and M. R. Pedersen. On the axiomatisability of priority III: Priority strikes again . Theoretical Computer Science 837:223-246, 2020. [Official publisher version (DOI)]
V. Castiglioni, K. Chatzikokolakis and C. Palamidessi. Logical Characterization of Differential Privacy. Science of Computer Programming 188, 2020. [Official publisher version (DOI)]
V. Castiglioni, M. Loreti and S. Tini. The Metric Linear Time - Branching Time Spectrum on Nondeterministic Probabilistic Processes. Theoretical Computer Science 813: 20-69, 2020. [Official publisher version (DOI)]
V. Castiglioni and S. Tini. Probabilistic Divide and Congruence: Branching Bismilarity. Theoretical Computer Science 802: 147-196, 2020. [Official publisher version (DOI)]
V. Castiglioni and S. Tini. Raiders of the Lost Equivalence: Probabilistic Branching Bismilarity. Information Processing Letters 159-160: 105947, 2020. [Official publisher version (DOI)]

Conference and workshop papers

L. Aceto, E. Anastasiadi, V. Castiglioni, A. Ingolfsdottir and B. Luttik. In search of lost time: Axiomatising parallel composition in process algebras. Proceedings of LICS 2021 (invited paper), IEEE, pp. 1-14, 2021. [Official publisher version (DOI)]
L. Aceto, E. Anastasiadi, V. Castiglioni, A. Ingolfsdottir and M. R. Pedersen. On the axiomatizability of priority III: The return of sequential composition. Proceedings of ICTCS 2019, the 20th Italian Conference on Theoretical Computer Science, CEUR Workshop Proceedings 2504: 145-157, September 2019.
L. Aceto, E. Anastasiadi and A. Ingolfsdottir. An axiomatisation of verdict equivalence over regular monitors. Selected for presentation at the 12th Panhellenic Logic Symposium, Anogeia, Crete, Greece, 26-30 June 2019.
Luca Aceto, Jos C. M. Baeten, Patricia Bouyer-Decitre, Holger Hermanns, Alexandra Silva. CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper). Proceedings of CONCUR 2020, LIPIcs 171, pp. 5:1-5:3, 2020.
L. Aceto, V. Castiglioni, W. Fokkink, A. Ingolfsdottir and B. Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition? . Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs 183, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
L. Aceto, V. Castiglioni, A. Ingolfsdottir, B. Luttik and M. R. Pedersen. On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. Proceedings of CONCUR 2020, LIPIcs 171, pp. 18:1-18:22, 2020. [Official publisher version (DOI)]
V. Castiglioni, M. Loreti and S. Tini. Measuring Adaptability and Reliability of Large Scale Systems . Proceedings of ISoLA, part 2, Lecture Notes in Computer Science 12477, pp. 380-396, 2020. [Official publisher version (DOI)]
V. Castiglioni, M. Loreti and S. Tini. How Adaptive and Reliable is Your Program? Proceedings of FORTE, Lecture Notes in Computer Science 12719, pp. 60-79, 2021. [Official publisher version (DOI)]

Book chapters

V. Castiglioni, R. Lanotte and S. Tini. Fully Syntactic Uniform Continuity Formats for Bisimulation Metrics. In M. Alvim, K. Chatzikokolakis, C. Olarte and F. Valencia (eds) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. Springer, 2019

Submitted papers

L. Aceto, A. Achilleos, E. Anastasiadi and A. Ingolfsdottir. An axiomatisation of verdict equivalence over regular monitors. Submitted for journal publication.

Open Problems in the equational Logic of Processes Icelandic Research Fund Project nr. 196050-051 (2019-to date) Status: Ongoing