| 基于完备抽象解释的模型检验CTL公式研究 |
| |
| 引用本文： | 钱俊彦,徐宝文.基于完备抽象解释的模型检验CTL公式研究[J].计算机学报,2009,32(5). |
| |
| 作者姓名： | 钱俊彦 徐宝文 |
| |
| 作者单位： | 1. 桂林电子科技大学计算机与控制学院,广西,桂林,541004
2. 南京大学计算机软件新技术国家重点实验室,南京,210093;南京大学计算机科学与技术系,南京,210093 |
| |
| 基金项目： | 国家杰出青年科学基金，国家自然科学基金重大项目，国家自然科学基金重点项目，国家自然科学基金，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.
|
| 关 键 词： | 抽象解释 抽象模型检验 强保留 完备性 精化 |
Model Checking CTL Based on Complete Abstraction Interpretation |
| |
| QIAN Jun-Yan,XU Bao-Wen.Model Checking CTL Based on Complete Abstraction Interpretation[J].Chinese Journal of Computers,2009,32(5). |
| |
| Authors: | QIAN Jun-Yan XU Bao-Wen |
| |
| Affiliation: | School of Computer and Control;Guilin University of Electronic Technology;Guilin;Guangxi 541004;State Key Laboratory for Novel Software Technology;Nanjing University;Nanjing 210093;Department of Computer Science and Technology;Nanjing 210093 |
| |
| Abstract: | Abstraction plays a fundamental role in combating state-space explosion in model checking.In a complete Abstract interpretation-based view,the authors reduce the state space of a Kripke structure in order to obtain a minimal Abstract state translation system that strongly preserves a given temporal specification language CTL.According to a relation between completeness of Abstract interpretations and strong preservation of Abstract model checking,the problem of minimally refining Abstract model in order to ... |
| |
| Keywords: | Abstract interpretation Abstract model checking strong preservation completeness refinement |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
