Trustworthy Systems

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},
    journal          = {Logical Methods in Computer Science},
    keywords         = {concurrency, process algebra, bccs, labeled transition systems, complete axiomatizations, impossible
                        futures semantics.},
    month            = sep,
    number           = {3},
    pages            = {1--31},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8502.pdf},
    title            = {On the Axiomatizability of Impossible Futures},
    volume           = {11},
    year             = {2015}
  }

Download