Optimizations for LTL synthesis

B Jobstmann, R Bloem - 2006 Formal Methods in Computer …, 2006 - ieeexplore.ieee.org
2006 Formal Methods in Computer Aided Design, 2006ieeexplore.ieee.org
We present an approach to automatic synthesis of specifications given in linear time logic.
The approach is based on a translation through universal co-Buchi tree automata and
alternating weak tree automata (O. Kupferman and M. Vardi, 2005). By careful optimization
of all intermediate automata, we achieve a major improvement in performance. We present
several optimization techniques for alternating tree automata, including a game-based
approximation to language emptiness and a simulation-based optimization. Furthermore, we …
We present an approach to automatic synthesis of specifications given in linear time logic. The approach is based on a translation through universal co-Buchi tree automata and alternating weak tree automata (O. Kupferman and M. Vardi, 2005). By careful optimization of all intermediate automata, we achieve a major improvement in performance. We present several optimization techniques for alternating tree automata, including a game-based approximation to language emptiness and a simulation-based optimization. Furthermore, we use an incremental algorithm to compute the emptiness of nondeterministic Buchi tree automata. All our optimizations are computed in time polynomial in the size of the automaton on which they are computed. We have applied our implementation to several examples and show a significant improvement over the straightforward implementation. Although our examples are still small, this work constitutes the first implementation of a synthesis algorithm for full LTL. We believe that the optimizations discussed here form an important step towards making LTL synthesis practical
ieeexplore.ieee.org