摘要
在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.
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 make it strongly preserving CTL can be formulated as a minimal abstract domain refinement in abstraction interpretation in order to get completeness, and this refined complete abstract domain always exists. Given initial abstract domain, we can obtain a minimal abstract domain which is complete for the standard operators of CTL by the iterative computation of the fixpoint. Moreover, the corresponding partition is the coarsest partition which is strong preserving for CTL. The authors show that the abstract domain is complete for the standard operators of CTL iff it is complete for complement and standard predecessor transformer operators.
出处
《计算机学报》
EI
CSCD
北大核心
2009年第5期992-1001,共10页
Chinese Journal of Computers
基金
国家杰出青年科学基金(60425206)
国家自然科学基金重大研究计划(90818027)
重点项目(60633010)
国家自然科学基金(60663005)
国家"八六三"高技术研究发展计划目标导向类项目(2009AA01Z147)资助~~
关键词
抽象解释
抽象模型检验
强保留
完备性
精化
abstract interpretation
abstract model checking
strong preservation
completeness refinement
