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=eu&o=a&ff=o&mf=d&af=t&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo= 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=eu&o=a&ff=o&mf=d&af=s&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo= 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