广义可能性计算树逻辑的不动点语义  

Fixed-point semantics of computation tree logic based on generalized possibility measures

作　　者：邓楠轶 张兴兴[1] 李永明[1] 

机构地区：[1]陕西师范大学计算机科学学院,陕西西安710119

出　　处：《陕西师范大学学报（自然科学版）》2015年第4期22-27,共6页Journal of Shaanxi Normal University：Natural Science Edition

基　　金：国家自然科学基金(11271237;61228305);高等学校博士学科点专项基金(20130202120001)

摘　　要：计算树逻辑的不动点语义在其对应的符号模型检测方法中具有重要意义。给出广义可能性计算树逻辑的不动点语义解释,并利用归纳法证明此不动点为最大或最小不动点。结论表明,广义可能性计算树逻辑的不动点语义具有不同于经典情形的形式。Fixed-point semantics of computation tree logic plays an important role in symbolic model checking. Fixed-point semantics of generalized possibilistic computation tree logic is presen- ted, then the greatest or least fixed-point is shown by the method of mathematical induction, which is different from the form in classical model checking.

关 键 词：广义可能性测度 计算树逻辑 不动点语义 模型检测 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]