论文部分内容阅读
针对 Specification Pattern System（SPS）和 Property Specification（Prospec）不能将组合命题形式化为模型检测器可以接受的 Computation tree logic（CTL）公式问题，通过深入研究 SPS 和 Prospec 产生系统性质描述的形式化方法，并对比 CTL 与 Future interval logic（FIL）的表达能力以及 CTL 与 Linear temporallogic（LTL）两者之间的关系，构造了一类具有较强描述能力