Title :
In and out of temporal logic
Author :
Peuli, A. ; Zuck, Lenore
Author_Institution :
Dept. of Comput. Sci., Weizmann Inst. of Sci., Rehovot, Israel
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
Keywords :
formal languages; temporal logic; theorem proving; finite sequences; future operators; logic translation; normal-form temporal logic formulas; restricting temporal logic; star-free regular expressions; temporal logic; temporal proof systems; theorem proof; two-way translations; Automata; Computer science; Logic; Protection;
Conference_Titel :
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-8186-3140-6
DOI :
10.1109/LICS.1993.287594
