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?


2 Answers 2


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.

  • $\begingroup$ Thanks, exactly what I was looking for! Though I'm not losing hope that even more answers are to come :) $\endgroup$
    – jkff
    Apr 14, 2011 at 8:54

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.