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?