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

Authors: Rocco De Nicola Fritz W. Vaandrager

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 = 	 {Rocco De Nicola and Fritz W. Vaandrager},
    title = 	 {Three logics for branching bisimulation},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {118--129},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }