TGBA stands for for Transitionbased Generalized Büchi Automaton.
It's an OmegaAutomaton where Büchi acceptance conditions are defined in terms of transitions instead of states. Also it uses generalized acceptance conditions, meaning there are several sets of transitions. A path in the automaton is accepted if it passes infinitely often by one transition of each acceptance set.
The acronym TGBA was coined by Dimitra Giannakopoulou and Flavio Lerda [#giannakopoulou.02.forte]. However TGBAs were used before that by JeanMichel Couvreur [#couvreur.99.fm].
Serge Haddad and François Vernadat [#haddad.03.vps] complement each set of the acceptance condition to define promise automata. (The use of promises to translate LTL formulae was illustrated by Alexandre DuretLutz and Denis Poitrenaud [#duret.04.mascots].) Max Michel also described a comparable structure earlier [#michel.84.stacs].
 [duret.04.mascots]

Alexandre DuretLutz and Denis Poitrenaud.
Spot: an extensible model checking library using transitionbased
generalized Büchi automata.
In Proceedings of the 12th IEEE/ACM International Symposium on
Modeling, Analysis, and Simulation of Computer and Telecommunication Systems
(MASCOTS'04), pages 7683, Volendam, The Netherlands, October 2004. IEEE
Computer Society Press.
[ .pdf ]  [couvreur.99.fm]

JeanMichel Couvreur.
Onthefly verification of temporal logic.
In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors,
Proceedings of the World Congress on Formal Methods in the Development of
Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253271, Toulouse, France, September 1999. ©SpringerVerlag.
[ .pdf ]  [giannakopoulou.02.forte]

Dimitra Giannakopoulou and Flavio Lerda.
From states to transitions: Improving translation of LTL formulae
to Büchi automata.
In D.A. Peled and M.Y. Vardi, editors, Proceedings of the 22nd
IFIP WG 6.1 International Conference on Formal Techniques for Networked and
Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 308326, Houston, Texas, November 2002.
©SpringerVerlag.
[ .pdf ]  [haddad.03.vps]

Serge Haddad and François Vernadat.
Vérification de propriétés spécifiques.
In Michel Diaz, editor, Vérification et mise en oeuvre
des réseaux de Petri, Traité IC2, série Informatique et
systèmes d'information, chapter 1. Hermes Science, January 2003.
 [michel.84.stacs]

Max Michel.
Algèbre de machines et logique temporelle.
In Max Fontet and Kurt Mehlhorn, editors, Proceedings of the
Symposium on Theoretical Aspects of Computer Science (STACS'84), volume 166
of Lecture Notes in Computer Science, pages 287298, Paris, April
1984. ©SpringerVerlag.