Paper: In and out of temporal logic (at LICS 1993)
Authors: Peuli, A. Zuck, L.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{PeuliZuck-Inandoutoftemporall,
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}
}