17 Mar
2012
17 Mar
'12
8:52 a.m.
On Sat, Mar 17, 2012 at 6:43 AM, Jianwen Li <lijwen2748(a)gmail.com> wrote:
When I use the SPOT tool online recently I found
the truth that the
result Buchi automata for such formulas G(F a && F b) from your tool is not
a traditional one. Can you explain why? Thank you very much!
Hi Jianwen,
You can use the online translator to produce two kinds of Büchi automata :
1) Generalized Büchi Automata with transition-based acceptance (the default)
http://spot.lip6.fr/ltl2tgba.html#f=G(Fa+%26%26+Fb)&r=br&r=si&r…
2) "degeneralized" Büchi Automata with state-based acceptance
(probably what you are looking for)
http://spot.lip6.fr/ltl2tgba.html#f=G(Fa+%26%26+Fb)&r=br&r=si&r…
As you can see in this very example, transition-based generalized
Büchi automata (TGBA) are much more compact than the state-based Büchi
automata used traditionally. In practice, it is more efficient to
build a model checker using TGBA than using BA: this is why Spot
produces TGBA by default. If you want a traditional Büchi automaton,
all you need is to click on "state-based degeneralized Büchi
automaton" in the "Desired Output / Büchi" panel.
Best regards,
--
Alexandre Duret-Lutz