Paper: Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes (at LICS 1993)

Authors: Søren Christensen Yoram Hirshfeld Faron Moller

Abstract

The authors prove the decidability of two subclasses of recursive processes involving a parallel composition operator with respect to bisimulation equivalence, namely, the so-called normed and live processes. To accomplish this, the authors first prove a unique decomposition result for (a generalization of) normed processes, in order to deduce a necessary cancellation law. The decidability proof leads to a complete axiomatization for these process classes

BibTeX

  @InProceedings{ChristensenHirshfel-Decomposabilitydeci,
    author = 	 {Søren Christensen and Yoram Hirshfeld and Faron Moller},
    title = 	 {Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes },
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {386--396},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }