有界模型檢測(cè)完備性閾值的優(yōu)化計(jì)算.pdf

1、有界模型檢測(cè)是尋找系統(tǒng)錯(cuò)誤的一種符號(hào)化模型檢測(cè)技術(shù)。它使用可滿足性問(wèn)題求解器求解模型檢測(cè)問(wèn)題，避免了其他模型檢測(cè)技術(shù)面臨的狀態(tài)空間爆炸問(wèn)題，然而它的計(jì)算時(shí)間復(fù)雜度是指數(shù)級(jí)別的。有界模型檢測(cè)方法的一個(gè)最大不足是，它雖然能有效的證明系統(tǒng)不滿足某一性質(zhì)，但很難或不能證明系統(tǒng)滿足某一性質(zhì)，即只能證偽不能證實(shí)。所以有界模型檢測(cè)對(duì)系統(tǒng)的驗(yàn)證是不完全的或者說(shuō)是不完備的。每一個(gè)有限狀態(tài)系統(tǒng)模型M和線性時(shí)態(tài)邏輯公式δ，都存在一個(gè)自然數(shù)CT，如果找不到長(zhǎng)度

2、小于CT的線性時(shí)態(tài)邏輯公式δ的反例，那么系統(tǒng)模型滿足公式δ，記作M|=δ，這個(gè)自然數(shù)稱為完備性閾值CT(CompletenessThreshold)。完備性閾值的計(jì)算是很困難的，有時(shí)候計(jì)算出來(lái)的值是巨大的。本文討論了系統(tǒng)模型的表示，提出系統(tǒng)關(guān)鍵變量和等價(jià)簡(jiǎn)化模型的概念，通過(guò)尋找非系統(tǒng)關(guān)鍵變量來(lái)合并系統(tǒng)狀態(tài)，得到等價(jià)簡(jiǎn)化模型。在這個(gè)模型上計(jì)算完備性閾值，提高了計(jì)算的效率同時(shí)得到簡(jiǎn)化模型的縮小的完備性閾值。本文實(shí)現(xiàn)了基于深度優(yōu)先搜索的算法來(lái)