On Sat, Mar 17, 2012 at 6:43 AM, Jianwen Li lijwen2748@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,