Paper: On the Axiomatizability of Impossible Futures: Preorder versus Equivalence (at LICS 2008)

Authors: Taolue Chen Wan Fokkink

Abstract

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.

BibTeX

  @InProceedings{ChenFokkink-OntheAxiomatizabili,
    author = 	 {Taolue Chen and Wan Fokkink},
    title = 	 {On the Axiomatizability of Impossible Futures: Preorder versus Equivalence},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {156--165},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }