Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
On the Expressive Power of QLTL
verfasst von : Zhilin Wu
Erschienen in: Theoretical Aspects of Computing – ICTAC 2007
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
LTL
cannot express the whole class of
ω
-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.