Paper: In and out of temporal logic (at LICS 1993)

Authors: Amir Pnueli Lenore D. Zuck

Abstract

Two-way translations between various versions of temporal logic and between temporal logic over finite sequences and star-free regular expressions are presented. The main result is a translation from normal-form temporal logic formulas to formulas that use only future operators. The translation offers a new proof to a theorem claimed by D. Gabbay et al. (1980), stating that restricting temporal logic to the future operators does not impair its expressive power. The theorem is the basis of many temporal proof systems

BibTeX

  @InProceedings{PnueliZuck-Inandoutoftemporall,
    author = 	 {Amir Pnueli and Lenore D. Zuck},
    title = 	 {In and out of temporal logic},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {124--135},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }