19 Jun
2012
19 Jun
'12
8:47 a.m.
Hi Akshay,
On Mon, Jun 18, 2012 at 10:10 PM, Agrawal, Akshay
<akshay.agrawal(a)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