時態(tài)邏輯及其在決策系統(tǒng)中的應(yīng)用

時態(tài)邏輯及其在決策系統(tǒng)中的應(yīng)用第1頁，課件共25頁，創(chuàng)作于2023年2月

斷言推理1目錄

時態(tài)邏輯

2

SIDSS系統(tǒng)描述

3

系統(tǒng)實(shí)現(xiàn)4

總結(jié)

5第2頁，課件共25頁，創(chuàng)作于2023年2月

斷言推理1Pre→Post由這樣的斷言推理為核心組織的產(chǎn)生式系統(tǒng)在決策支持系統(tǒng)、專家系統(tǒng)中使用得最多，也是最為成熟的解決方案但是語義是靜態(tài)的當(dāng)遇到諸如動態(tài)的、實(shí)時的、并發(fā)的或具有其他時態(tài)特性的推理時，這種靜態(tài)的推理方式則有很大的缺陷時態(tài)邏輯斷言推理則可有效地彌補(bǔ)這方面出現(xiàn)的難題。第3頁，課件共25頁，創(chuàng)作于2023年2月

時態(tài)邏輯2時態(tài)邏輯（tenselogic）是非經(jīng)典邏輯的分支學(xué)科其研究對象是:

把含有時態(tài)動詞的語句形式化

把含有這種語句的推理系統(tǒng)化引入以下常見的時態(tài)邏輯操作符：

Next:

ΟA,IfAandBareformulaethenΟA

Always:

□A,AlwaysinthefutureA

Sometimes:

A,SometimesinthefutureA

Until:

AUB,AuntilB

Since:

ASB,AsinceB

After:

AΠB,BafterA第4頁，課件共25頁，創(chuàng)作于2023年2月

系統(tǒng)描述3智能工資決策支持系統(tǒng)（SIDSS）是由劉冬寧、湯庸等人自主開發(fā)的一個典型的時態(tài)信息系統(tǒng)目前已有6000多家機(jī)關(guān)事業(yè)單位用戶針對我國機(jī)關(guān)事業(yè)單位工資政策復(fù)雜性、地域性和時間性等主要特點(diǎn)應(yīng)用時態(tài)數(shù)據(jù)和知識處理技術(shù)解決了根據(jù)機(jī)關(guān)事業(yè)單位工作人員隨時間變化影響工資變動的信息（時態(tài)性數(shù)據(jù)），依據(jù)相應(yīng)時期的工資政策（時態(tài)知識庫）自動確定工資的問題第5頁，課件共25頁，創(chuàng)作于2023年2月3.1SIDSS中的時態(tài)特征根據(jù)我國國情，工資政策繁雜，隨時間變動大在復(fù)雜的規(guī)則、高時態(tài)信息變動的條件下如何確保工資確定的正確性成了SIDSS中的重點(diǎn)和難點(diǎn)涉及到了大量的斷言推理與時態(tài)信息處理

系統(tǒng)描述3第6頁，課件共25頁，創(chuàng)作于2023年2月簡單地以工資政策中“兩年優(yōu)秀晉升”的政策為例該政策在1999年以前的描述是這樣的：

如果人員連續(xù)兩年考核優(yōu)秀，或某年考核優(yōu)秀有“一年優(yōu)”標(biāo)志，工資檔次允許晉升一檔，考核結(jié)果有效年份從下年算起，但連續(xù)兩次晉升之間必須相隔兩年以上。在1999年以后的描述則改為：

其他與之前相同，但連續(xù)兩次晉升之間必須相隔四年以上。舉例說明：

人員A從1995年到2000年的考核均為優(yōu)秀，則他可以分別在1997年和1999年執(zhí)行一次工資檔次晉升，而不允許在2001年執(zhí)行檔次晉升，正是由于1999年以后的工資政策規(guī)定，2001年與1999年之間并未相隔4年以上，因此不能進(jìn)行晉升

系統(tǒng)描述3第7頁，課件共25頁，創(chuàng)作于2023年2月表1人員A工資晉升隨時間的變化年份考核結(jié)果執(zhí)行操作政策依據(jù)1995優(yōu)秀

1999年以前的“兩年優(yōu)晉升”相隔必須兩年以上1996優(yōu)秀1997年允許晉升一檔1997優(yōu)秀

1998優(yōu)秀1999年允許晉升一檔1999優(yōu)秀

1999年以后的“兩年優(yōu)晉升”相隔必須四年以上2000優(yōu)秀2001年不允許晉升一檔

系統(tǒng)描述3第8頁，課件共25頁，創(chuàng)作于2023年2月3.2規(guī)則描述在“人員越級晉升”的過程中，會遇到的各種規(guī)則本文中僅以1999年更改政策一項(xiàng)規(guī)則變更為基準(zhǔn)其規(guī)則、條件、動作的相關(guān)表如下：

系統(tǒng)描述3第9頁，課件共25頁，創(chuàng)作于2023年2月規(guī)則規(guī)則名規(guī)則說明起始條件表達(dá)式規(guī)則生命周期R1越級晉升用于處理1999年以前考核結(jié)果引起的越級晉升C1[1993/10,1998/12]R2越級晉升用于處理1999年以后考核結(jié)果引起的越級晉升C2[1999/1,NOW]表2越級晉升規(guī)則表

系統(tǒng)描述3第10頁，課件共25頁，創(chuàng)作于2023年2月表3越級晉升條件表?xiàng)l件條件THENELSEC1連續(xù)兩年考核結(jié)果優(yōu)秀C3NULLC2連續(xù)兩年考核結(jié)果優(yōu)秀C4NULLC3當(dāng)前年份—上次越級晉升年份>=2或以前從未越級晉升A1NULLC4當(dāng)前年份—上次越級晉升年份>=4或以前從未越級晉升A1NULL

系統(tǒng)描述3第11頁，課件共25頁，創(chuàng)作于2023年2月表4越級晉升動作表動作動作NEXTA1人員工資檔次加一檔NULL表2~4中，是關(guān)于“越級晉升”這一事件涉及到的規(guī)則、條件和動作。從表中可以看到這樣的規(guī)則、條件、動作具有斷言推理的特征，而其中在規(guī)則表中，定義的生命周期，更體現(xiàn)了時態(tài)變更性的特點(diǎn)，同時這一系列的判斷推理都具有強(qiáng)時序性，鑒于對推理的正確性應(yīng)引入時態(tài)邏輯斷言推理。

系統(tǒng)描述3第12頁，課件共25頁，創(chuàng)作于2023年2月4.1時態(tài)邏輯斷言規(guī)則的設(shè)計(jì)根據(jù)表2~4，設(shè)計(jì)執(zhí)行規(guī)則如下：（S1）WhenReceivePromotingApplication

Then_DoTimeVerificationAnd_ThenCondictionChecking（S2）WhenCondictionChecking

Then_DoPromotionExecuting在執(zhí)行規(guī)則中體現(xiàn)出了較強(qiáng)的時間序列性（1）接到越級晉升的請求后，先判斷系統(tǒng)時間，根據(jù)規(guī)則的生命周期挑出該使用的條件序列判斷；（2）完成匹配條件序列判斷嵌套；（3）執(zhí)行動作。

系統(tǒng)實(shí)現(xiàn)4第13頁，課件共25頁，創(chuàng)作于2023年2月進(jìn)一步細(xì)化這些執(zhí)行序列：（S3）WhenCondictionChecking

IfInvalidCondiction

Then_DoNext_CondictionChecking

UntilEndofLayer_CondictionChecking在條件判斷嵌套過程中，當(dāng)前條件得不到匹配時，則輪轉(zhuǎn)到下一條件進(jìn)行匹配，直到該層所有條件判斷完畢即判斷嵌套完成

系統(tǒng)實(shí)現(xiàn)4第14頁，課件共25頁，創(chuàng)作于2023年2月（S4）WhenCondictionChecking

IfEndofLayer_CondictionChecking

Then_DoRejectPromotingApplication在條件判斷嵌套過程中，當(dāng)前條件得不到匹配和該層所有條件又判斷完畢時，則表示不符合越級晉升的條件，不通過該處理（S5）WhenNotInvalidCondiction

Then_DoNextLayer_CondictionCheckingUntilEndofAll_CondictionCheckingAnd_ThenPromotionExecute在條件判斷嵌套中，當(dāng)前條件匹配成功則遞進(jìn)到下一層條件判斷，如所有條件沒有判斷完畢則繼續(xù)進(jìn)行判斷嵌套直到嵌套完畢，如嵌套完畢而條件匹配又成功則執(zhí)行晉升動作

系統(tǒng)實(shí)現(xiàn)4第15頁，課件共25頁，創(chuàng)作于2023年2月4.2對斷言規(guī)則的邏輯描述對（S1）、（S2）邏輯描述如下：（S6）receive(SIDSS,Promoting_Application)=>verify(SIDSS,System_Time)Πcheck(SIDSS,Condiction)其中“Π”表示After，AΠB，意為BafterA。（S7）check(SIDSS,Condiction)=>act(SIDSS,Promotion)

系統(tǒng)實(shí)現(xiàn)4第16頁，課件共25頁，創(chuàng)作于2023年2月對（S3）-（S5）邏輯描述如下：（S8）check(SIDSS,Condiction)∧┑match(SIDSS,Condiction)=>samelayer_check(SIDSS,Condiction)Uend_check(Condiction,Layer)其中“U”在這里代表Until。（S9）┑match(SIDSS,Condiction)Πend_check(Condiction,Layer)=>reject(SIDSS,Promoting_Application)（S10）match(SIDSS,Condiction)=>(nextlayer_check(SIDSS,Condiction)Uend_check(Condiction,All))Πact(SIDSS,Promotion)

系統(tǒng)實(shí)現(xiàn)4第17頁，課件共25頁，創(chuàng)作于2023年2月4.3對規(guī)則生命周期的時態(tài)邏輯表示不僅可以對推理規(guī)則進(jìn)行時態(tài)邏輯斷言設(shè)計(jì)以及邏輯推理，還可對規(guī)則的生命周期也用時態(tài)邏輯進(jìn)行擴(kuò)展。引入時態(tài)因子Ti時態(tài)因子狀態(tài)T1表示時間T2表示時間表5時態(tài)因子表

系統(tǒng)實(shí)現(xiàn)4第18頁，課件共25頁，創(chuàng)作于2023年2月因此對規(guī)則R1和R2的表示分別為：（1）AlwaysR1SinceT1UntilT2（2）AlwaysR2SinceT2用時態(tài)邏輯運(yùn)算符表示為：（1）□((R1ST1)UT2)（2）□(R2ST1)

系統(tǒng)實(shí)現(xiàn)4第19頁，課件共25頁，創(chuàng)作于2023年2月4.4Java實(shí)現(xiàn)根據(jù)上述時態(tài)邏輯斷言，可以在代碼中實(shí)現(xiàn)上述規(guī)則斷言。調(diào)用TimeRoverInc.的TemporalRover工具它是一種用于處理Java程序中時態(tài)邏輯斷言并根據(jù)斷言生成有效Java代碼的工具，并可以配備數(shù)據(jù)庫表的工具DBRover同時使用。

系統(tǒng)實(shí)現(xiàn)4第20頁，課件共25頁，創(chuàng)作于2023年2月給出斷言規(guī)則（S6）-（S7）的Java偽代碼如下所示：S6:receivePromoting_Applicationimplies{Next{{checkCondiction}Until{verifySystemTime}}};S7:Always{{matchCondiction}implies{Next{actPromotion}}};

系統(tǒng)實(shí)現(xiàn)4第21頁，課件共25頁，創(chuàng)作于2023年2月給出斷言規(guī)則（S8）~（S10）的Java偽代碼如下所示：S8:If!{matchCondiction}implies{Next{{checkNext_Condiction}UntilEmpty{CondictionofthisLayer}}};S9:IfEmpty{CondictionofthisLayer}implies{Next!{actPromotion}};S10:If{matchCondiction}implies{Next{{{checkNextLayor_Condiction}UntilEmpty{AllCondictions}}implies{Next{actPromotion}}};

系統(tǒng)實(shí)現(xiàn)4第22頁，課件共25頁，創(chuàng)作于2023年2月對時態(tài)規(guī)則生命周期：（1）□((R1ST1)UT2)（2）□(R2ST1)給出Java偽代碼如下所示：（1）Always{{

R1SinceT1

}UntilT2

};（2）Always{

R2SinceT1