On the expressive power of QLTL

Abstract

LTL cannot express the whole class of w-regular languages and several extensions have been proposed. Among them, Quantified propositional Linear Temporal Logic (QLTL), proposed by Sistla, extends LTL by quantifications over the atomic propositions. The expressive power of LTL and its fragments have been made relatively clear by numerous researchers. However, there are few results on the expressive power of QLTL and its fragments (besides those of LTL). In this paper we get some initial results on the expressive power of QLTL. First, we show that both Q(U) (the fragment of QLTL in which "Until" is the only temporal operator used, without restriction on the use of quantifiers) and Q(F) (similar to Q(U), with temporal operator "Until" replaced by "Future") can express the whole class of ω-regular languages. Then we compare the expressive power of various fragments of QLTL in detail and get a panorama of the expressive power of fragments of QLTL. Finally, we consider the quantifier hierarchy of Q(U) and Q(F), and show that one alternation of existential and universal quantifiers is necessary and sufficient to express the whole class of ω-regular languages. © Springer-Verlag Berlin Heidelberg 2007.