Hi Akshay, On Mon, Jun 18, 2012 at 10:10 PM, Agrawal, Akshay <akshay.agrawal@vanderbilt.edu> wrote:

if a TGBA (Transition based generalized Buchi automaton) has all transitions as accepting transitions by definition

No, all transitions are not accepting by definition of TGBA. If you got this impression while reading Spot's web pages or Spot's source code, it would help if you could tell me what gave you this impression, so that I can clarify the wording. A TGBA may have several acceptance sets of transitions. A transition may be in several acceptance set. An infinite run of a TGBA is accepted if it visits at least one transition from each acceptance set infinitely often. If course this definition implies that if no acceptance set is defined, or if all acceptance set all include all transitions, then all transitions are accepting. But these are special cases.

then what is this {ACC[r]} condition that explicitly appears ion automaton when I write LTL formula : F r.

Acc[r] is the name of an acceptance set. The transitions marked with Acc[r] are the transitions that belong to this acceptance set. On the automaton for this particular formula, this set ensures that a run that stays in state "Fr" continuously is rejected.

And why don’t I get any such thing when I use LTL formula : X r.

No acceptance set are needed to express Xr as a TGBA. That means that all infinite runs are accepting (but in this case, the automaton has only one possible run anyway). Best regards, -- Alexandre Duret-Lutz