時態(tài)描述邏輯DL-LiteLTL模型檢測研究.pdf

1、當前語義Web環(huán)境下復(fù)雜的動態(tài)系統(tǒng)存在著許多的時態(tài)規(guī)范，為了對這些時態(tài)規(guī)范進行驗證是否滿足系統(tǒng)所期望的性質(zhì)，本文采用了基于時態(tài)描述邏輯的模型檢測方法，對時態(tài)規(guī)范進行驗證，驗證結(jié)果表明該模型檢測方法是可行的。本文基于輕量級描述邏輯DL-Lite和線性時態(tài)邏輯LTL給出了時態(tài)描述邏輯DL-LiteLTL，用其對語義Web環(huán)境下動態(tài)性質(zhì)的刻畫，用含變量的時態(tài)合取查詢規(guī)范擴大了其描述的范圍，將描述邏輯的推理機制融入模型檢測過程中進行模型檢測，對

2、時態(tài)合取查詢規(guī)范進行驗證?？紤]到本體是不斷變化的，當期發(fā)生演變導致推理失效時，該文將其基于DL-Lite本體轉(zhuǎn)換為圖的方法，對不一致情況下的查詢應(yīng)答。
　　本研究主要內(nèi)容包括：⑴為了對Web環(huán)境下動態(tài)系統(tǒng)的時態(tài)規(guī)范進行驗證，本文首先結(jié)合輕量級描述邏輯DL-Lite和時態(tài)邏輯LTL給出時態(tài)描述邏輯DL-LiteLTL，用DL-Lite的知識刻畫能力對系統(tǒng)知識進行刻畫，用LTL的時態(tài)表達能力對系統(tǒng)的時態(tài)規(guī)范進行描述，然后將案例系統(tǒng)建模