Optimization of Büchi automata by language equivalence relationships
Puhan Zhang · Journal of Tsinghua University(Science and Technology) · 2009
The rapid increase in the number of states during model checking and the number of states and transitions for Buchi automata is reduced by defining a language equivalence class based on the language equivalence relationships of Buchi automata with an efficient algorithm to reduce the automata states and transitions.The algorithm takes into account the reachability of states in the language equivalence class and uses simulation relationships to compute the language equivalence class.The language equivalence class is combined with an automata quotient to delete more Buchi automata states and transitions during polynomial growth time.An analysis of a typical example and a correctness proof show that the algorithm gives better optimization than existing algorithms.