Lifting non-finite axiomatizability results to extensions of process algebras

L. Aceto, W.J. Fokkink, A. Ingolfsdottir, M.R. Mousavi

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. © 2010 Springer-Verlag.
Original languageEnglish
Pages (from-to)147-177
JournalActa Informatica
Volume47
Issue number3
DOIs
Publication statusPublished - 2010

Fingerprint

Algebra
Acoustic waves

Cite this

Aceto, L. ; Fokkink, W.J. ; Ingolfsdottir, A. ; Mousavi, M.R. / Lifting non-finite axiomatizability results to extensions of process algebras. In: Acta Informatica. 2010 ; Vol. 47, No. 3. pp. 147-177.
@article{9e8affc4e7cb411e952e03688815a541,
title = "Lifting non-finite axiomatizability results to extensions of process algebras",
abstract = "This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. {\circledC} 2010 Springer-Verlag.",
author = "L. Aceto and W.J. Fokkink and A. Ingolfsdottir and M.R. Mousavi",
year = "2010",
doi = "10.1007/s00236-010-0114-7",
language = "English",
volume = "47",
pages = "147--177",
journal = "Acta Informatica",
issn = "0001-5903",
publisher = "Springer New York",
number = "3",

}

Lifting non-finite axiomatizability results to extensions of process algebras. / Aceto, L.; Fokkink, W.J.; Ingolfsdottir, A.; Mousavi, M.R.

In: Acta Informatica, Vol. 47, No. 3, 2010, p. 147-177.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Lifting non-finite axiomatizability results to extensions of process algebras

AU - Aceto, L.

AU - Fokkink, W.J.

AU - Ingolfsdottir, A.

AU - Mousavi, M.R.

PY - 2010

Y1 - 2010

N2 - This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. © 2010 Springer-Verlag.

AB - This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. © 2010 Springer-Verlag.

U2 - 10.1007/s00236-010-0114-7

DO - 10.1007/s00236-010-0114-7

M3 - Article

VL - 47

SP - 147

EP - 177

JO - Acta Informatica

JF - Acta Informatica

SN - 0001-5903

IS - 3

ER -