%0 Journal Article
%T 基于LTLTableau的自动机构造
%A 刘万伟
%A 王戟
%A 陈火旺
%J 吉林大学学报(工学版)
%P 132-135
%D 2007
%X 基于线性时序逻辑（LTL）的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题，其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机（StufferAlternatingCoBüchi）的具有线性复杂度的方法，该方法能够降低最终乘积自动机的空间复杂度。
%K 计算机软件
%K 模型检验
%K LTLTableau
%K Co-Büchi自动机
%K 计算机软件
%K 模型检验
%K LTLTableau
%K Co-Büchi自动机
%U http://xuebao.jlu.edu.cn/gxb/CN/Y2007/V37/I01/132