model-checking - LTL がサポートする言語

Question

ltl p {(Xq) || (FP)}、

この LTL 式で受け入れられる正式な言語は何ですか?

例: ltl p { p && (Xq)}

{w = a0a1a2.... | p∈a0 && q∈a1}