I need some help in Generalized Büchi automaton .. I do understand the translation of a LTL-formula ϕ into Generalized Büchi automaton A= (Q, Δ, I, F), with F= {F1,...,Fn}
My problem is F .. I know that for every until-formula (a_i U b_i) there exist F-i that contains states with b_i or states with "not (a_i U b_i)"
if there no exists an until-subformula in ϕ? then F is empty !!
But how do i know if a word is accepted or not ??
For example the LTL-Formula ϕ= Xp with an atomic proposition p. the generalized Büchi automaton A ist then: Q= {q1, q2, q3, q4}
q1= {Xp, p};
q2= {not Xp, p};
q3= {XP, not p};
q4= {not Xp, not p};
Δ(q1, p)= { q1, q2 };
Δ(q2, p)= { q3, q4 };
Δ(q3, not p)= { q1, q2 };
Δ(q4, not p)= { q3, q4 };
I= {q1, q3};
F= {};
how do i know if a word is accepted from A or not ?? isn't a word like pppppppppp.... an accepted word ? where i can see that ? and why isn't pqppppppp...an accepted run?
thanks!!