2008 23rd Annual IEEE Symposium on Logic in Computer Science
On the Axiomatizability of Impossible Futures: Preorder versus Equivalence
June 24-June 27
ISBN: 978-0-7695-3183-0
We investigate the (in)equational theory of impossible futures semantics over the process algebra BCCSP. We provethat 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 /piv-complete. If the alphabet is finite, we prove that the inequational theory of BCCSP modulo impossible futures preorder lacks such a finite basis. We also derive non-finite axiomatizability results for nested impossible futures semantics.