Skip to main content
CSIRO Logo Data 61 logo

On the axiomatizability of impossible futures

Authors

Rob van Glabbeek, Taolue Chen and Wan Fokkink

NICTA

UNSW

Middlesex University
London

VU University
Amsterdam

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 omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finite, sound, ground-complete axiomatization for the weak impossible futures preorder. In contrast, we prove that no finite, sound axiomatization for BCCS modulo concrete and weak impossible futures equivalence is ground-complete. If the alphabet of actions is infinite, then the aforementioned ground-complete axiomatizations are shown to be omega-complete. If the alphabet is finite, we prove that the inequational theories of BCCS modulo the concrete and weak impossible futures preorder lack such a finite basis.

BibTeX Entry

  @article{vanGlabbeek_CF_15,
    author           = {van Glabbeek, Robert and Chen, Taolue and Fokkink, Wan},
    doi              = {10.2168/LMCS-11(3:17)2015},
    number           = {3},
    month            = sep,
    year             = {2015},
    keywords         = {concurrency, process algebra, bccs, labeled transition systems, complete axiomatizations, impossible
                        futures semantics.},
    title            = {On the Axiomatizability of Impossible Futures},
    volume           = {11},
    pages            = {1--31},
    journal          = {Logical Methods in Computer Science},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/8502.pdf}
  }

Download