首页 | 本学科首页   官方微博 | 高级检索  
     

具有过去时态算予的计算树逻辑模型检测
引用本文:周从华 刘志锋. 具有过去时态算予的计算树逻辑模型检测[J]. 计算机工程, 2007, 33(22): 98-100
作者姓名:周从华 刘志锋
作者单位:江苏大学计算机科学与通信工程学院,镇江212013
基金项目:国家自然科学基金资助项目(60573046)
摘    要:在计算树逻辑(CTL)中引入过去时态算子,得到了表达力更强的属性规约语言CTLP,给出了CTLP的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现,从而有效克服了模型检测中的状态爆炸问题。

关 键 词:计算树逻辑 模型检测 二叉判定图
文章编号:1000-3428(2007)22-0098-03
修稿时间:2006-12-31

Model Checking of Computation Tree Logic with Past Temporal Operators
ZHOU Cong-hua, LIU Zhi-feng. Model Checking of Computation Tree Logic with Past Temporal Operators[J]. Computer Engineering, 2007, 33(22): 98-100
Authors:ZHOU Cong-hua   LIU Zhi-feng
Affiliation:School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013
Abstract:
Keywords:
本文献已被 维普 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号