Paper: Explicit clock temporal logic (at LICS 1990)

Authors: Eyal Harel Orna Lichtenstein Amir Pnueli

Abstract

The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic)

BibTeX

  @InProceedings{HarelLichtensteinPn-Explicitclocktempor,
    author = 	 {Eyal Harel and Orna Lichtenstein and Amir Pnueli},
    title = 	 {Explicit clock temporal logic},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {402--413},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }