On the axiomatizability of impossible futures

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

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

1 Citaat (Scopus)
30 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
Artikelnummer17
Aantal pagina's31
TijdschriftLogical Methods in Computer Science
Volume11
Nummer van het tijdschrift3
DOI's
StatusGepubliceerd - 22 sep 2015
Extern gepubliceerdJa

Vingerafdruk

Duik in de onderzoeksthema's van 'On the axiomatizability of impossible futures'. Samen vormen ze een unieke vingerafdruk.

Citeer dit