摘要
尽管近年来模型检测取得了很大的进步,但是对于大系统的验证能力依然有限。在众多的状态减少和压缩技术中,抽象技术是最有效的方法之一。本文给出了基于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.
出处
《计算机科学》
CSCD
北大核心
2007年第9期242-244,共3页
Computer Science
基金
国家自然科学基金(70271069)的支持