电子学报2012，Vol.40Issue(1)：95-102,8.DOI:10.3969/j.issn.0372-2112.2012.01.016
基于启发式SCCs的广义Büchi自动机判空检测算法
Heuristic SCCs Emptiness Checking Algorithm for Generalized Büchi Automata
摘要
Abstract
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 biichi automata is proposed, which is based on the on-the-fly algorithm, and can compute accepting runs of transition-based generalized Biichi 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.关键词
模型检测/Büchi自动机/on-the-fly算法/判空检测Key words
model checking/ Büchi automata/ on-the-fly algorithm/ emptiness checking分类
信息技术与安全科学引用本文复制引用
王曦,徐中伟..基于启发式SCCs的广义Büchi自动机判空检测算法[J].电子学报,2012,40(1):95-102,8.基金项目
国家科技支撑计划重大项目(No.2009BAG11B00,No.2011BAG01B03) （No.2009BAG11B00,No.2011BAG01B03）
国家自然科学基金(No.60674004,No.61075002) （No.60674004,No.61075002）
