Computer Science – Formal Languages and Automata Theory
Scientific paper
2012-01-03
Computer Science
Formal Languages and Automata Theory
Full version of the paper presented at TACAS 2012
Scientific paper
We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into B\"uchi automata via very weak alternating co-B\"uchi automata and generalized B\"uchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator 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 modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially.
Babiak Tomáš
Křetínský Mojmír
Řehák Vojtěch
Strejček Jan
No associations
LandOfFree
LTL to Büchi Automata Translation: Fast and More Deterministic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with LTL to Büchi Automata Translation: Fast and More Deterministic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and LTL to Büchi Automata Translation: Fast and More Deterministic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-184161