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 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, from the 1st of May 2019), and Alexandra Silva (co-proposer, University College London, UK).

Project-related key events and news

Publications

Accepted and published papers

Journal papers

  1. 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)]
  2. Valentina Castiglioni, Konstantinos Chatzikokolakis and Catuscia Palamidessi. Logical Characterization of Differential Privacy. Science of Computer Programming 188, 2020. [Official publisher version (DOI)]
  3. Valentina Castiglioni, Michele Loreti and Simone Tini. The Metric Linear Time - Branching Time Spectrum on Nondeterministic Probabilistic Processes. Theoretical Computer Science 813: 20-69, 2020. [Official publisher version (DOI)]
  4. Valentina Castiglioni and Simone Tini. Probabilistic Divide and Congruence: Branching Bismilarity. Theoretical Computer Science 802: 147-196, 2020. [Official publisher version (DOI)]
  5. Valentina Castiglioni and Simone Tini. Raiders of the Lost Equivalence: Probabilistic Branching Bismilarity. Information Processing Letters, 2020, to appear.

Conference and workshop papers

  1. L. Aceto, E. Anastasiadi, V. Castiglioni, A. Ingolfsdottir and M. Ruggaard 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.
  2. 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.

Book chapters

  1. 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

  1. Anonymous Author(s). Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. Submitted.