Concepts of Automata Construction from LTL

We present an algorithm for the conversion of very weak alternating Büchi automata into nondeterministic Büchi automata (NBA), and we introduce a local optimization criterion for deleting superfluous transitions in these NBA. We show how to use this algorithm in the translation of LTL formulas into NBA, matching the upper bounds of other LTL-to-NBA translations. We compare the NBA resulting from our translation to the results of two popular algorithms for the translation of LTL to generalized Büchi automata: the translation of Gerth et al. of 1995 (resulting in the GPVWautomaton), and the translation of Daniele et al. of 1999 (resulting in the DGV-automaton) which improves on the GPVW algorithm. We show that the redundancy check by syntactical implication used in the construction of the DGV-automaton is covered by our local optimization, that is, all transitions removed by the redundancy check will also be removed according to our local optimization criterion. Moreover, for a fix...

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Carsten Fritz
• Keywords: Büchi Automata, Et Al, Local Optimization Criterion, LPAR 2005