文件名称：模型检测中的CTL形式化描述模板 (2013年)
文件大小：488KB
文件格式：PDF
更新时间：2024-07-03 14:45:14
工程技术 论文
针对SPS(specificationpatternsystem)和Prospe(cpropertyspecification)不能将组合命题形式化为模型检测器可以接受的CTL(computationtreelogic)公式问题,通过研究SPS和Prospec产生系统性质描述的形式化方法,并对比CTL与F1L(futureintervallogic)的表达能力以及CTL与LTL(lineartemporallogic)两者之间的关系,构造了一类具有较强描述能力的CTL公式模板,并通过重新定义合取逻辑运算符