基于启发式SCCs的广义Büchi自动机判空检测算法

Heuristic SCCs Emptiness Checking Algorithm for Generalized Büchi Automata

基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法,能较快地判断TGBA的非空性.通过正确性证明、复杂性分析和实验验证了该算法的正确可行性.在TGBA非空的情况下,该算法的时空性能比已有算法更优.

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 Btichi automata with a single accep- tance condition, whose state size is very large and the state space explosion is prone to happen. In this paper, a heuristic SCCs empti- ness checking algorithm for generalized btichi automata is proposed, which is based on the on-the-fly algorithm, and can compute ac- cepting rims of transition-based generalized Btichi automaton by heuristic depth first searching and detecting for strongly connected components. The con＇ectness and feasibility of our method have been confirmed by theoretical proofs and experimental results. Com- pared with the traditional methods, while transition-based generalized Bachi automaton is not empty, the time and memory consump- tion are reduced in our method.