搜索结果: 1-3 共查到“工学 CTL”相关记录3条 . 查询时间(0.057 秒)
模型检验中对CTL公式的空属性探测
空属性探测 可计算时态逻辑公式 验证综合系统系统
2009/5/27
在模型检验中建立了一种新方法：检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性．根据原子命题的极性，用TRUE 或FALSE替换原子命题，得到一系列的CTL公式，再对这些CTL公式用模型检验工具验证，若CTL公式中有一个通过了验证，则可得出该系统属性是一个空属性．该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE 或FALSE替换，只需对原子命题替换，这样检验的次数与原子命...
模型检验中对CTL公式的空属性探测
模型检验 空属性探测 可计算时态逻辑公式
2009/1/22
在模型检验中建立了一种新方法：检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性．根据原子命题的极性，用TRUE 或FALSE替换原子命题，得到一系列的CTL公式，再对这些CTL公式用模型检验工具验证，若CTL公式中有一个通过了验证，则可得出该系统属性是一个空属性．该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE 或FALSE替换，只需对原子命题替换，这样检验的次数与原子命...
符号化模型检测CTL*
模型检测 时态逻辑 有序二值判定图(OBDD)
2007/11/1
提出了一个关于时态逻辑CTL*的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL*规范.根据该理论,作者已实现了一个基于OBDD技术的CTL*符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等,都只能对CTL*的子集逻辑(如CTL,LTL)进行检测，而文中算法的结果是令人满意的,并且当规...