hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Lifting non-finite axiomatizability results to extensions of process algebras
School of Computer Science, Reykjavík University, Kringlan 1, 103 Reykjavík, Iceland.
Department of Computer Science, Vrije Universiteit Amsterdam, 1081 HV Amsterdam, Netherlands.
School of Computer Science, Reykjavík University, Kringlan 1, 103 Reykjavík, Iceland.
Department of Computer Science, Eindhoven University of Technology, 5600 MB Eindhoven, Netherlands.ORCID iD: 0000-0002-4869-6794
2010 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 47, no 3, 147-177 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2010. Vol. 47, no 3, 147-177 p.
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:hh:diva-20520DOI: 10.1007/s00236-010-0114-7ISI: 000276699100001Scopus ID: 2-s2.0-77952668658OAI: oai:DiVA.org:hh-20520DiVA: diva2:584483
Available from: 2013-01-09 Created: 2013-01-08 Last updated: 2014-11-11Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mousavi, Mohammad Reza
In the same journal
Acta Informatica
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 97 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf