Speaker

李永明 教授，陕西师范大学计算机科学学院

　　Title

基于广义可能性测度的计算树逻辑模型检测

　　Time

　　Venue

N614

　　Abstract

模型检测是一种很重要的自动化验证技术，是形式化验证的一种主要研究方向，而量化模型检测是当前模型检测技术的一种主要研究分支。本报告将主要报告新近提出的基于可能性测度的模型检测方法-基于广义可能性测度的计算树逻辑(CTL)模型检测，它是和概率模型检测互补的一种模型检测方法。我们提出了基于广义可能性测度的CTL模型检测方法：模型用广义可能性Kripke结构表示，性质用广义可能性CTL表示，证明了广义可能性CTL在表达能力方面强于经典CTL，模型检测算法采用矩阵运算，其具有多项式时间复杂性。 

　　Affiliation