Warning: This page has not been updated from 2006. Many new LTL translation algorithms have been published since.
1. A Genealogy of LTLtoBüchi Translators
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).
2. References
(When adding new entries to this page, please complete the HlinsDatabase with the author homepages and other things that must be turned into hyperlinks.)
 [barringer.89.avmfss]

Howard Barringer, Michael D. Fisher, and Graham D. Gough.
Fair SMG and linear time model checking.
In Proceedings of the International Workshop on Automatic
Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 133150. ©SpringerVerlag, 1989.
 [beth.59.fom]

Evert Willem Beth.
The Foundations of Mathematics.
North Holland, 1959.
Second edition revised in 1965.
 [burch.91.slcd]

Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L.J.
Hwang.
Symbolic model checking: 10^{20} states and beyond.
In Proceedings of the Fifth Annual IEEE Symposium on Logic in
Computer Science, pages 133, Washington, D.C., 1990. IEEE Computer Society
Press.
 [couvreur.00.lacim]

JeanMichel Couvreur.
Un point de vue symbolique sur la logique temporelle linéaire.
In Pierre Leroux, editor, Actes du Colloque LaCIM 2000,
volume 27 of Publications du LaCIM, pages 131140. Université du
Québec à Montréal, August 2000.
[ .pdf ]  [couvreur.99.fm]

JeanMichel Couvreur.
Onthefly verification of linear 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 ]  [daniele.99.cav]

Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi.
Improved automata generation for Linear Temporal Logic.
In N. Halbwachs and Doron A. Peled, editors, Proceedings of the
11th International Conference on Computer Aided Verification (CAV'99),
volume 1633 of Lecture Notes in Computer Science, pages 249260.
©SpringerVerlag, 1999.
 [etessami.00.concur]

Kousha Etessami and Gerard J. Holzmann.
Optimizing Büchi automata.
In C. Palamidessi, editor, Proceedings of the 11th International
Conference on Concurrency Theory (Concur'2000), volume 1877 of Lecture Notes in Computer Science, pages 153167. ©SpringerVerlag, 2000.
 [etessami.01.alp]

Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller.
Fair simulation relations, parity games, and state space reduction
for buchi automata.
In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors,
Proceedings of the 28th international colloquium on Automata, Languages
and Programming, volume 2076 of Lecture Notes in Computer Science,
pages 694707, Crete, Greece, July 2001. ©SpringerVerlag.
 [fritz.03.ciaa]

Carsten Fritz.
Constructing Büchi automata from linear temporal logic using
simulation relations for alternating Büchi automata.
In Oscar H. Ibarra and Zhe Dang, editors, Proceedings of the 8th
International Conference on Implementation and Application of Automata
(CIAA'03), volume 2759 of Lecture Notes in Computer Science, pages
3548, Santa Barbara, California, July 2003. ©SpringerVerlag.
 [gastin.01.cav]

Paul Gastin and Denis Oddoux.
Fast LTL to Büchi automata translation.
In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of
the 13th International Conference on Computer Aided Verification (CAV'01),
volume 2102 of Lecture Notes in Computer Science, pages 5365.
©SpringerVerlag, 2001.
 [gerth.95.pstv]

Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper.
Simple onthefly automatic verification of linear temporal logic.
In Proceedings of the 15th Workshop on Protocol Specification
Testing and Verification (PSTV'95), pages 318, Warsaw, Poland, 1996.
Chapman & Hall.
[ .html ]  [giannakopoulou.02.forte]

Dimitra Giannakopoulou and Flavio Lerda.
From states to transitions: Improving translation of LTL formulae
to Büchi automata.
In Doron A. Peled and Moshe 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 ]  [kesten.93.cav]

Yonit Kesten, Zohar Manna, Hugh McGuire, and Amir Pnueli.
A decision algorithm for full propositional temporal logic.
In C. Courcoubetis, editor, Proceedings for the 5th Conference
on Computer Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 97109. ©SpringerVerlag, 1993.
 [lichtenstein.85.popl]

Orna Lichtenstein and Amir Pnueli.
Checking that finite state cocurrent programs satisfy they linear
specification.
In Proceedings of the 12th ACM Symposium on Principles of
Programming Languages (POPL'85), pages 97107. ACM, 1985.
 [miyano.84.tcs]

Satoru Miyano and Takeshi Hayashi.
Alternating finite automata on ωwords.
Theoretical Computer Science, 32:321330, 1984.
 [sebastiani.03.charme]

Roberto Sebastiani and Stefano Tonetta.
more deterministic vs. smaller Büchi automata for efficient
ltl model checking.
In G. Goos, J. Hartmanis, and J. van Leeuwen, editors,
Proceedings for the 12th Advanced Research Working Conference on Correct
Hardware Design and Verification Methods (CHARME'03), volume 2860 of
Lecture Notes in Computer Science, pages 126140. ©SpringerVerlag, October
2003.
[ .ps ]  [smullyan.68.fol]

Raymon M. Smullyan.
FirstOrder Logic.
©SpringerVerlag, 1968.
 [somenzi.00.cav]

Fabio Somenzi and Roderick Bloem.
Efficient Büchi automata for LTL formulae.
In Proceedings of the 12th International Conference on Computer
Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 247263. ©SpringerVerlag, 2000.
 [tauriainen.03.a83]

Heikki Tauriainen.
On translating linear temporal logic into alternating and
nondeterministic automata.
Research Report A83, Helsinki University of Technology, Laboratory
for Theoretical Computer Science, Espoo, Finland, December 2003.
 [tauriainen.06.phd]

Heikki Tauriainen.
Automata and Linear Temporal Logic: Translation with
Transitionbased Acceptance.
PhD thesis, Helsinki University of Technology, Espoo, Finland,
September 2006.
 [thirioux.02.fmics]

Xavier Thirioux.
Simple and efficient translation from LTL formulas to Büchi
automata.
In Rance Cleaveland and Hubert Garavel, editors, Proceedings of
the 7th International ERCIM Workshop in Formal Methods for Industrial
Critical Systems (FMICS'02), volume 66(2) of Electronic Notes in
Theoretical Computer Science, Málaga, Spain, July 2002. Elsevier.
 [vardi.94.ic]

Moshe Y. Vardi and Pierre Wolper.
Reasoning about infinite computations.
Information and Computation, 115(1):137, Nov 1994.
 [wolper.83.focs]

Pierre Wolper, Moshe Y. Vardi, and Aravinda Prasad Sistla.
Reasoning about infinite computation paths.
In Proceedings of the 24th IEEE Symposium on Foundations of
Computer Science (FOCS'83), pages 185194. IEEE Computer Society Press,
1983.
Later extended and published as [vardi.94.ic].
 [wolper.83.ic]

Pierre Wolper.
Temporal logic can be more expressive.
Information and Control, 56(12):7299, 1983.
 [wolper.85.la]

Pierre Wolper.
The tableau method for temporal logic: An overview.
Logique et Analyse, (110111):119136, 1985.
3. See also
You might also be interested in a similar genealogy of EmptinessCheckAlgorithms.