基于完备抽象解释的模型检验CTL公式研究

• 作者: 徐宝文 钱俊彦
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 抽象解释 抽象模型检验 强保留 完备性 精化
• 年，卷（期）: 2009,（5）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 992-1001
• 页数: 10页
• 分类号: TP311
• 字数: 11227字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2009.00992

摘要

在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐宝文	南京大学计算机软件新技术国家重点实验室	40	414	12.0	19.0
5	钱俊彦	桂林电子科技大学计算机与控制学院	86	238	9.0	10.0