基于K-模拟的抽象  

K-Simulation Based Abstractions

作　　者：袁志斌[1] 徐正权[1] 王能超[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉430074

出　　处：《计算机科学》2007年第9期242-244,共3页Computer Science

基　　金：国家自然科学基金(70271069)的支持

摘　　要：尽管近年来模型检测取得了很大的进步,但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中,抽象技术是最有效的方法之一。本文给出了基于K-模拟的抽象的高效算法,并证明了在线性时序逻辑框架下抽象的可靠性和完备性。In spite of the impressive progress in the development of model checking, it is still limited in their ability to handle large systems. It is generally recognized that abstraction techniques are one of the most general state reduction techniques. A novel efficient algorithm for computing abstraction of Kripke structure based on K-simulation is proposed. The soundness and completeness of abstraction framework in Linear temporal logic are proved.

关 键 词：抽象 线性时序逻辑 K-模拟 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]