What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?
One construction not listed on the SPOT website is given in a survey by Demri &amp; Gastin, Specification and Verification using Temporal Logics, 2009.  The construction is simple and yields reasonably small automata, so it can be carried out by hand for small formulæ, which is good for teaching (which is how I use it), but might also be helpful for debugging an implementation.  I wouldn't bet on it being more efficient than the one used by SPOT though.

About minimization, there is no canonical minimal Büchi automaton for a given $\omega$-regular language.  In order to get smaller automata, one can quotient the automaton by some simulation relation.  A classical paper on the subject is by Etessami, Wilke &amp; Schuller, Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata, SIAM Journal on Computing 34: 1159--1175, 2005.