论文部分内容阅读
为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENusMV该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够