模型检测中的CTL形式化描述模板

针对SPS（specificationpatternsystem）和Prospec（propertyspecification）不能将组合命题形式化为模型检测器可以接受的CTL（computationtreelogic）公式问题，通过研究SPS和Prospec产生系统性质描述的形式化方法，并对比CTL与FIL（futureintervallogic）的表达能力以及CTL与LTL（lineartemporallogic）两者之间的关系，构造了一类具有较强描述能力的CTL公式模板，并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的CTL公式可以直接应用到模型检测器中，利于系统性质验证.