# What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation.

For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want the code to remain extremely clear and concise for as long as possible.

I've looked at the "local automata + eventuality automata" approach, described in multiple tutorials, but it seems to be neither simple to implement/understand (the correctness proof is quite large), nor does it yield small automata. So I'm not implementing it until I'm sure I won't regret it :)

So, I'd be grateful for references to papers describing simple and efficient algorithms for this translation, or perhaps simple and inefficient ones - then papers on minimization of Buchi automata would be welcome too :)

...Or perhaps there are interesting alternative approaches to LTL verification?

For reference, here's a genealogy of LTL-to-Buchi translation algorithms http://spot.lip6.fr/wiki/LtlTranslationAlgorithms . Can anyone say something about these?

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 & Schuller, Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata, SIAM Journal on Computing 34: 1159--1175, 2005.