On the axiomatisability of priority III: Priority strikes again

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

doi:10.1016/j.tcs.2020.07.044

On the axiomatisability of priority III: Priority strikes again

Luca Aceto
, Elli Anastasiadi
, Valentina Castiglioni (Corresponding author)
, Anna Ingólfsdóttir
, Bas Luttik
, Mathias Ruggaard Pedersen

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

2 Citations (Scopus)

Abstract

Aceto et al., proved that, over the process algebra BCCSP with the priority operator of Baeten, Bergstra and Klop, the equational theory of order-insensitive bisimilarity is not finitely based. However, it was noticed that by substituting the action prefixing operator of BCCSP with BPA's sequential composition, the infinite family of equations used to show that non-finite axiomatisability result could be proved by a finite collection of sound equations. That observation left as an open question the existence of a finite axiomatisation for order-insensitive bisimilarity over BPA with the priority operator. In this paper we provide a negative answer to this question. We prove that, in the presence of at least two actions, order-insensitive bisimilarity is not finitely based over BPA with priority.

Original language	English
Pages (from-to)	223-246
Number of pages	24
Journal	Theoretical Computer Science
Volume	837
DOIs	https://doi.org/10.1016/j.tcs.2020.07.044
Publication status	Published - 12 Oct 2020

Funding

We thank the reviewers for their constructive feedback and careful reading of our paper. The work reported in this paper has been supported by the project ‘ Open Problems in the Equational Logic of Processes ’ (OPEL) of the Icelandic Research Fund (grant nr. 196050-051 ).

Keywords

Bisimilarity
Finite axiomatisations
Priority operator
Sequential composition

Access to Document

10.1016/j.tcs.2020.07.044

Cite this

@article{d81cc1c05c1a4c3ab51ee41ced6fc597,

title = "On the axiomatisability of priority III: Priority strikes again",

abstract = "Aceto et al., proved that, over the process algebra BCCSP with the priority operator of Baeten, Bergstra and Klop, the equational theory of order-insensitive bisimilarity is not finitely based. However, it was noticed that by substituting the action prefixing operator of BCCSP with BPA's sequential composition, the infinite family of equations used to show that non-finite axiomatisability result could be proved by a finite collection of sound equations. That observation left as an open question the existence of a finite axiomatisation for order-insensitive bisimilarity over BPA with the priority operator. In this paper we provide a negative answer to this question. We prove that, in the presence of at least two actions, order-insensitive bisimilarity is not finitely based over BPA with priority.",

keywords = "Bisimilarity, Finite axiomatisations, Priority operator, Sequential composition",

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

year = "2020",

month = oct,

day = "12",

doi = "10.1016/j.tcs.2020.07.044",

language = "English",

volume = "837",

pages = "223--246",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - On the axiomatisability of priority III

T2 - Priority strikes again

AU - Aceto, Luca

AU - Anastasiadi, Elli

AU - Castiglioni, Valentina

AU - Ingólfsdóttir, Anna

AU - Luttik, Bas

AU - Ruggaard Pedersen, Mathias

PY - 2020/10/12

Y1 - 2020/10/12

N2 - Aceto et al., proved that, over the process algebra BCCSP with the priority operator of Baeten, Bergstra and Klop, the equational theory of order-insensitive bisimilarity is not finitely based. However, it was noticed that by substituting the action prefixing operator of BCCSP with BPA's sequential composition, the infinite family of equations used to show that non-finite axiomatisability result could be proved by a finite collection of sound equations. That observation left as an open question the existence of a finite axiomatisation for order-insensitive bisimilarity over BPA with the priority operator. In this paper we provide a negative answer to this question. We prove that, in the presence of at least two actions, order-insensitive bisimilarity is not finitely based over BPA with priority.

AB - Aceto et al., proved that, over the process algebra BCCSP with the priority operator of Baeten, Bergstra and Klop, the equational theory of order-insensitive bisimilarity is not finitely based. However, it was noticed that by substituting the action prefixing operator of BCCSP with BPA's sequential composition, the infinite family of equations used to show that non-finite axiomatisability result could be proved by a finite collection of sound equations. That observation left as an open question the existence of a finite axiomatisation for order-insensitive bisimilarity over BPA with the priority operator. In this paper we provide a negative answer to this question. We prove that, in the presence of at least two actions, order-insensitive bisimilarity is not finitely based over BPA with priority.

KW - Bisimilarity

KW - Finite axiomatisations

KW - Priority operator

KW - Sequential composition

UR - https://www.scopus.com/pages/publications/85089253991

U2 - 10.1016/j.tcs.2020.07.044

DO - 10.1016/j.tcs.2020.07.044

M3 - Article

AN - SCOPUS:85089253991

SN - 0304-3975

VL - 837

SP - 223

EP - 246

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

On the axiomatisability of priority III: Priority strikes again

Abstract

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this