Efficient Translation from Transition-Based Generalized Büchi Automata to Büchi Automata
从基于迁移的扩展Büchi自动机到Büchi自动机

The automata-theoretic approach is one of the state-of-the-art model-checking methods, which consists of the following steps: use a Büchi automaton to represent the abstract system model; use an LTL formula to express the properties to be verified; translate the negation of the LTL formula to a Büchi automaton and check whether the intersection of sentences accepted by the two automata is non-empty. One type of methods for translating LTL formulas to Büchi automata has one step for calculating transition-based generalized Büchi automata (TGBA) and another step for translating TGBA to Büchi automata. This paper redefines the product operation of TGBA according to the characteristics of the accepting language of Büchi automata. This leads to the reduction of the number of states that need to be copied and therefore smaller Büchi automata. The experimental results given at the end of this paper demonstrate the advantage of the approach based on test cases with randomly generated formulas.