On the axiomatizability of impossible futures

T. Chen, W.J. Fokkink, R.J. van Glabbeek

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves ω completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and ω complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a ω nite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a ω nite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no ω nite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is in_nite, then the aforementioned ground- complete axiomatizations are shown to be ω complete. If the alphabet is ω nite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a ω nite basis.
Original languageEnglish
JournalLogical Methods in Computer Science
Volume11
Issue number3
DOIs
Publication statusPublished - 2015

Fingerprint

Axiomatization
Semantics
Concretes
Acoustic waves
Preorder
Modulo
Algebra
Trace
Process Algebra
Completeness
Equivalence
Imply
Sound

Cite this

@article{bc97c867847544528dca016509312b4c,
title = "On the axiomatizability of impossible futures",
abstract = "A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves ω completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and ω complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a ω nite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a ω nite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no ω nite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is in_nite, then the aforementioned ground- complete axiomatizations are shown to be ω complete. If the alphabet is ω nite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a ω nite basis.",
author = "T. Chen and W.J. Fokkink and {van Glabbeek}, R.J.",
year = "2015",
doi = "10.2168/LMCS-11(3:17)2015",
language = "English",
volume = "11",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "3",

}

On the axiomatizability of impossible futures. / Chen, T.; Fokkink, W.J.; van Glabbeek, R.J.

In: Logical Methods in Computer Science, Vol. 11, No. 3, 2015.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - On the axiomatizability of impossible futures

AU - Chen, T.

AU - Fokkink, W.J.

AU - van Glabbeek, R.J.

PY - 2015

Y1 - 2015

N2 - A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves ω completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and ω complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a ω nite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a ω nite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no ω nite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is in_nite, then the aforementioned ground- complete axiomatizations are shown to be ω complete. If the alphabet is ω nite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a ω nite basis.

AB - A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves ω completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and ω complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a ω nite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a ω nite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no ω nite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is in_nite, then the aforementioned ground- complete axiomatizations are shown to be ω complete. If the alphabet is ω nite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a ω nite basis.

U2 - 10.2168/LMCS-11(3:17)2015

DO - 10.2168/LMCS-11(3:17)2015

M3 - Article

VL - 11

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

ER -