Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: Explicit clock temporal logic (at LICS 1990)

Authors: Harel, E. Lichtenstein, O. Pnueli, A.

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 = 	 {Harel, E. and Lichtenstein, O. and Pnueli, A.},
    title = 	 {Explicit clock temporal logic},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {402--413},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }