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,
from the 1st of May 2019), 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, 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)]
- Valentina Castiglioni, Konstantinos Chatzikokolakis and Catuscia Palamidessi.
Logical Characterization of Differential Privacy.
Science of Computer Programming 188, 2020.
[Official publisher version (DOI)]
- 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)]
- Valentina Castiglioni and Simone Tini.
Probabilistic Divide and Congruence: Branching Bismilarity.
Theoretical Computer Science 802: 147-196, 2020.
[Official publisher version (DOI)]
- Valentina Castiglioni and Simone Tini.
Raiders of the Lost Equivalence: Probabilistic Branching Bismilarity.
Information Processing Letters, 2020, to appear.
Conference and workshop papers
- 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.
- 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
- 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
- Anonymous Author(s). Are Two Binary Operators Necessary to Finitely
Axiomatise Parallel Composition?. Submitted.