Logic in Computer Science (LICS 1990)

Paper: Three logics for branching bisimulation (at LICS 1990)

Authors: De Nicola, R. Vaandrager, F.

Abstract

Three temporal logics are introduced which induce on labeled transition systems the same identifications as branching bisimulation. The first is an extension of Hennessy-Milner logic with a kind of unit operator. The second is another extension of Hennessy-Milner logic which exploits the power of backward modalities. The third is CTL* with the next-time operator interpreted over all paths, not just over maximal ones. A relevant side effect of the last characterization is that it sets a bridge between the state- and event-based approaches to the semantics of concurrent systems

BibTeX

  @InProceedings{DeNicolaVaandrager-Threelogicsforbranc,
    author = 	 {De Nicola, R. and Vaandrager, F.},
    title = 	 {Three logics for branching bisimulation},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {118--129},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }