On the Axiomatisability of Parallel Composition

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

doi:10.46298/LMCS-18(1:15)2022

On the Axiomatisability of Parallel Composition

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

Research output: Contribution to journal › Article › Academic › peer-review

1 Citation (Scopus)

56 Downloads (Pure)

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. We also show that no congruence over BCCSP 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
Article number	15
Number of pages	51
Journal	Logical Methods in Computer Science
Volume	18
Issue number	1
DOIs	https://doi.org/10.46298/LMCS-18(1:15)2022
Publication status	Published - 29 Jan 2022

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

Keywords

Axiomatisation
Linear time-branching time spectrum
Parallel composition

Access to Document

10.46298/LMCS-18(1:15)2022

pdfFinal published version, 544 KBLicence: CC BY

Cite this

@article{2328b5ecc98a4a29a58fd4b06edaceef,

title = "On the Axiomatisability of Parallel Composition",

abstract = "This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek{\textquoteright}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. We also show that no congruence over BCCSP 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: This work has been supported by the project {\textquoteleft}Open Problems in the Equational Logic of Processes{\textquoteright} (OPEL) of the Icelandic Research Fund (grant No. 196050-051). Publisher Copyright: {\textcopyright} L. Aceto, V. Castiglioni, A. Ing{\'o}lfsd{\'o}ttir, B. Luttik, and M. R. Pedersen.",

year = "2022",

month = jan,

day = "29",

doi = "10.46298/LMCS-18(1:15)2022",

language = "English",

volume = "18",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "1",

}

TY - JOUR

T1 - On the Axiomatisability of Parallel Composition

AU - Aceto, Luca

AU - Castiglioni, Valentina

AU - Ingólfsdóttir, Anna

AU - Luttik, Bas

AU - Pedersen, Mathias Ruggaard

N1 - Funding Information: 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: © L. Aceto, V. Castiglioni, A. Ingólfsdóttir, B. Luttik, and M. R. Pedersen.

PY - 2022/1/29

Y1 - 2022/1/29

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. We also show that no congruence over BCCSP 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. We also show that no congruence over BCCSP 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 - https://www.scopus.com/pages/publications/85123532197

U2 - 10.46298/LMCS-18(1:15)2022

DO - 10.46298/LMCS-18(1:15)2022

M3 - Article

AN - SCOPUS:85123532197

SN - 1860-5974

VL - 18

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 1

M1 - 15

ER -

On the Axiomatisability of Parallel Composition

Abstract

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this