loading...
On the Axiomatizability of Impossible Futures: Preorder versus Equivalence
June 24-June 27
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.132008 23rd Annual IEEE Symposium on Lo ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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.