| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 基于完备抽象解释的模型检验CTL公式研究 |
| 作者 | 钱俊彦1) 徐宝文2),3) |
| 作者单位 | 1)(桂林电子科技大学计算机与控制学院 广西桂林 541004) 2)(南京大学计算机软件新技术国家重点实验室 南京 210093) 3)(南京大学计算机科学与技术系 南京 210093) |
| 发表年份 | 2009 |
| 发表月份 | 5期(992—1001) |
| 文章摘要 | 摘要 在模型检验中，抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL，基于抽象解释框架以及完备抽象解释和性质强保留之间的关系，抽象模型最小精化使得CTL性质强保留，可转换为抽象解释中抽象域的最小完备精化，并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域，然后通过不动点求解，获得对CTL标准算子完备的最小抽象域，并依据此抽象域求得CTL性质强保留的最优抽象状态划分，最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的. 关键词 抽象解释;抽象模型检验;强保留;完备性;精化 中图法分类号 TP311 DOI号: 10.3724/SP.J.1016.2009.00992 |