[發(fā)明專利]一種對(duì)歷史事務(wù)的建模驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201810101474.3
• 申請(qǐng)日: 2018-02-01
• 公開（公告）號(hào): CN108197314B
• 公開（公告）日: 2020-06-09
• 發(fā)明（設(shè)計(jì)）人: 殷萍;高翠芳
• 申請(qǐng)（專利權(quán)）人: 江南大學(xué)
• 主分類號(hào): G06F16/36
• 分類號(hào): G06F16/36
• 代理公司: 哈爾濱市陽光惠遠(yuǎn)知識(shí)產(chǎn)權(quán)代理有限公司 23211
• 代理人: 張勇

1.一種對(duì)歷史事務(wù)的建模驗(yàn)證方法，其特征在于，包括以下步驟：

步驟一：將系統(tǒng)建立模型表示為M＝(S,→,L)，其中S是一個(gè)狀態(tài)集合，遷移關(guān)系→表示對(duì)每個(gè)s∈S，有某個(gè)s'∈S，滿足s→s'，標(biāo)記函數(shù)L表示S→P(Atoms)，P(Atoms)表示原子命題Atoms的冪集；

步驟二：對(duì)歷史事務(wù)進(jìn)行建模：

(1)增加一個(gè)計(jì)算過去一個(gè)政策被滿足次數(shù)的量詞，并用該量詞來寫另一個(gè)政策，公式擴(kuò)展為Nx:形式的構(gòu)造，其中x綁定公式并且不是自由出現(xiàn)的，表達(dá)方式如下：

其中n＝|{j|1≤j≤iΛ(h,j)|＝ψ}|，h代表“歷史事務(wù)”，i是一個(gè)整型變量，代表歷史事務(wù)中的第i個(gè)會(huì)話，ψ是一個(gè)公式，Nx:表示公式被滿足的次數(shù)，iff表示當(dāng)且僅當(dāng)；

(2)設(shè)置一個(gè)量詞進(jìn)行篩選，用擴(kuò)展的篩選量詞來修正，其表達(dá)方式如下：

其中是篩選量詞，保證對(duì)有限的值進(jìn)行量化，是它的唯一的自由變量；

步驟三：用φ表示上述邏輯公式，為公式φ構(gòu)造一個(gè)自動(dòng)機(jī)，用A_φ表示，該自動(dòng)機(jī)有一個(gè)接受跡的概念，跡是命題原子的賦值序列，從一條路徑出發(fā)，可以抽象出它的跡，自動(dòng)機(jī)A_φ有性質(zhì)：編碼滿足φ的所有跡，即所有滿足φ的跡；

步驟四：將自動(dòng)機(jī)A_φ與模型M結(jié)合，結(jié)合運(yùn)算的結(jié)果是一個(gè)遷移系統(tǒng)，其路徑既是自動(dòng)機(jī)的路徑又是該遷移系統(tǒng)的路徑；

步驟五：在結(jié)合的遷移系統(tǒng)中搜尋從s出發(fā)的滿足邏輯公式φ；如果存在該路徑，則輸出“Yes,M,s|＝φ”，即存在相應(yīng)的歷史事務(wù)；如果沒有這樣的路徑，則輸出“No，M,s|≠φ”，即不存在相應(yīng)的歷史事務(wù)。

2.如權(quán)利要求1所述的對(duì)歷史事務(wù)的建模驗(yàn)證方法，其特征在于，所述步驟二進(jìn)一步包括：在一些歷史數(shù)據(jù)無法獲取或者丟失的情況，局部可觀測(cè)性存在兩個(gè)問題，一個(gè)是潛在可滿足性，一個(gè)是遵守問題；部分可觀察的會(huì)話是p(u₁，...，u_n)形式的有限謂詞集合，其中p是未解釋的謂詞符號(hào)，每個(gè)u_i是常數(shù)或變量；部分可觀察的歷史是部分可觀察會(huì)話的有限列表，在部分可觀察歷史中，用V(h)表示在歷史h中出現(xiàn)的變量，用V(ψ)表示在公式ψ中出現(xiàn)的自由變量的集合。

3.如權(quán)利要求1所述的對(duì)歷史事務(wù)的建模驗(yàn)證方法，其特征在于，所述步驟二中篩選量詞是對(duì)策略線性時(shí)序邏輯的直接擴(kuò)展，即：

if(h,i)|＝ψ(c₁,...,c_n)then(h,i)|＝φ[x₁:＝c₁,...,x_n:＝c_n]

篩選量詞產(chǎn)生公式的表達(dá)方式如下：

其中列表是變量和常量的集合，用表示只有唯一自由變量的篩選量詞，正項(xiàng)篩選量詞代表唯一的變量是的公式，它的表達(dá)方式如下：

其中，S表示“自從”操作符。