The key operation of the automata-theoretic approach for model-checking is an emptiness checking algorithm

which can tell whether a finite state system satisfies its properties.It is usually done on standard Büchi automata with a single acceptance condition

whose state size is very large and the state space explosion is prone to happen.In this paper

a heuristic SCCs emptiness checking algorithm for generalized büchi automata is proposed

which is based on the on-the-fly algorithm

and can compute accepting runs of transition-based generalized Büchi automaton by heuristic depth first searching and detecting for strongly connected components.The correctness and feasibility of our method have been confirmed by theoretical proofs and experimental results.Compared with the traditional methods

while transition-based generalized Büchi automaton is not empty

the time and memory consumption are reduced in our method.