Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

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

Authors: Peuli, A. Zuck, L.


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


    author = 	 {Peuli, A. and Zuck, L.},
    title = 	 {In and out of temporal logic},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {124--135},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}