Язык, поддерживаемый LTL

Question

ltl p {(Xq) || (Fp)},

Какой будет официальный язык этой формулы LTL?

Например: Лт р {р & & (Хд)}

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

Answer 1

Свойство X q || F p принимает слова языка

{ w = w0w1w2... | q ∈ w1 or ∃wi. p ∈ wi } 

Другой способ взглянуть на принятый язык является нарисовать Buchi Automaton, соответствующий формуле LTLX q || F p:

Кредиты: изображения, сгенерированные с ltl2ba