<p>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. </p>

CC BY-SA 3.0
2011-05-07T21:26:10.670Z
2011-05-07T21:26:10.670Z
Guy
<p>One construction not listed on the <a href="http://spot.lip6.fr/wiki/LtlTranslationAlgorithms" rel="noreferrer">SPOT</a> website is given in a survey by Demri &amp; Gastin, <em><a href="http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-iis09.pdf" rel="noreferrer">Specification and Verification using Temporal Logics</a></em>, 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.</p>

<p>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, <em><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.62.8014&amp;rep=rep1&amp;type=pdf" rel="noreferrer">Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata</a></em>, SIAM Journal on Computing 34: 1159--1175, 2005.</p>

CC BY-SA 3.0
2011-04-14T08:54:32.453Z
Thanks, exactly what I was looking for! Though I'm not losing hope that even more answers are to come :)
jkff
CC BY-SA 3.0
2011-04-14T08:15:37.077Z
2011-04-14T08:15:37.077Z
Sylvain
<p>I'm writing a <a href="http://github.com/jkff/minxmod" rel="nofollow">toy modelchecker</a>, and I'm at the point where it's time to implement LTL to Buchi automata translation.</p>

<p>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.</p>

<p>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 :)</p>

<p>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 :)</p>

<p>...Or perhaps there are interesting alternative approaches to LTL verification?</p>

<p>For reference, here's a genealogy of LTL-to-Buchi translation algorithms <a href="http://spot.lip6.fr/wiki/LtlTranslationAlgorithms" rel="nofollow">http://spot.lip6.fr/wiki/LtlTranslationAlgorithms</a> . Can anyone say something about these?</p>

<lo.logic><automata-theory><model-checking><program-verification><linear-temporal-logic>
What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?
jkff
# What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

(Asked by: username_0 on 2011-04-14)

I'm writing a [toy modelchecker](http://github.com/jkff/minxmod), 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?

**Tags:** lo.logic, automata-theory, model-checking, program-verification, linear-temporal-logic

---

## 2 answers

### Answer by username_2 on 2011-04-14. Score: 9 | Accepted answer

One construction not listed on the [SPOT](http://spot.lip6.fr/wiki/LtlTranslationAlgorithms) website is given in a survey by Demri & Gastin, *[Specification and Verification using Temporal Logics](http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-iis09.pdf)*, 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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.62.8014&rep=rep1&type=pdf)*, SIAM Journal on Computing 34: 1159--1175, 2005.

> **Comments:**
> **username_0**: Thanks, exactly what I was looking for! Though I'm not losing hope that even more answers are to come :)  

---

### Answer by username_1 on 2011-05-07. Score: 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.


---

