This graph represents a chronology of algorithms for translating LTL to Büchi automata. Three kinds of automata are distinguished:
Legend |
Büchi automata with labeled and accepting states |
Büchi automata with labeled transitions and accepting states |
Büchi automata with labeled and accepting transitions (see TGBA) |
All of them are as expressive as the other. It's easy to show that pink automata (i.e. TGBA) are more compact than blue automata which in turn are more compact that yellow automata. Some of the translation algorithms colored in pink actually use TGBA only as an intermediate step; it doesn't matter (since Spot handles TGBA we are interested by algorithms that produces TGBA at any moment).