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
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.13
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.
Citation:
Taolue Chen, Wan Fokkink, "On the Axiomatizability of Impossible Futures: Preorder versus Equivalence," lics, pp.156-165, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||