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 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.
Additional Metadata
Keywords Concurrency, Process Algebra
ACM Concurrent Programming (acm D.1.3), Models of Computation (acm F.1.1), Modes of Computation (acm F.1.2)
MSC Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Abstract data types; algebraic specification (msc 68Q65), Algebraic theory of languages and automata (msc 68Q70)
THEME Software (theme 1)
Publisher CWI
Series Software Engineering [SEN]
Chen, T, & Fokkink, W.J. (2008). On the axiomatizability of impossible futures: preorder versus equivalence. Software Engineering [SEN]. CWI.