Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski