LTL to Buchi Automata Translation: Fast and More Deterministic ?
Tom · arXiv (Cornell University) · 2012
We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Buchi automata via very weak alternating co-Buchi automata and generalized Buchi automata. Sev- eral improvements are based on specic properties of any formula where each branch of its syntax tree contains at least one eventually opera- tor and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modied all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modications are real im- provements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially. This is a full version of (1) published at TACAS 2012.