|
吉林大学学报(工学版) 2007
基于LTLTableau的自动机构造, PP. 132-135 Keywords: 计算机软件,模型检验,LTLTableau,Co-Büchi自动机,计算机软件,模型检验,LTLTableau,Co-Büchi自动机 Abstract: 基于线性时序逻辑(LTL)的模型检验是使用较为广泛的技术。该种模型检验最终归结为有穷自动机的判空问题,其复杂性来源于性质和模型乘积自动机的状态空间膨胀。作者提出了一种构造迟滞交换Co-Büchi自动机(StufferAlternatingCoBüchi)的具有线性复杂度的方法,该方法能够降低最终乘积自动机的空间复杂度。
|