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

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

doi:10.4230/LIPIcs.CONCUR.2020.18

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

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

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Citations (Scopus)

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 language	English
Title of host publication	31st International Conference on Concurrency Theory, CONCUR 2020
Editors	Igor Konnov, Laura Kovacs
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	1-22
ISBN (Electronic)	9783959771603
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2020.18
Publication status	Published - 2020
Event	31st International Conference on Concurrency Theory, CONCUR 2020 - Virtual, Vienna, Austria Duration: 1 Sept 2020 → 4 Sept 2020

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	171
ISSN (Print)	1868-8969

Conference

Conference	31st International Conference on Concurrency Theory, CONCUR 2020
Country/Territory	Austria
City	Virtual, Vienna
Period	1/09/20 → 4/09/20

Bibliographical note

Funding Information:
Funding This work has been supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051).

Publisher Copyright:
© Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen; licensed under Creative Commons License CC-BY 31st International Conference on Concurrency Theory (CONCUR 2020).

Other keywords

Axiomatisation
Linear time-branching time spectrum
Parallel composition

Access to Document

10.4230/LIPIcs.CONCUR.2020.18Licence: CC BY

Cite this

Aceto, L., Castiglioni, V., Ingólfsdóttir, A., Luttik, B., & Pedersen, M. R. (2020). On the axiomatisability of parallel composition: A journey in the spectrum. In I. Konnov, & L. Kovacs (Eds.), 31st International Conference on Concurrency Theory, CONCUR 2020 (pp. 1-22). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 171). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2020.18

Aceto, Luca ; Castiglioni, Valentina ; Ingólfsdóttir, Anna et al. / On the axiomatisability of parallel composition : A journey in the spectrum. 31st International Conference on Concurrency Theory, CONCUR 2020. editor / Igor Konnov ; Laura Kovacs. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. pp. 1-22 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{1c632895f93347878e3552dd93d5dc6f,

title = "On the axiomatisability of parallel composition: A journey in the spectrum",

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.",

keywords = "Axiomatisation, Linear time-branching time spectrum, Parallel composition",

author = "Luca Aceto and Valentina Castiglioni and Anna Ing{\'o}lfsd{\'o}ttir and Bas Luttik and Pedersen, {Mathias Ruggaard}",

note = "Funding Information: Funding This work has been supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051). Publisher Copyright: {\textcopyright} Luca Aceto, Valentina Castiglioni, Anna Ing{\'o}lfsd{\'o}ttir, Bas Luttik, and Mathias Ruggaard Pedersen; licensed under Creative Commons License CC-BY 31st International Conference on Concurrency Theory (CONCUR 2020).; 31st International Conference on Concurrency Theory, CONCUR 2020 ; Conference date: 01-09-2020 Through 04-09-2020",

year = "2020",

doi = "10.4230/LIPIcs.CONCUR.2020.18",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "1--22",

editor = "Igor Konnov and Laura Kovacs",

booktitle = "31st International Conference on Concurrency Theory, CONCUR 2020",

address = "Germany",

}

Aceto, L, Castiglioni, V, Ingólfsdóttir, A, Luttik, B & Pedersen, MR 2020, On the axiomatisability of parallel composition: A journey in the spectrum. in I Konnov & L Kovacs (eds), 31st International Conference on Concurrency Theory, CONCUR 2020. Leibniz International Proceedings in Informatics, LIPIcs, vol. 171, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-22, 31st International Conference on Concurrency Theory, CONCUR 2020, Virtual, Vienna, Austria, 1/09/20. https://doi.org/10.4230/LIPIcs.CONCUR.2020.18

On the axiomatisability of parallel composition: A journey in the spectrum. / Aceto, Luca; Castiglioni, Valentina; Ingólfsdóttir, Anna et al.
31st International Conference on Concurrency Theory, CONCUR 2020. ed. / Igor Konnov; Laura Kovacs. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. p. 1-22 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 171).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On the axiomatisability of parallel composition

T2 - 31st International Conference on Concurrency Theory, CONCUR 2020

AU - Aceto, Luca

AU - Castiglioni, Valentina

AU - Ingólfsdóttir, Anna

AU - Luttik, Bas

AU - Pedersen, Mathias Ruggaard

N1 - Funding Information: Funding This work has been supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051). Publisher Copyright: © Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen; licensed under Creative Commons License CC-BY 31st International Conference on Concurrency Theory (CONCUR 2020).

PY - 2020

Y1 - 2020

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

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

KW - Axiomatisation

KW - Linear time-branching time spectrum

KW - Parallel composition

UR - http://www.scopus.com/inward/record.url?scp=85091560477&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CONCUR.2020.18

DO - 10.4230/LIPIcs.CONCUR.2020.18

M3 - Conference contribution

AN - SCOPUS:85091560477

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 1

EP - 22

BT - 31st International Conference on Concurrency Theory, CONCUR 2020

A2 - Konnov, Igor

A2 - Kovacs, Laura

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Y2 - 1 September 2020 through 4 September 2020

ER -

Aceto L, Castiglioni V, Ingólfsdóttir A, Luttik B, Pedersen MR. On the axiomatisability of parallel composition: A journey in the spectrum. In Konnov I, Kovacs L, editors, 31st International Conference on Concurrency Theory, CONCUR 2020. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2020. p. 1-22. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.CONCUR.2020.18

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

Abstract

Publication series

Conference

Bibliographical note

Other keywords

Access to Document

Fingerprint

Cite this