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