On the Axiomatizability of Impossible Futures: Preorder versus Equivalence
Taolue Chen, Wan J. Fokkink · Proceedings - Symposium on Logic in Computer Science · 2008
We investigate the (in)equational theory of impossible futures semantics over the process algebra BCCSP. We prove that no finite, sound axiomatization for BCCSP modulo impossible futures equivalence is ground-complete. By contrast, we present a finite, sound, ground-complete axiomatization for BCCSP modulo impossible futures preorder. If the alphabet of actions is infinite, then this axiomatization is shown to be omega-complete. If the alphabet is finite, we prove that the in equational theory of BCCSP modulo impossible futures preorder lacks such a finite basis. We also derive non-finite axiomatizability results for nested impossible futures semantics.