计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2007年
9期
242-244
,共3页
抽象%线性时序逻辑%K-模拟
抽象%線性時序邏輯%K-模擬
추상%선성시서라집%K-모의
尽管近年来模型检测取得了很大的进步,但是对于大系统的验证能力依然有限.在众多的状态减少和压缩技术中,抽象技术是最有效的方法之一.本文给出了基于K-模拟的抽象的高效算法,并证明了在线性时序逻辑框架下抽象的可靠性和完备性.
儘管近年來模型檢測取得瞭很大的進步,但是對于大繫統的驗證能力依然有限.在衆多的狀態減少和壓縮技術中,抽象技術是最有效的方法之一.本文給齣瞭基于K-模擬的抽象的高效算法,併證明瞭在線性時序邏輯框架下抽象的可靠性和完備性.
진관근년래모형검측취득료흔대적진보,단시대우대계통적험증능력의연유한.재음다적상태감소화압축기술중,추상기술시최유효적방법지일.본문급출료기우K-모의적추상적고효산법,병증명료재선성시서라집광가하추상적가고성화완비성.
