On Sat, Mar 17, 2012 at 6:43 AM, Jianwen Li <lijwen2748(a)gmail.com> wrote: 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