1
$\begingroup$

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!!

$\endgroup$
2
  • 1
    $\begingroup$ The acceptance condition for generalized Büchi automata is that for every set of states $S\in F$, there exists a state $s\in S$ that occurs infinitely often in the run. If $F$ is empty, this condition is vacuously true, hence the automaton accepts every $\omega$-word for which there exists an infinite run (note that the automaton is nondeterministic and $\Delta(q,s)$ may well be empty, hence it may happen that there is no run). $\endgroup$ Aug 3, 2014 at 17:13
  • $\begingroup$ thank you very much for your fast answer _ my last question: should the first position of an infinite word accept ϕ? and that's why "pqppppppp..." isn't an accepted word for my automata A for the formula ϕ= Xp? $\endgroup$
    – sansun
    Aug 3, 2014 at 19:23

0

Browse other questions tagged or ask your own question.