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

Department of Computer Science

Research output: Contribution to journal › Article › peer-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. 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
Pages (from-to)	15:1-15: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 - 19 Jan 2022

Bibliographical note

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.

Other keywords

Axiomatisation
Linear time-branching time spectrum
Parallel composition

Access to Document

10.46298/LMCS-18(1:15)2022

Cite this

@article{37bc3c1db25b474eadd15221948b2207,

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 = "19",

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

language = "English",

volume = "18",

pages = "15:1--15:51",

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/19

Y1 - 2022/1/19

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 - http://www.scopus.com/inward/record.url?scp=85123532197&partnerID=8YFLogxK

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

SP - 15:1-15:51

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 1

ER -

ON THE AXIOMATISABILITY OF PARALLEL COMPOSITION

Abstract

Bibliographical note

Other keywords

Access to Document

Fingerprint

Cite this