模型检验中对CTL公式的空属性探测

在模型检验中建立了一种新方法：检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性．根据原子命题的极性，用TRUE 或FALSE替换原子命题，得到一系列的CTL公式，再对这些CTL公式用模型检验工具验证，若CTL公式中有一个通过了验证，则可得出该系统属性是一个空属性．该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE 或FALSE替换，只需对原子命题替换，这样检验的次数与原子命题的个数呈线性关系．利用验证综合系统对十字路口交通控制器规范的空属性进行了检验．

Vacuity detection in computation temperal logic

In model checking a new method is proposed on checking whether a system property represented by a computation temperal logic(CTL) formula is vacuity.From the polarity of atomic proposition,a series of CTL formulae is derived by substituting the atomic proposition with TRUE or FALSE,before they are verified by model checking tools.If one of the CTL formulae has passed the verification,then it is concluded that the system property is a vacuity.In this solution,to check the vacuity of the CTL formula,it is not necessary to substitute all of its sub-formulae by TRUE or FALSE,but instead,it is enough to substitute its atomic proposition,and thus the number of times for checking is linear with the number of atomic propositions.With a VIS system,effectiveness of this solution is further verified by checking the vacuity of specification on the cross-road traffic controller.