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

Question

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?

Answer 1

One construction not listed on the SPOT website is given in a survey by Demri & 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 & Schuller, Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata, SIAM Journal on Computing 34: 1159--1175, 2005.

Answer 2

I would consider the translation that goes through an alternating automata. (See Vardi's paper "Alternating Automata and program verification"). It's a very elegant translation from LTL to alternating automata and then you can use Mihano Ayashi (which is also elegant - it's a double subset construction) to reach a non deterministic Buchi automata.