On the axiomatisability of parallel composition: A journey in the spectrum

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, Mathias Ruggaard Pedersen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.

Original languageEnglish
Title of host publication31st International Conference on Concurrency Theory, CONCUR 2020
EditorsIgor Konnov, Laura Kovacs
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages181-1822
Number of pages1642
ISBN (Electronic)9783959771603
DOIs
Publication statusPublished - 1 Aug 2020
Event31st International Conference on Concurrency Theory, CONCUR 2020 - Virtual, Vienna, Austria
Duration: 1 Sep 20204 Sep 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume171
ISSN (Print)1868-8969

Conference

Conference31st International Conference on Concurrency Theory, CONCUR 2020
CountryAustria
CityVirtual, Vienna
Period1/09/204/09/20

Keywords

  • Axiomatisation
  • Linear time-branching time spectrum
  • Parallel composition

Fingerprint Dive into the research topics of 'On the axiomatisability of parallel composition: A journey in the spectrum'. Together they form a unique fingerprint.

Cite this