On the axiomatizability of impossible futures

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

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)
35 Downloads (Pure)


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.

Original languageEnglish
Article number17
Number of pages31
JournalLogical Methods in Computer Science
Issue number3
Publication statusPublished - 22 Sep 2015
Externally publishedYes


  • Concurrency theory
  • Equational logic
  • Impossible futures
  • Process algebra


Dive into the research topics of 'On the axiomatizability of impossible futures'. Together they form a unique fingerprint.

Cite this