On the Axiomatizability of Impossible Futures

TL;DR

This paper develops a method to derive complete axiomatizations for weak semantics from concrete ones in process algebra, applies it to various semantics, and analyzes the finiteness and completeness properties of these axiomatizations.

Contribution

It introduces a general transformation technique for axiomatizations in BCCS, preserving omega-completeness and applying to impossible futures semantics.

Findings

Derived ground- and omega-complete axiomatizations for weak failures, traces, and completed trace semantics.

Established finite, sound, ground-complete axiomatization for concrete impossible futures preorder.

Proved non-existence of finite, sound, ground-complete axiomatizations for certain equivalences with finite alphabet.

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.