| 具有过去时态算予的计算树逻辑模型检测 |
| |
| 引用本文： | 周从华,刘志锋.具有过去时态算予的计算树逻辑模型检测[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: | |
| 本文献已被 维普 等数据库收录！ |
