Provable State-Space Minimization of Büchi Automata arising from LTL Specifications
Peter Wita
The transformation of a Linear-time Temporal Logic (LTL) formula to a Büchi automaton is a widely used reduction and builds a crucial path in the verification against or the synthesis of a given specification. To deal with the exponential blowup in the state-space of the resulting automata, recent research already focused on reducing the number of states by creating and applying different constructions. Although some of them focus on a previous pushing in or pushing out of LTL operators, most of them lack in execution and argumentation of the effectiveness of such a simplification. In this thesis, we consider the constructions from an LTL formula to a Büchi Automaton by Gastin and Oddoux and by Gerth et al., also called Tableau Construction. Subsequent we will examine both constructions in terms of the most familar equivalences over LTL and prove the discovered simplifications in the field of the resulting state space with the help of decent prove systems. At the end we present for each mentioned construction a set of provable theorems over their LTL input, guaranteeing a state space minimization by applying them on the given formula before using the related construction.
Bachelor Thesis.